Welcome > Arch > Basics > Bluespec > Types

Types

Reference ¹

Strong, static type-checking.

Every variable and every expression in BSV has a type.

Convention: first char uppercase. (except for int and bit for backward compatibility with Verilog)

Type expression

Type expression/paramterized types: X#(t1,…,tn). X is the type constructor and x1,…,xn are parameters of X.

// Type Expression Examples
Tuple2#(int, Bool) // pair of items, an int and a Bool
Tuple3#(int, Bool, String)
List#(Bool)
List#(List#(Bool))
RegFile#(Integer, String)

//paraeter can be natural numbers (numeric types)
Bit#(16) // 16-bit wide bit-vector (16 is a numeric type)
bit[15:0] // synonym for Bit#(16)
Vector#(16, Int#(29)) // Vector of size 16, containing Int#(29)'s

bit[m:n] –> n must be 0.

Types in libraries

Prelude package.

Bit types: Bit#(n), UInt#(n), Int#(n), Bool, Maybe, Tuples;

Non-bit types: Integer, Real, String, Char, Fmt.

Maybe: used to tag values as Valid or Invalid, where valid values contain data.
Fmt: representation of arguments to the $display familiy of tasks.

Interface types: Reg, FIFO, Clock, Reset, Inout.

Types used by compiler:

Action. An expression intended to acto on the state of the circuit. equal to ActionValue#(void).
ActionValue#(a). An expression intended to act on the state of the cirtuit. a is the type of return value.

Rules. Used to represent one or more rules as a first class type.

method Action grab(Bit#(8) value);
last_value <= value;
endmethod

interface IntStack;
method Action push (int x);
method ActionValue#(int) pop();
endinterface: IntStack

seq
noAction;
endseq

Type synonyms:

typedef Bits#(8) Byte;
typedef Tuple2#(a, a) Pair#(type(a));
typedef 32 DataSize; typedef Bit#(DataSize) Data;

Enumerated types:

typedef enum(Red, Blue, Green) Color deriving(Bits, Eq)

Polymorphism:

List#(a)
List#(List#(b))
RegFile#(i,List#(x))

// Type variables, a, b, x, represent unknown (but specific) types.

Type Functions

used when defining variable size for types:

TAadd#(n1, n2): Calculate n1 + n2 // example: Int#(TAdd#(5,n)): define a signed integer n+5 bits wide, n must be in scope somewhere
TSub#(n1,n2)
TMul#(n1,n2)
TDiv#(n1,n2) // ceiling n1/n2
TLog#(n) // ceiling log_2(n)
TExp#(n) // 2^{n}
TMax#(n1,n2)
TMin#(n1,n2)

Provisos (brief intro)

A proviso is a static condition attached to certain constructs, to impose certain restrictions on the types involve in the construct. The restrictions are of two kinds:

Require instance of a type class (overloading group): this kind of proviso states that certain types must be instances of certain type classes, i.e., that certain overloaded functions are defined on this type.
Require size relationships: this kind of proviso expresses certain constraints between the size of certain types.

Common overloading provisos:

Bits#(t,n) // Type class (overloading group) Bits
        // Meaning: overloaded operators pack/unpack are defined
        // on type t to convert to/from Bit#(n)
        // pack/unpack: {1,0,1} <-> 101

Eq#(t)  // Type class (overloading group) Eq
        // Meaning: overloaded operators == and != are defined on type t

Literal#(t) // Meaning: Overloaded function fromInteger() defined on type t
            //  to convert an integer literal to type t. Also overloaded
            //  function inLiteralRange to determine if an Integer
            //  is in the range of the target type t.

Ord#(t) // Meaning: Overloaded order-comparison operators <, <=, > and >=
        //   are defined on type t

Bounded  // Meaning: Overloaded identifiers minBound and maxBound
         //  are defined for type t

Bitwise#(t) // Meaning: Overloaded operators &, |, ^, ~^, ^~, ~, <<, >>
            //   and overloaded function invert are defined on type t

BitReduction#(t) // Meaning: Overloaded prefix operators &, |, ^, ~&, ~|, 
                 //   ~^, ^~ are defined on type t

BitExtend#(t)  // Meaning: Overloaded functions extend, zeroExtend, signExtend and truncate are defined on type t

Arith#(t) // Meaning: Overloaded operators +, -, *, overloaded prefix operator - (same as function negate), negate, defined on type t

Size relationship provisos are:

Add#(n1,n2,n3) // Meaning: assert n1 + n2 = n3
Mul#(n1,n2,n3) // Meaning: assert n1 * n2 = n3
Div#(n1,n2,n3) // Meaning: assert ceiling n1 / n2 = n3
Max#(n1,n2,n3) // Meaning: assert max(n1,n2) = n3
Log#(n1,n2) // Meaning: assert ceiling(log(n1)) = n2
            // The logarithm is base 2

Example of using provisos:

module mkExample (ProvideCurrent#(a))
  provisos(Bits#(a,sa), Arith#(a));

  Reg#(a) value_reg <- mkReg(?); // requires that type "a" be in the Bits typeclass.
  rule every;
     value_reg <= value_reg + 1; // requires that type "a" be in the Arith type class.
  endrule

function Bit#(m) pad0101 (Bit#(n) x)
  provisos (Add#(n,4,m)); // m is 4 bits longer than n
  pad0101 = {x, 0b0101};
endfunction: pad0101

`deriving` clauses

directing the compiler to define automatically certain overloaded functions for that type.

deriving(Eq) // Meaning: automatically define == and != 
             //  for equality and inequality comparisons

deriving(Bits) // Meaning: automatically define pack and unpack
               // for converting to/from bits

deriving(FShow) // define fshow to convert to a Fmt representation for $display functions

deriving (Bounded) // automatically define minBound and maxBound

Example:

typedef enum {LOW, NORMAL, URGENT} Severity deriving(Eq, Bits);
// == and != are defined for variables of type Severity
// pack and unpack are defined for variables of type Severity

module mkSeverityProcessor (SeverityProcessor);
  method Action process (Severity value);
     // value is a variable of type Severity
     if (value == URGENT) $display("WARNING: Urgent severity encountered.");
     // Since value is of the type Severity, == is defined
  endmethod
endmodule

reference ↩

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?