Types

Types in Virdant describe the kinds of values that may flow across components and be stored in registers. Virdant has a strong, static type system that catches many classes of errors at compile time.

Every component in a Virdant design has a type annotation. The type determines what operations are valid on the value and how it is represented in hardware.

Built-in Types

Virdant provides several built-in types that serve as the primitive building blocks of hardware designs.

Clock

Clock represents a clock signal. A clock is a 1-bit signal that oscillates at a fixed frequency in standard operation.

Every reg declaration must have a clock associated with it. The register latches its next value on the rising edge of that clock.

Clock is an opaque type. There are no operations that can manipulate or inspect values of type Clock. Clocks may only be passed through ports or associated with registers using the on keyword.

mod Top {
    incoming clock : Clock
    // ...
}

Bit

Bit is a 1-bit value. It is analogous to the boolean type found in programming languages. Its two values are true and false.

wire ready : Bit
ready := true

Bit supports the following operations:

Logical: ! (not), && (and), || (or), ^^ (xor)
Comparison: ==, !=

Word

Word[n] is an n-bit unsigned integer value. n must be a compile-time constant natural number.

When used as a number, it is interpreted as an unsigned integer in 2’s complement representation.

wire data : Word[8]
data := 0xff

Word[n] supports the following operations:

Arithmetic: +, - (addition and subtraction)
Bitwise: &, |, ^, ~ (and, or, xor, not)
Comparison: ==, !=, <, <=, >, >=
Indexing: w[i], w[i..j] (bit and range selection)
Concatenation: word(...) builtin function

Operations are always fully defined. Overflow in addition and subtraction wraps around (modular arithmetic).

Valid

Valid[T] is an optional value that wraps any type T with a validity bit. The wire or register carrying the value may be valid (holding a value of type T) or invalid (holding no value). Like every enum, Valid is one-hot encoded: the total hardware width is width(T) + 2, where the 2-bit tag distinguishes @Valid from @Invalid above the payload.

Unlike Clock, Bit, and Word[n], which are built into the compiler, Valid[T] is an ordinary generic enum type defined in the builtin package:

pub enum type Valid[T : Type] {
    Invalid
    Valid(value : T)
}

It requires no special compiler support. See Generics and Parameterized Types for the full generics story.

wire v1 : Valid[Bit]
v1 := @Valid(true)

wire v2 : Valid[Bit]
v2 := @Invalid()

Two constructors are provided:

@Valid(value) — wraps a valid value of type T.
@Invalid() — represents an invalid (absent) value.

Values of type Valid[T] are deconstructed using match:

wire got_it : Bit
got_it := match v1 {
    with @Valid(x) => x
    with @Invalid() => false
}

The Valid[T] type is useful for representing handshake signals, optional values, or data that may not yet be ready.

Built-in Modules

In addition to built-in types, Virdant ships a small library of built-in modules in lib/builtin.vir. These modules are available to every design without an import.

Sync

Sync synchronizes a single Bit signal from one clock domain onto another. It safely samples an asynchronous input, such as a button press, into a synchronous design.

The Sync module exposes the following ports:

inp (incoming Bit): The asynchronous input signal on a foreign clock domain.
clock (incoming Clock): The clock of the destination domain. The synchronized output is updated on this clock.
out (outgoing reg of Bit on clock): The synchronized output.

Internally Sync is two back-to-back flip-flops on clock. The first register may go metastable when inp changes near the clock edge, but it has a full cycle to settle before the second register samples it. The output of the second register is therefore stable.

mod Top {
    incoming clock  : Clock
    incoming button : Bit

    mod sync of Sync {
        it.clock := clock
        it.inp   := button
    }

    outgoing led    : Bit {
        it := sync.out // `sync.out` is safe to use on `clock`.
    }
}

Struct Types

A struct type is a user-defined type that bundles several named fields together.

Struct types are declared with the struct type keywords:

struct type Color {
    red   : Word[8]
    green : Word[8]
    blue  : Word[8]
}

Each field has a name and a type. Struct types are nominal: two struct types with the same structure are distinct types.

Struct values are constructed with the $ syntax:

wire pixel : Color
pixel := ${ red = 0, green = 0, blue = 0 }

Fields are accessed with the -> projection operator:

wire r : Word[8]
r := pixel->red

Struct types support structural pattern matching in match expressions. For details, see the Patterns chapter.

Union Types

A union type, also known as an algebraic data type, represents a value that may take one of several alternative forms. Each alternative, called a variant, may carry associated data of its own.

Union types are declared with the union type keywords:

union type MyUnion {
    Foo()
    Bar(x : MyEnum)
}

A variant with no associated data is written with empty parentheses (). A variant with associated data lists the parameters inside the parentheses, similar to a function parameter list.

Union values are constructed using the @ syntax:

wire u : MyUnion
u := @Bar(#Baz)

Union values are deconstructed using match expressions:

wire result : MyEnum
result := match u {
    with @Foo()   => #Baz
    with @Bar(x)  => x
}

Union types must be matched exhaustively. If a variant is not covered by any arm of a match, the compiler will report an error.

Enum Types

An enum type is a fixed set of named constant values. Each named constant is called an enumerant. Enum types are declared with the enum type keywords:

enum type Opcode {
    Add = 1w4
    Sub = 2
    And = 4
    Or  = 8
}

Each enumerant may be given an explicit value with =. Values are constant expressions. The width of the enum type is taken from the first enumerant’s literal: write the first value with an explicit width (1w4 above); the remaining values may be bare literals.

If the first literal’s width is not inferrable, the enum’s width cannot be determined:

enum type Bad {
    A = 0
    B = 1
}

reports Enum type's first enumerant does not have an inferrable width. Add an explicit width, e.g. `= 0wN`. — write A = 0w4 instead.

Every enumerant must have a distinct value. Two enumerants that evaluate to the same value are an error, even when the values are written in different bases:

enum type Code {
    A = 15w4
    B = 0x0F
}

reports Duplicate enum value: enumerants of Code share value 15.

Enum values are referenced with the # syntax:

wire op : Opcode
op := #Add

Enum values may be compared with == and !=. They may be matched in match expressions:

wire decoded : Word[8]
decoded := match op {
    with #Add => 1
    with #Sub => 2
    with #And => 3
    with #Or  => 4
}

Enum types also participate in the word() and any() builtin functions.

In hardware, an enum whose enumerants carry no parameters is represented as a tag of the enum’s width. When some enumerants carry parameters (see Payload Enumerants below), the representation is a tag followed by the widest payload, like a union.

One-Hot Encoding by Default

When no enumerant specifies a value, the enumerants are one-hot encoded: enumerant i (in declaration order) gets the value 1 << i, and the width of the enum type is the number of enumerants.

enum type State {
    Idle   // value 1 (1 << 0)
    Busy   // value 2 (1 << 1)
    Done   // value 4 (1 << 2)
}

mod Ctl {
    incoming state : State
    outgoing code : Word[3] // State is exactly 3 bits wide.
    code := word(state)     // #Idle == 1, #Busy == 2, #Done == 4.
}

One-hot is the default for two reasons:

The all-zeros word is never a valid enumerant, so a signal that has been explicitly initialized to zero can never be confused with a legitimate enum value.
Testing which enumerant a signal holds, and comparing it against a constant, only requires checking a single bit.

Giving some enumerants explicit values and leaving others unspecified is ambiguous, and therefore an error — either give every enumerant a value, or none:

enum type Color {
    Red
    Green = 1
    Blue
}

reports Enum type Color specifies values for some but not all enumerants. Either give every enumerant a value, or none (which defaults to one-hot encoding).

Payload Enumerants

An enumerant may carry parameters, like a union variant:

enum type Opt[T : Type] {
    None
    Some(value : T)
}

An enumerant that carries parameters is constructed with the @ syntax, exactly like a union variant:

wire o1 : Opt[Word[4]]
o1 := @Some(14w4)

An enumerant without parameters uses the # syntax, and may also be constructed with an empty argument list:

wire o2 : Opt[Word[4]]
o2 := #None

wire o3 : Opt[Word[4]]
o3 := @None()

Using #Name on an enumerant that carries parameters is an error:

o1 := #Some

reports Ctor Some requires arguments: use @Some(...).

Payload enumerants are matched with with @Name(pattern), which binds the parameters to names inside the arm:

wire inner : Word[4]
inner := match o1 {
    with @Some(v) => v
    with #None    => 0
}

Matching an enum exhaustively requires covering every enumerant, with or without parameters; a missing enumerant is reported like a missing union variant (Non-exhaustive match ... not covered: #None).

The builtin Valid[T] type is exactly such a generic payload enum (see Valid above):

pub enum type Valid[T : Type] {
    Invalid
    Valid(value : T)
}

For the pattern side, see the Patterns chapter.

Generics and Parameterized Types

Type definitions may declare generic parameters, making them parameterized (generic) types. This is how Word[n] supports arbitrary bit widths and how Valid[T] wraps an arbitrary type.

Every type definition form may declare generic parameters: struct type, union type, enum type, and builtin type. The parameter list is written in square brackets after the type name. Parameters are comma-separated, and each parameter is written name : kind:

struct type Pair[A : Type, B : Type] {
    fst : A
    snd : B
}

union type Either[L : Type, R : Type] {
    Left(l : L)
    Right(r : R)
}

enum type Opt[T : Type] {
    None
    Some(value : T)
}

builtin type Word[n : Nat] {}

The parameter list syntax is shared by all definition forms; the two available kinds are described in Kind System below:

Generics := "[" KindParamList "]"
KindParamList := (KindParam ",")* KindParam
KindParam := Ident ":" Kind

Module and socket definitions accept the same generic parameter lists; see Modules and Sockets.

Generic parameter names are in scope inside the body of the declaring definition, where member types may reference them by name (fst : A and snd : B above). The definition is analyzed once, generically, with the parameters as placeholders; actual types are substituted only at the use sites.

Type Arguments

A reference to a generic type supplies type arguments in square brackets, comma-separated and in the same order as the declared parameters: Pair[Word[4], Bit] supplies Word[4] for A and Bit for B.

A parameter of kind Nat takes a number literal, as in the familiar Word[8]. A parameter of kind Type takes a full type expression, so type arguments nest to arbitrary depth:

reg pair : Pair[Word[4], Bit] on clock {
    it <= ${ fst = a, snd = b }
}

// The argument to Valid is itself a full type expression.
wire nested : Valid[Pair[Word[4], Bit]]
nested := @Valid(${ fst = a, snd = b })

Checks at the Reference Site

The number and the kinds of the type arguments are checked at each reference site.

Wrong arity. A reference must supply exactly one argument per declared parameter:

incoming inp : Pair[Bit]

reports Type Pair takes 2 type arguments, but 1 was given.

Kind mismatch, `Type` parameter given a number. A Type parameter stands for a whole type, not a number literal:

incoming inp : Valid[8]

reports Type argument mismatch: parameter T of Valid expects a type, but found a Nat literal.

Kind mismatch, `Nat` parameter given a type. A Nat parameter stands for a number literal:

incoming inp : Word[Bit]

reports Type argument mismatch: parameter n of Word expects a Nat, but found a type.

Unbound parameter. A generic parameter name is only in scope inside its declaring definition; referencing it anywhere else is an unresolved type:

struct type Box[T : Type] {
    value : T
}

pub mod Top {
    incoming inp : T
}

reports Unresolved type T.

Parameters take no arguments. A generic parameter stands for a single type and cannot itself be applied to type arguments:

struct type Box[T : Type] {
    value : T[Bit]
}

reports Parameter T takes no type arguments.

Type Expressions

A type expression in Virdant consists of an ofness (a simple name like Word or a fully-qualified name like buffer::BufferType) followed by an optional comma-separated list of type arguments in square brackets:

type            ::=  Ofness GenericsParams?
ofness          ::=  Ident | Ident "::" Ident
genericsparams  ::=  "[" GenericsArgList "]"
genericsarglist ::=  (GenericsArg ",")* GenericsArg
genericsarg     ::=  Nat | Type

The argument list is matched against the generic parameters of the referenced type in declaration order. Each argument is either a number literal (for a Nat-kind parameter) or a full type expression (for a Type-kind parameter), so type arguments nest arbitrarily: Valid[Pair[Word[4], Bit]].

Kind System

Types are classified into kinds. A kind describes what a generic parameter stands for.

Virdant has exactly two kinds:

Type — the parameter stands for a whole type, such as Bit, Word[4], or a user-defined type.
Nat — the parameter is a number literal, used for bit widths (as in Word[n : Nat]).

Any other kind name is a compile-time error. Declaring a parameter with an unknown kind:

struct type S[X : Foo] {
    value : X
}

reports:

Unknown kind Foo: generic parameters must be declared as `: Type` or `: Nat`