Spade 0.21.0 | The Spade Blog

Associated changelog Swim changelog Git DOI

Today we release Spade v0.21.0! Since we skipped one release this version is packed with big and small changes. As always, you can read all the changes in the Changelog

Begone, `$`

One of the worst eye sores in the Spade syntax has been the $ used for named arguments. We finally managed to find a way to improve that which means that named arguments can now be passed in two ways, so what used to be written as

$(shorthand, long: value)

can now be written as

(shorthand:, long: value)

{ shorthand, long: value }

In principle, you are free to use either version, though our official recommendation is to use () for units and {} for types.

Disclaimer: ::$<...> syntax for named type parameters remain in Spade, for now.

Dedicated Memories

A fundamental assumption that Spade makes around state elements is that all register values are re-computed by a combinational circuit every clock cycle. However, early on, we realized that this is incompatible with defining memory-like structures, since those only update a fixed number of memory cells every clock cycle. As an interim solution early on, we added the clocked_memory construct; a special entity that the compiler is able to lower into a memory structure. Several years later, this interim solution and its ugliness lived on, until now.

With this release, we are adding a new memory to the language. With it, a memory is defined by the number of elements it contains, as well as which read and write ports it should have. For example, a 32 bit register file with two read ports and one write port can be written, all with 1 clock cycle latency can be written as

memory: [[bool; 32]; 32] {
    r0: std::mem::Ro<[bool; 32], 32, 1>,
    r1: std::mem::Ro<[bool; 32], 32, 1>,
    w: std::mem::Wo<[bool; 32], 32, 1>,
};

You can also specify initial values for the memory by adding initial(...) after the memory keyword.

Type inference also allows skipping most of the tedium when the information is already available somewhere

// Port type parameters can be inferred from the memory type
memory: [[bool; 32]; 32] {
    r0: std::mem::Ro<_, _, 1>,
    r1: std::mem::Ro<_, _, 1>,
    w: std::mem::Wo<_, _, 1>,
};

// Even the memory type can be inferred from a known initial value!
memory initial([[false; 32]; 32]) {
    r0: std::mem::Ro<_, _, 1>,
    r1: std::mem::Ro<_, _, 1>,
    w: std::mem::Wo<_, _, 1>,
};

r0, r1 and w are ports to the memory which you can use to read or write its content.

This memory construct is designed to cover most use cases for memories in FPGAs, assuming you do not use too many ports, though it does not attempt to model all possible memories. If you need to use specific features of the memories on your platform, you are better off directly instantiating the vendor provided memory primitives.

Copy views contain `inv` wires + `inspect`

In v0.20 we introduced “copy views” (&T) which allow you to access types containing inverted wires without actually consuming the whole type, effectively allowing you to inspect the values. In that initial implementation, a big limitation was that inverted components were erased. For example,

struct ReadyValid<T> {
    is_ready: inv bool,
    data: Option<T>,
}

let ready_valid_view: &ReadyValid<T> = /* ... */;
let data: Option<T> = *ready_valid_view.data;

worked alright and retrieved the forward value, but there was no way to “peek into” backward wires.

let is_ready: bool = ready_valid_view.is_ready /* what now? */;

Spade v0.21 makes copy views carry inverted wire data and adds a method to inv wires, inspect, that flips their direction to allow reading their values:

// Step by step
let step_1: &inv bool = ready_valid_view.is_ready;
let step_2: &bool = step_1.inspect();
let is_ready: bool = *step_2;

// Now in one go
let is_ready = *ready_valid_view.is_ready.inspect();

`inv` in enums

Enums allow you to model, among other things, valid/data pairs in a type safe manner. I.e. the language can prevent accidentally reading invalid data. In an attempt to do the same for ready-signals we have added support for enums to contain inv wires.

For example, a ready/data pair can be written as

enum Bus<T> {
    Busy,
    Ready { t: inv T }
}

A unit which consumes a ready/data pair as input can now take an inverted Bus as an input, to which it can set Busy/Ready depending on its readyness. To set Ready, it must provide a signal where it will accept the data, and a consumer of a ready/data pair can only get access to this signal when it has checked the Busy/Ready state of the bus.

In its current state, using this feature turns out to be somewhat unergonomic so a bit more work is needed.

Conditionals returning `inv`

In this new release of Spade, inv wires can be returned from conditional blocks like if/else or match blocks. When the returned wire is set to some value, all branches of the conditional block observe the same value.

let cond = /* some boolean condition */;

let (a_input, b_input, output) = if cond {
    let (a, a_inv) = port();
    let (b, b_inv) = port();

    (a_inv, b_inv, a +. b)
} else {
    let (a, a_inv) = port();
    let (b, b_inv) = port();

    (a_inv, b_inv, a -. b)
};

set a_input = 3i8;
set b_input = 5i8;

`const type`

Spade does not yet have a system corresponding to const in Rust. While this is planned, a stop gap solution has been to use the type level math expression system to perform computations that are guaranteed to be const evaluated, but doing this has been tedious. With this release we added a const type {..} expression where you can perform type level arithmetic directly in an expression.

`gen match`

A mechanism analogous to gen if has been added that matches type values instead of testing conditions to determine which block of code to include.

// Example from Spade's stdlib
fn zip<O>(self, other: [O; N]) -> [(T, O); N] {
    gen match N {
        0 => [],
        1 => [(self[0], other[0])],
        _ => {
            let (ll, lr) = self.split_at::<{N/2}>();
            let (rl, rr) = other.split_at::<{N/2}>();

            let l = ll `zip` rl;
            let r = lr `zip` rr;

            l.concat(r)
        }
    }
}

The choice between gen match and gen if is mostly aesthetic, letting the developer better express their intent.

No more `inv` consumption in conditionals

inv wires coming from outside a conditional block (if/else or match) cannot be consumed inside them anymore. It never worked in any reasonable way, but it was never rejected explicitly which is changed now.

`impl` for type aliases

This new version fixes an annoying bug: impl blocks targetting type aliases were completely broken! Now they work fine.

struct CoolArray<T, #uint N> {
    cool: [T; N],
}

type CoolTenArray<T> = CoolArray<T, 10>;

impl<T> CoolTenArray<T> {
    fn first_cool(self) -> T {
        self.cool[0]
    }
}

fn main() -> {
    let x: CoolArray<bool, 10> = CoolArray([true; 10]);
    // This used to fail because `.first_cool()` was defined for `CoolTenArray<T>`, not `CoolArray<T, 10>`
    let y = x.first_cool();
}

`set` through arrays and tuples

Inverted wires must be set with, well, set. So far, the requirement was strict: given a right-hand side type T, the left hand side had to be inv T.

fn connect_things_together(fwd: bool, back: inv bool) {
    set back = fwd;
}

However, this simple definition was too limiting: several users reported having trouble with set when tuples and arrays were involved:

entity top(leds: [inv bool; 4]) {
    // error! `leds` is `[inv bool; 4]`, not `inv [bool; 4]`
    set leds = [true, true, false, false];
}

The technically correct answer involved a lecture about our type system and what set expects, but the real lesson we learned is that users kept making this mistake and expecting a reasonably-looking piece of code to work.

Spade v0.21 makes set a bit smarter, allowing setting arrays and tuples element-wise when each pairs of elements have matching types.

entity top(leds: [inv bool; 4], things: (inv bool, inv int<8>)) {
    // Now this is allowed (each `inv bool` can be set to a `bool` value)
    set leds = [true, true, false, false];

    // It also works with tuples
    set things = (true, 4);
}

Cocotb 2.1

For the long time, we have been using cocotb 1.9.2 for tests since we relied on some cocotb internals that changed with 2.x for test discovery. We have finally addressed this and are now using cocotb 2.1, giving you access to new cocotb features.

This also means that the tests should work on macos without intervention

Implicit register clocks in pipelines

reg(clk) count_up initial(0) = count_up +. 1;

However, inside pipelines, there is already an implicit clock that drives registered stages (it is always the first parameter of the pipeline, which must be a clock).

pipeline(1) count_up_and_compare_against_sum(clk: clock, a: int<8>, b: int<8>) -> bool {
    reg(clk) count_up initial(0) = count_up +. 1;
    let sum = a +. b;
reg;
    count_up == sum
}

To make registers like these more concise and to avoid the potential mistake of using the wrong clock in multi-clock pipelines, now the clock parameter of registers can be omitted inside pipelines.

pipeline(1) count_up_and_compare_against_sum(clk: clock, a: int<8>, b: int<8>) -> bool {
    // v-- uses `clk` implicitly
    reg count_up initial(0) = count_up +. 1;
    let sum = a +. b;
reg;
    count_up == sum
}

Altered definitions of `Data` and `Copy`

Before, Data was a finer selection of types that were already Copy, essentially specifying all types that can be easily read and consumed multiple times without any problems, and with Data also excluding clock.

To handle inv better, including but not limited to them now being allowed inside enums, their definition was altered to not be built on top of each other but complete each other instead:

Copy still describes a type which can be passed around and read freely an indefinite amount of times (e.g. uint<8>, clock).
Data now means that the associated value is actually known to be represented by bits that may run on your targets data wires. This may be, as before, bool, uint<8>, etc. while still not including clock, but now also includes non-Copy types like inv bool.

To store a value in an register, you thus now need a type both Copy and Data.

Those traits are still automatically derived and shouldn’t cause any problems.

Begone, $

Dedicated Memories

Copy views contain inv wires + inspect

inv in enums

Conditionals returning inv

const type

gen match

No more inv consumption in conditionals

impl for type aliases

set through arrays and tuples