Spade

Spade Logo

Spade is a Rust-inspired hardware description language.

For a brief guided introduction to Spade, you can read the chapter on implementing a ws2128 RGB LED driver

If you are more interested in a reference of all constructs in the language, see the language reference

If you have any questions or would like to discuss Spade with others, feel free to join the Discord community.

Spade is a work in progress language and so is this documentation. Writing documentation is hard since it is hard to know what details are obvious and what things need more explanation. To make the documentation better, your feedback is invaluable so if you notice anything that is unclear or needs more explanation, please, reach out either via a gitlab issue or on Discord

Chapters

Installation

At the moment, Spade is only well-supported on Linux systems, though some users have had success running it on macOS as well. Windows is not supported for now, though it should be usable in WSL.

In order to install Spade, you need the Rust toolchain, specifically cargo. If you don't have it installed, you can install it with https://rustup.rs/. Simply run the command there, make sure its binaries are in your PATH and then run rustup toolchain install stable

Unless you have specific needs, you should install the Spade compiler via its build tool Swim. Swim then manages the compiler version on a per-project basis. To install Swim, run

cargo install --git https://gitlab.com/spade-lang/swim

If you are on arch-linux you can also install the swim-git package from the aur https://aur.archlinux.org/packages/swim-git

You should now be able to create a swim project using swim init hello_world

Synthesis Tools and Simulators

Spade compiles to Verilog code which is simulated and synthesised (compiled to hardware) by other tools. In particular cocotb for simulation, and yosys+nextpnr for synthesis.

Automated install

The easiest way to install those tools is via Swim. This is done by running

swim install-tools

which downloads https://github.com/YosysHQ/oss-cad-suite-build into ~/.local/share/swim. If it is installed, swim will always use the cad-suite tools instead of system tools.

NOTE: If you need to uninstall those tools, remove ~/.local/share/swim/bin

Manual install

You can also install the tools manually. Refer to the individual installation instructions in that case. The tools you need are:

  • Python3.8 or later
  • Simulation via Icarus Verilog (using cocotb): https://github.com/steveicarus/iverilog
  • Simulation via Verilator: https://github.com/verilator/verilator
  • Synthesis: https://yosyshq.net/yosys/
  • Place and route: https://github.com/YosysHQ/nextpnr. Build nextpnr-ice40 or nextpnr-ecp5 depending on your target FPGA
  • Bitstream generation and upload. Depends on your target FPGA
  • Cocotb: https://www.cocotb.org/ (this automatically is installed for you by swim)

If you're just starting out, you probably don't need all of these. Start of by simulating your designs using cocotb and icarus, then you can move on to testing in hardware using yosys and nextpnr.

If your simulations are too slow, you can try verilator

Simulation and Testing

Because it is time-consuming and difficult to debug hardware, most hardware projects use simulation to speed up the development process and ease debugging.

To set up simulation, add a simulation section to your swim.toml file, specifying in which directory the test files will be placed (usually test)

[simulation]
testbench_dir = "test"

Tests are not written in Spade itself, instead they are written in Python using cocotb or C++ in Verilator. Cocotb is easier to set up and use but is usually very slow.

If you haven't already, install the tools by following the installation instructions

Cocotb

Any Python files in the testbench_dir will be run with cocotb. The first line must be a comment on the form

# top = <path to unit under test>

where the path is relative to your project. I.e. if you have a unit called top in main.spade, this will be main::top

Tests are asynchronous functions annotated with @cocotb.test(), they take a single input which is the design under test.

When working with Spade, you generally want to be able to use Spade values rather than pure bit vectors. To do so, import SpadeExt from spade and instantiate SpadeExt class, passing the dut to hits constructor.

You can then access the inputs of your unit using .i.<input name> and the output using .o. If the output of the unit is a struct, you can refer to individual fields using .o.<field name>

As an example, consider this unit which computes a+b and a*b with a latency of one cycle:

struct Output {
    sum: int<9>,
    product: int<16>
}

pipeline(1) add_mul(clk: clock, a: int<8>, b: int<8>) -> Output {
        let result = Output$(
            sum: a+b,
            product: a*b
        );
    reg;
        result
}

A test bench for this module looks like this (this assumes that the Spade code is in src/cocotb_sample.spade. If this is not the case, adjust the # top=cocotb_sample::add_mul part to reflect your module name):

#top = cocotb_sample::add_mul

from cocotb.clock import Clock
from spade import FallingEdge, SpadeExt
from cocotb import cocotb

@cocotb.test()
async def test(dut):
    s = SpadeExt(dut) # Wrap the dut in the Spade wrapper

    # To access unmangled signals as cocotb values (without the spade wrapping) use
    # <signal_name>_i
    # For cocotb functions like the clock generator, we need a cocotb value
    clk = dut.clk_i

    await cocotb.start(Clock(
        clk,
        period=10,
        units='ns'
    ).start())

    s.i.a = "2"
    s.i.b = "3"
    await FallingEdge(clk)
    s.o.sum.assert_eq("5")
    s.o.product.assert_eq("6")

    s.i.a = "3"
    s.i.b = "2"
    await FallingEdge(clk)
    s.o.sum.assert_eq("5")
    s.o.product.assert_eq("6")

    s.i.a = "0"
    s.i.b = "1"
    await FallingEdge(clk)
    s.o.sum.assert_eq("1")
    s.o.product.assert_eq("0")

You can then run the test using swim test or swim t. If you want to run all tests in a specific file, run swim test <pattern>. All files which contain the pattern will be run, for example, swim test abc will run tests in both abc.py and cdeabc.py.

You can also run individual tests using -t <test name> though here, the name has to be exactly the name of the test, not a pattern

For more information on the cocotb api, refer to its documentation

Viewing the waveform

One cool thing about HDL simulation is that it tracks how all signals trace over time, allowing you to see exactly how your circuit behaves. These traces are called waveforms, and stored in a file which you can view with a waveform viewer.

Once all tests are run, Swim will print the result of each test, along with a .vcd file in which the waveform is stored:

...

ok   test/cocotb_sample.py 0/1 failed
 🭼 test ok [build/cocotb_sample_test/cocotb_sample.vcd]

For waveform viewers, we recommend https://surfer-project.org/ which was developed specifically for the Spade project, but you can also use GtkWave if you are already familiar with it.

Once the waveform viewer is installed, you can simply run surfer build/cocotb_sample_test/cocotb_sample.vcd or gtkwave build/cocotb_sample_test/cocotb_sample.vcd.

If you have a relatively modern terminal, Swim also supports clickable links for opening wave files for each test, but it needs an initial automated setup. Just run swim setup-links. Now Swim will print two clickable links, one for surfer and one for gtkwave:

ok   test/cocotb_sample.py 0/1 failed
🭼 test ok [build/cocotb_sample_test/cocotb_sample.vcd ([🏄] [🌊])]

Surfer also supports translation from the raw bit patterns to Spade types which makes debugging much easier. By far the easiest way to get this is with the clickable links mentioned above, but you can also run Surfer with this manually by running

surfer <path-to-vcd> --spade-state build/state.ron --spade-top path::to::top::module

Tips and Tricks

For now, &mut wires can not be read by the Spade API in cocotb. Similarly, tests can not be run on generic units. Therefore, it is often a good idea to define a wrapper function, typically called a harness around your units which use advanced features.

Verilator

C++ source files with the .cpp extension in the testbench_dir will be simulated using Verilator. Like cocotb, these files consist of a set of test cases, but the test cases are defined using macros rather than attributes.

The Spade path to the top module is specified using a comment, i.e.

// top = path::to::module

where the path is relative to the current project.

After that, the Verilog name of the top module must be specified using a #define. Unless you know the details of how Verilator name mangling works, you almost certainly want to specify #[no_mangle] on your unit under test.

The last thing you need to do before defining your tests is to include <verilator_util.hpp>.

After all your test have been defined, end test file with MAIN which defines a main function which is compatible with Swim.

// top=main::main

#define TOP main
#include <verilator_util.hpp>


TEST_CASE(it_works, {
    // Your test code here
    return 0;
})

MAIN

Accessing inputs and outputs

Like the cocotb API, there is a wrapper around Spade types to allow easier interactions with your design.

As an example, consider testing the following code

struct SubStruct {
    b: int<10>,
    c: int<5>,
}

struct SampleOutput {
    a: Option<int<20>>,
    sub: SubStruct
}

#[no_mangle]
fn sample(a: Option<int<20>>, b: int<10>, c: int<5>) -> SampleOutput {
    SampleOutput(a, SubStruct(b, c))
}

In the TEST_CASE macro, you have access to two variables: dut and s. dut is the raw verilator interface around your module which. s is the Spade wrapper which has a field i for its inputs and o for its output.

You can set the value of inputs to your module with s.i->input_name = "<spade expression>", for example:

    s.i->a = "Some(5)";
    s.i->b = "10";
    s.i->c = "5";

Similarly, you can compare the output to a spade expression using s.o == "<spade expression>"

If your unit under test returns a struct, you can also access its fields and sub-fields as fields on the output struct, for example s.o->field->subfield == "<spade expression>".

Finally, to assert that an output value is what you expect, you can use the ASSERT_EQ macro which takes s.o or a subfield, and compares it against a Spade expression. The advantage of using this macro over a C++ assert is that you get a diff print, both with the Spade value and the underlying bits.

For example, tests the fields in our example look like:

    ASSERT_EQ(s.o, "SampleOutput$(a: Some(5), sub: SubStruct$(b: 10, c: 5))");
    ASSERT_EQ(s.o->a, "Some(5)");
    ASSERT_EQ(s.o->sub, "SubStruct$(b: 10, c: 5)");
    ASSERT_EQ(s.o->sub->b, "10");
    ASSERT_EQ(s.o->sub->c, "5");

Clock generation

Clocks need to be ticked manually in verilator. The spade clock type does not allow direct assignment, so the clock needs to be accessed via the Verilator dut. Spade mangles inputs names as <name>_i, so if you want to set clk, you would set dut->clk_i. Or you can mark the clock input with #[no_mangle]

The following code will tick the clock once

    dut->clk_i = 1;
    ctx->timeInc(1);
    dut->eval();
    dut->clk_i = 0;
    ctx->timeInc(1);
    dut->eval();

Since this is so common, it is helpful to define a macro for it:

#define TICK \
    dut->clk_i = 1; \
    ctx->timeInc(1); \
    dut->eval(); \
    dut->clk_i = 0; \
    ctx->timeInc(1); \
    dut->eval();

which can then be used like this:

    s.i->a = "5";
    s.i->b = "10";
    TICK;
    ASSERT_EQ(s.o, "15");

Interfacing with Verilog

It is often desirable to interface with existing Verilog, either instantiating a Verilog module inside a Spade project, or including a Spade module as a component of a larger Verilog project. Both are quite easy to do as long as you have no generics on the Spade side, and no parameters on the Verilog side. Generics and parameters may be supported in the future.

Instantiating a Verilog module

If you have a Verilog module that you want to instantiate from Spade, you need to add a stub for it in your Spade project. This is done by defining a function, entity or pipeline1 but using __builtin__ instead of the body of the unit. For example,

struct Output {
    valid: bool,
    value: int<16>
}
entity external_module(clk: clock, x: int<8>) -> Output __builtin__

While this works, Spade will "mangle" names to avoid namespace collisions and collisions with keywords, so this would in practice look for a module like

module \your_project::your_file::external_module(
    input clk_i,
    input[7:0] x_i,
    output[16:0] output__
);

Changing your module to follow this signature would work, but is not very convenient, the more convenient thing is to add #[no_mangle] to both the module and its inputs in order to use the raw names instead of the mangled names:

#[no_mangle]
entity external_module(
    #[no_mangle] clk: clock,
    #[no_mangle] x: int<8>
) -> Output __builtin__

Now, the resulting Verilog signature is

module external_module(
    input clk_i,
    input[7:0] x_i,
    output[16:0] output__
);

As you can see it still has a single output__ which is both inconvenient if you can't change the signature, and annoying since you need to know how Spade packs structs in order to generate the correct signals. Spade currently does not even define the packing of the structs, so we need to do something about this. The solution is to use mutable wires to generate Verilog ouputs

Changing our module to

#[no_mangle]
entity external_module(
    #[no_mangle] clk: clock,
    #[no_mangle] x: int<8>
    #[mo_mangle] output_valid: &mut bool,
    #[no_mangle] output_value: int<16>,
) __builtin__

results in

module external_module(
    input clk_i,
    input[7:0] x_i,
    output output_valid,
    output[15:0] output_value
);

which is a normal looking Verilog signature.

One downside of this however, is that the interface to this module isn't very Spadey, so typically you will want to define a wrapper around the external module that provides a more Spade-like interface

use std::ports::new_mut_wire;
use std::ports::read_mut_wire;
// Put the wrapper inside a `mod` to allow defining a spade-native unit of the same name.
mod extern {
    #[no_mangle]
    entity external_module(
        #[no_mangle] clk: clock,
        #[no_mangle] x: int<8>
        #[mo_mangle] output_valid: &mut bool,
        #[no_mangle] output_value: int<16>,
    ) __builtin__
}

struct Output {
    valid: bool,
    value: int<16>
}

entity external_module(clk: clock, x: int<8>) -> Output {
    let valid = inst new_mut_wire();
    let value = inst new_mut_wire();
    let _ = inst extern::external_module$(clk, x, output_valid: valid, output_value: value);
    Output {
        valid: inst read_mut_wire(valid),
        value: inst read_mut_wire(value),
    }
}

With this, we have the best of both worlds. A canonical spade-entity on the Spade side, and a canonical Verilog module on the other.

Finally, to use the Verilog module in a Spade project, the Verilog file containing the implementation must be specified in swim.toml under extra_verilog at the root, or extra_verilog in the synthesis section. This takes a list of globs that get synthesized with the rest of the project.

1

See the documentation for units for more details. Most of the time, you probably want to use entity for external Verilog.

Instantiating Spade in a Verilog project

Instantiating Spade in a larger Verilog project is similar to going the other way around as just described. Mark the Spade unit you want to expose as #[no_mangle] on both the unit itself and its inputs. Prefer using &mut instead of returning output values, as that results in a more Verilog-friendly interface.

To get the Verilog code, run swim build, which will generate build/spade.sv which contains all the Verilog code for the Spade project, including your exposed module.

Ws2812b Example

This chapter will guide you through how to build a spade library for the ws2812b RGB led and should serve as a practical example for "real world" Spade usage.

This assumes a bit of familiarity with basic spade concepts, and is written primarily with software people in mind, as such more weight will be put on the FPGA specifics than on spade syntax and concepts.

The chapter starts off with a discussion on how to create a spade project and how that project is laid out. After that, we will discuss the interfaces we want to and need to use, i.e. how to talk to the LEDs, and how to make the driver interface nice to use for other spade code. Finally, we'll go over the implementation of the actual driver.

Creating a Project.

It is strongly advised to use the Swim build tool to write Spade projects. It manages rebuilding the spade compiler, including the standard library and dependencies, testing and synthesis etc.

If you haven't installed swim already, do so by following the installation instructions.

After you have swim installed, we should create a new project. The easiest way to do this is to run swim init --board <fpga name>. To get a list of the boards we currently have templates for, run

swim init --list-boards

which should give you something like

Cloning into '/tmp/swim-templates'...
remote: Enumerating objects: 135, done.
remote: Counting objects: 100% (50/50), done.
remote: Compressing objects: 100% (49/49), done.
remote: Total 135 (delta 11), reused 0 (delta 0), pack-reused 85
Receiving objects: 100% (135/135), 30,73 KiB | 30,73 MiB/s, done.
Resolving deltas: 100% (37/37), done.
[INFO] Available boards:
ecpix5
go-board
icesugar-nano
tinyfpga-bx
ulx3s_85k

If your FPGA board is not on the list, you can also set up your project manually, but that's out of scope for this guide. Have a look at the templates repository for inspiration.

For this project, the exact board isn't super important. I like my ecpix5 so I will use that. Create the project using

swim init --board ecpix5 ws2812b

Note that it is likely that this project, being a library to drive specific hardware should be a library, not a standalone project, it is still useful to initialise it targeting a specific FPGA board in order to test in hardware it later.

Basic project layout

Inside the newly created directory we find the following files:

  • ecpix5.lpf
  • openocd-ecpix5.cfg
  • src
    • main.spade
    • top.v
  • swim.toml

FPGA specific files

The ecpix5.lpf file is a pin mapping file which tells the synthesis tool what physical pins correspond to the inputs and outputs from our top module.

If you are using a ice40 based FPGA, this file is instead a pcf file which has the same purpose but different syntax.

We'll get back to this file when it is time to test on hardware

The openocd-ecpix5.cfg file is a file needed to program the FPGA. It is specific to the ecpix5 programmer and you don't really have to care what it does or why it is needed.

Since spade is a very work in progress language with breaking changes being very common, it's easiest to have each project depend on a specific git version of the compiler. This is handled by swim, which will track a specific compiler version for us.1 The first time we build the project using swim, it will download and compile the compiler.

Since the compilation process takes quite a while the first time you run it, now is a good time to call swim build

The src directory contains our spade source code. Each file is given a unique namespace based on the name, so anything you define inside main.spade will be under the namespace ws2812b::main::<unit name>.

Finally, there is the swim.toml file which describes our project

name = "ws2812b"

[synthesis]
top = "top"
command = "synth_ecp5"

[board]
name = "ecpix-5"
pin_file = "ecpix5.lpf"
config_file = "openocd-ecpix5.cfg"

The name is, as you might expect, the name of your project. If another project depends on your project, this is the namespace at which your project will reside.

The synthesis, pnr, upload, and packing fields tell swim what tools to call to synthesise the project and upload it to the board. Most things can be ignored here, but the top field is worth knowing about, as that is how you specify the top module (roughly equivalent to main in most software languages).

1

You can read more about this in the swim README.

Basic swim usage

Swim has several subcommands which you can use. These commands call their prerequisites so you only have to call the one you actually want to run. I.e. you don't have to call swim build before swim test.

swim build

Compiles your spade code to verilog. The output ends up in build/spade.sv

swim synth, swim pnr

Call the synthesis tool and place and route tool respectively.

swim upload

Build the project and upload it to the board

swim test

Run simulation to test your code. Note that by default, your project does not contain any test benches, so this will complain. We'll write some later in the guide.

Aliases

Most of these commands have aliases that you can use to be lazy and avoid typing.

  • b: build
  • syn: synthesise
  • u: upload
  • t, sim: test

In the next section, we will start discussing how to talk to the LEDs.

LED protocol overview

Now that we are familiar with the project layout, we can start writing the driver for our LEDs. To do so, a good place to start is the datasheet. By reading it we can find out how the protocol works:

The LEDs are chained together, with us talking to the data in pin on the first LED in the chain, and it relaying messages to the rest of the chain automatically.

Data transmission consists of 3 symbols:

  • 0 code
  • 1 code
  • RET code

Each LED has 24 bit color, 8 bits per channel and the transmission order is GRB 1 with the most significant bit first. The first 24 bits of color control the first LED, the next 24 the second and so on, until the RET code is sent at which point data transmission re-starts from the beginning

1

Because apparently standard color orders like RGB is too mainstream

As a more graphical example, a transmission of the color information for a sequence of three LEDs look like this:

| G7..0 | R7..0 | B7..0 | G7..0 | R7..0 | B7..0 | G7..0 | R7..0 | B7..0 | RET |...
|<        LED 1        >|<        LED 2        >|<        LED 2        >|     |< ...

Each color segment is a sequence of 1 or 0 codes depending on the desired color for that led and color channel.

We should also have a look at the waveform of the 0, 1 and RET codes which look like this (see the datasheet for prettier figures):

0 code

------+
      |
      +-----------
| T0H |    T0L   |

I.e. a signal that is High for T0H units of time, followed by Low for T0L units of time

1 code

----------+
          |
          +-------
|   T1H   |  T1L |

I.e. a signal that is High for T1H units of time, followed by Low for T1L units of time. It is very similar to the 0 code, but for the 1 code, the high duration is longer than the low duration.

RET code

The RET code is just a Low signal which lasts for Tret units of time.

NOTE: The datasheet usually refers to this signal as reset and the timing as Treset. In order to make the rest of this text less confusing, we use the name ret throughout, as we already have a FPGA reset signal in our design which has different purposes.

Durations

We'll leave the durations of the signals for now and get back to them when we start implementing things. If you're curious already, have a look at the datasheet.

With the discussion of the external protocol out of the way, the next section will discuss our internal protocol, i.e. what interface we expose to users of our driver.

Driver interface

Now that we know how we should talk to the LEDs, we should also consider how we want the interface to our library to work. Here we have a few options with various trade-offs.

Passing an array around

The most familiar coming from a software world might be for the library to take a copy or a reference to an array containing the values to set the LEDs to. However, this is quite a difficult interface to implement in an FPGA. If we were to copy the LED values, we would need 24 bits per LED to be connected between the driver and user. Those bits would need individual wires, so the number of wires would quickly grow very large.

This interface would look something like

entity ws2812<#N>(clk: clock, rst: bool, to_write: [Color; N]) -> bool {
    // ...
}

"Function" to write single LED

Another option we might be tempted to try is to have an interface where you "call" a function to set a specific LED. This is difficult to do in practice however. In spade, one does not "call" a function, instead you instantiate a block of hardware. One might work around that by passing something like an Option<(Index, Color)> to the driver, which updates the specified LED.

However, this is still not without flaws. First, we can't update a single LED, we need to send colors to all the LEDs before it too, so we'd need to store what the color of the other LEDs are. Second, it takes time to transmit the control signals, so one couldn't send new colors at any rate, the module must be ready to transmit before receiving the next command. This is technically solvable, but there are better options for this particular interface.

Letting the driver read from memory

Passing a reference is slightly more doable in an FPGA. Here, we might give the LED driver a read port to a memory from which it can read the color values at its own pace. This is certainly an option for us to use here, though spade currently doesn't have great support for passing read ports to memories around. Until that is mitigated, we'll look for other options

This might look something like this, but the MemoryPort is not currently supported in spade

entity ws2812<#N>(clk: clock, rst: bool, mem: MemoryPort<Color>, start_addr: int<20>) -> bool {
    // ...
}

For those unfamiliar, the #NumLjds syntax means that the entity is generic over an integer called NumLeds.

In current spade, one would have to write it as

struct Ws2812Out {
    signal: bool,
    read_addr: int<20>,
}
entity ws2812<#NumLeds>(clk: clock, rst: bool, memory_out: Color, start_addr: int<20>) -> Ws2812Out {
    // ...
}

which decouples the read_addr from memory_out, and does not make clear the read delay between them.

Driver owned memory

Another, more spade- and FPGA friendly option is to have the driver itself own a memory where it stores the colors to write, and expose a write port to that memory for instanciators to write new values. This might look as follows:

entity ws2812<#NumLeds>(clk: clock, rst: bool, write_cmd: Option<int<20, Color>>) -> bool {
    // ...
}

Just in time output

Finally, an interface which might be unfamiliar coming from the software world is to have the user generate the color on the fly, i.e. the user provides a translation from LED index to LED color. This is quite a nice setup as it doesn't intrinsically require any memory; if color selection is simple, it can be made on the fly. This interface is best demonstrated graphically

       Control
       signals
          |
          v
  +---------------+
  | State machine |
  +---------------+
          |
          v
+-------------------+
|   User provided   |
| color translation |
+-------------------+
          |
          v
+------------------+
| Output generator |
+------------------+
          |
          V
         LED
       Signals

Here, as driver implementors we are responsible for providing the state machine, whose output would be some signal which says "Right now, we should emit byte B of the color for LED N". We'll represent it by an enum

The color translator translates that into a known color, and the output generator generates the signals that actually drive the led.

In some sense, this interface is the most general. Both the driver owned memory version, as well as the memory read port version can be implemented by plugging the read logic into the translation part. For that reason, we will implement this interface first.

With all that discussion on interfaces out of the way, it is finally time to start implementing things. The next section will introduce the finite state machine, a real work horse in any spade project.

State Machine

Now it is finally time to write some code. The swim template project contains some example code in main.spade, feel free to run swim upload to test it if you'd like. However, for this project, we won't need any of it, so once you are done playing around with it, remove all code from main.spade.

We'll start off by writing the state machine that generates the drive signals for the rest of the circuit. Before we do that though, it is a good idea to think about the input and output signals we want.

For simplicity, the state machine will not take any input control signals, it will start running as soon as the reset signal is turned off, and write data as fast as possible until the end of time.

Output type

The output is a bit more interesting. As stated before, we want the Finite State Machine (FSM) to emit information about what we are currently drawing.

For those unfamiliar, a Finite State Machine is less scary than the words make it seem. It is a way to do computation by describing a series of states and how and when to change between the states.

For example, if we want to build a circuit to toggle an LED whenever a short pulse arrives 1, our FSM would consist of two states: On and Off. If no pulse arrives, the current state remains. If the pulse arrives, we transition from the current state to the opposite state.

It is usually convenient to look at small FSMs graphically, the following figure shows the states and transitions of the pulse example

1

perhaps a pulse from a button, though some extra circuitry would be needed to turn the "short" pulse of a human pressing the button into a pulse that is "short" for an electronics circuit :)

Before we discuss our state machine further, we should consider what output we want it to generate. Initially, we might do something like this:

enum OutputControl<#IndexWidth> {
    /// Currently emitting the RET signal
    Ret,
    /// Currently emitting the specified bit of the color for LED `index`
    Led{index: int<IndexWidth>, bit: int<6>}
}

We make this enum generic over the width of the led indices to not waste bits and allow an arbitrary number of LEDs

The bit field is an int<6> because we want to be able to express 0..24. If spade had better unsigned support, we'd be able to use uint<5> :)

This enum has a few issues though, so let's make some improvements.

First, the data coming out of the color translation block will end up being quite similar to this enum, so we can use generics to share some code. The user will translate the index into a color, so we will allow arbitrary payload instead of that index

enum OutputControl<T> {
    /// Currently emitting the Ret signal
    Ret,
    /// Currently emitting the specified bit of the color for LED `index`
    Led{payload: T, bit: int<6>}
}

This is enough information to write the color translator, but to generate the output, it would be nice to have some more information. Specifically, because this is a time based interface, we could more easily generate the output waveforms if we knew how long we've been emitting the current bit. Let's add that to the enum

enum OutputControl<T> {
    /// Currently emitting the RET signal
    Ret,
    /// Currently emitting the specified bit of the color for LED `index`
    Led{payload: T, bit: int<6>, duration: int<12>}
}

If you are curious, the width of the duration field is 12 to support a counter counting from 0 to 1250. This was chosen because the total duration of a data bit is 1.25 microseconds, which takes 1250 clock cycles at 1 GHz, and we are unlikely to run our FPGA above that frequency. Better generics over clock frequencies is something that might happen down the line

State machine entity

We can finally stop talking about interfaces and write some actual code. Let's start off writing an entity where we can put the logic to generate the OutputControl enum. This entity will be generic over the index width as discussed previously, and will take a number of LEDs to control as a normal parameter.

In practice, it would be a lot nicer to set the number of LEDs at compile time too, but spade generics are not quite there yet.

entity state_gen<#IndexWidth>(
    clk: clock,
    rst: bool,
    num_leds: int<IndexWidth>
) -> OutputControl<int<IndexWidth>> {
    // TODO
}

Let's work on that // TODO next. Recall that when working in spade, we always describe the behaviour of our circuit between one clock cycle and the next. However, we want to implement an interface that is time dependent, so we need to do some thinking. In a high level language, we'd want to do something like


#![allow(unused_variables)]
fn main() {
while true {
    for t in 0..ret_duration {
        output = Ret;
        wait_clock_cycle;
    }

    for i in 0..num_leds {
        for bit in 0..24 {
            for t in 0..bit_duration {
                output = Led(i, bit, t)
                wait_clock_cycle;
            }
        }
    }
}
}

Unfortunately, loops are out of reach, so we will need to encode this logic in some other way. Most of the time, this is done by writing a state machine. The exact method is somewhat situation dependent and takes some practice. To be successful at this task, we have two basic constrains: we need enough information to know what state to jump to at all times, and we need enough information to know what output to generate. In spade, we'll almost always represent the states with an enum

enum State {
    // TODO
}

The RET signal

Let's start off with the first for loop to generate the RET signal. We need to keep track of how long we've been in RET, so we know when to jump over to the output generation loop. A good starting point is therefore a state, with a duration

enum State {
    Ret{duration: int<17>},
    // ...
}

The state_gen will need an instance of the state enum, which is updated at every clock cycle. A perfect use for the reg statement and match expression

entity state_gen<#IndexWidth>(
    clk: clock,
    rst: bool,
    num_leds: int<IndexWidth>
) -> OutputControl<int<IndexWidth>> {
    reg(clk) state reset(rst: State::Ret(0)) = match state {
        // Compute next state here
    };
}

What happened here? We have a register called state which we update by checking the state in the current clock cycle, to build a circuit that gives the state in the next. Since state depends on itself, it needs to be reset back to an initial value when the FPGA, which is why write reset(rst: State::Ret(0)). This will make the circuit send the RET signal to the LEDs when starting up, then operate as normal. We could have started emitting LED values too, but this makes the description easier and gives the LEDs a few microseconds to get up and running during power up.

How do we compute the next state in the Ret state? That depends on how long we have been in Ret already. If that time is longer than the minimum time in Ret, we can start emitting LED data, otherwise we'll stay in the Ret state. We'll write this logic as

entity state_gen<#IndexWidth>(
    clk: clock,
    rst: bool,
    num_leds: int<IndexWidth>
) -> OutputControl<int<IndexWidth>> {
    reg(clk) state reset(rst: State::Ret(0)) = match state {
        State::Ret(duration) => {
            if duration >= Tret {
                // First LED state
            }
            else {
                State::Ret(trunc(duration + 1))
            }
        },
        // ...
    };
}

You may be curious why we need trunc there. That's because spade does not implicitly cast away overflow. duration+1 is 1 bit larger than duration if it overflows. To make it fit back into our state, we truncate the result of the addition, since we know that we have chosen duration to be large enough for it not to be an issue.

Timing

The keen eyed might have noticed Tret there. What is its value? It represents the minimum time that we should emit the ret signal, but duration is in clock cycles. Eventually, Spade might support being generic over clock cycles and allow you to reason about time natively. For now, we need to compute how many clock cycles Tret is manually. This of course depends on the clock frequency, a value which varies between FPGAs. At the time of writing this guide, out of the boards that swim currently supports natively, there are 4 different clock frequencies, so we probably want to be generic over it in order to write a library.

Since we'll need a few more time dependent parameters down the line, we'll define a Timing struct which we pass to the modules, which contains the relevant timings. We might write something like this

struct Timing {
    Tret: int<17>,
    T0h: int<12>,
    T0l: int<12>,
    T1h: int<12>,
    T1l: int<12>,
    bit_time: int<12>,
}

However, now the user needs to know what those implementation dependent times are, which probably requires going to the data sheet. To make their life simpler, let's change it to

struct Timing {
    // 280 microseconds
    us280: int<17>,
    // 0.4 microseconds
    us0_4: int<12>,
    // 0.8 microseconds
    us0_8: int<12>,
    // 0.45 microseconds
    us0_45: int<12>,
    // 0.85 microseconds
    us0_85: int<12>,
    // 1.25 microseconds
    us1_25: int<12>,
}

and update our entity

entity state_gen<#IndexWidth>(
    clk: clock,
    rst: bool,
    num_leds: int<IndexWidth>
    t: Timing,
) -> OutputControl<int<IndexWidth>> {
    let t_ret = t.us280;
    reg(clk) state reset(rst: State::Ret(0)) = match state {
        State::Ret(duration) => {
            if duration >= t_ret {
                // First LED state
            }
            else {
                State::Ret(trunc(duration + 1))
            }
        },
        // TODO: next states
    };
    // TODO: Output
}

NOTE: If you've been following along with a datasheet, for example the first result on duck duck go, or the first result from google you may be confused by why we use 280 microseconds and not 50. It turns out that the manufacturers of the LEDs updated the protocol at some point without updating model numbers or datasheets. this took quite a few hours of debugging when the code worked on old LEDs, but not a new strip.

Bit signals

To generate the bit signals, i.e. the nested for loop in the example above, we need to keep track of 3 things: which LED we're working on, which bit on that LED we're working on, and how long we've been in that state. Essentially 1 variable per loop level. We'll extend the state enum to fit:

enum State<#IndexWidth> {
    Ret{duration: int<17>},
    Led{idx: int<IndexWidth>, bit: int<6>, duration: int<12>}
}

How do we want the logic to work? At the "innermost level", if we aren't done emitting the current bit, we increase the duration by 1. If the duration reaches the bit time, we move on to the next bit, and if we are done with all bits, we move on to the next LED. Finally, if we reached the last LED, we'll go back to the RET state.

In spade, we'll write that as

entity state_gen<#IndexWidth>(
    clk: clock,
    rst: bool,
    num_leds: int<IndexWidth>,
    t: Timing,
) -> OutputControl<int<IndexWidth>> {
    let t_ret = t.us280;
    let t_bit = t.us1_25;
    reg(clk) state reset(rst: State::Ret(0)) = match state {
        State::Ret(duration) => {
            if duration >= t_ret {
                State::Led(0, 0, 0)
            }
            else {
                State::Ret(trunc(duration + 1))
            }
        },
        State::Led$(idx, bit, duration) => {
            if duration == t_bit {
                if bit == 23 {
                    if idx == trunc(num_leds-1) {
                        State::Ret(0)
                    }
                    else {
                        State::Led$(idx: trunc(idx+1), bit: 0, duration: 0)
                    }
                }
                else {
                    State::Led$(idx, bit: trunc(bit+1), duration: 0)
                }
            }
            else {
                State::Led$(idx, bit, duration: trunc(duration + 1))
            }
        },
    };
    // TODO: Output
}

Spade supports passing arguments to units both by position, i.e. argument 1 is passed to parameter 1, 2 to 2 and so on, and also by name. To specify parameters by name, the calling parenthesis are preceded by $, i.e. State::Led$(idx, bit, duration: trunc(duration + 1)) says to pass the variable called idx to the parameter idx, bit to bit, and trunc(duration + 1) to duration. This works the same way as the rust struct initialisation syntax

Finally, generating the output signal can be done by another match statement. Since State and OutputControl are very similar in this case, the resulting match statement is not very complex:

    match state {
        State::Ret(_) => OutputControl::Ret(),
        State::Led$(idx, bit, duration) => OutputControl::Led$(payload: idx, bit, duration)
    }

Putting it all together, we end up with the following code:

enum OutputControl<T> {
    /// Currently emitting the RET signal
    Ret,
    /// Currently emitting the specified bit of the color for LED `index`
    Led{payload: T, bit: int<6>, duration: int<12>}
}

struct Timing {
    // 50 microseconds
    us280: int<17>,
    // 0.4 microseconds
    us0_4: int<12>,
    // 0.8 microseconds
    us0_8: int<12>,
    // 0.45 microseconds
    us0_45: int<12>,
    // 0.85 microseconds
    us0_85: int<12>,
    // 1.25 microseconds
    us1_25: int<12>,
}

enum State<#IndexWidth> {
    Ret{duration: int<17>},
    Led{idx: int<IndexWidth>, bit: int<6>, duration: int<12>}
}

entity state_gen<#IndexWidth>(
    clk: clock,
    rst: bool,
    num_leds: int<IndexWidth>,
    t: Timing,
) -> OutputControl<int<IndexWidth>> {
    let t_ret = t.us280;
    let t_bit = t.us1_25;
    reg(clk) state reset(rst: State::Ret(0)) = match state {
        State::Ret(duration) => {
            if duration >= t_ret {
                State::Led(0, 0, 0)
            }
            else {
                State::Ret(trunc(duration + 1))
            }
        },
        State::Led$(idx, bit, duration) => {
            if duration == t_bit {
                if bit == 23 {
                    if idx == trunc(num_leds-1) {
                        State::Ret(0)
                    }
                    else {
                        State::Led$(idx: trunc(idx+1), bit: 0, duration: 0)
                    }
                }
                else {
                    State::Led$(idx, bit: trunc(bit+1), duration: 0)
                }
            }
            else {
                State::Led$(idx, bit, duration: trunc(duration + 1))
            }
        }
    };
    match state {
        State::Ret(_) => OutputControl::Ret(),
        State::Led$(idx, bit, duration) => OutputControl::Led$(payload: idx, bit, duration)
    }
}

While we hope that the above code will work on the first try, that is rarely the case in practice. The next section will discuss how we can test our design

Testing the state machine

Just like software, testing our code is vital. Unlike software however, we don't have (easy) access to fancy tools like debuggers, printfs or error messages when we run on hardware. Therefore, we usually simulate FPGA designs to make sure they work in simulation in order to avoid painful debugging in hardware.

Currently, writing simulation code in spade is not possible, as the things you want to do in a simulator are quite different to describing hardware. Instead, tests are written in python using the cocotb testing framework.

If you haven't already, refer to the installation instructions to see how to install cocotb.

Setting up tests

To do our testing, we need to do a tiny bit more setup in swim.

To do testing, we need to tell swim where we put our test benches. To do so, create a directory called test

Then edit swim.toml adding a simulation section like so:

[simulation]
testbench_dir = "test"

Inside the test folder we put our test benches in python files. Let's create our first one by creating test/state_gen.py. Each spade test file must start with a comment telling swim which unit is to be tested, the "top module", like so. The path must be a fully namespaced name, and since our module resides in main.spade, it will be main::state_gen

# top=main::state_gen

We'll also add an empty test to that file like this:

# top=main::state_gen
import cocotb
from spade import SpadeExt

@cocotb.test()
async def normal_operation(dut):
    s = SpadeExt(dut)

Each test is annotated by @cocotb.test() and is an async python function which takes a single parameter dut, the Design Under Test.

Running swim test (or swim t for the lazy :)) presents us with the following error1

Error:
   0: In {tb}
   1: main::state_gen is generic which is currently unsupported in test benches

Which is a limitation of the spade python interface. To test our module, we'll need to create a dummy entity without any generic parameters, for now we'll use one with 10 LEDs.

entity state_gen_10(clk: clock, rst: bool, t: Timing) -> OutputControl<int<5>> {
    inst state_gen(clk, rst, 10, t)
}

After updating the top to # top=main::state_gen_10 we can swim test again and we should see a nice PASS (along with some other output which we'll ignore for now)

[INFO] Building spade compiler
    Finished release [optimized] target(s) in 0.04s
[INFO] Built spade compiler
[INFO] build/spade.sv is up to date
[INFO] Building spade-python
    Finished release [optimized] target(s) in 0.04s
[INFO] Built spade-python
     -.--ns INFO     cocotb.gpi                         ..mbed/gpi_embed.cpp:109  in set_program_name_in_venv        Using Python virtual environment interpreter at /home/frans/Documents/spade/ws2812-spade/build/.env/bin/python
     -.--ns INFO     cocotb.gpi                         ../gpi/GpiCommon.cpp:99   in gpi_print_registered_impl       VPI registered
/home/frans/Documents/spade/ws2812-spade/build/spade.sv:177: Warning: Calling system function $value$plusargs() as a task.
/home/frans/Documents/spade/ws2812-spade/build/spade.sv:177:          The functions return value will be ignored.
/home/frans/Documents/spade/ws2812-spade/build/spade.sv:111: Warning: Calling system function $value$plusargs() as a task.
/home/frans/Documents/spade/ws2812-spade/build/spade.sv:111:          The functions return value will be ignored.
     0.00ns INFO     Running on Icarus Verilog version 11.0 (stable)
     0.00ns INFO     Running tests with cocotb v1.6.2 from /home/frans/Documents/spade/ws2812-spade/build/.env/lib/python3.10/site-packages/cocotb
     0.00ns INFO     Seeding Python random module with 1657993983
     0.00ns WARNING  Pytest not found, assertion rewriting will not occur
     0.00ns INFO     Found test state_gen.normal_operation
     0.00ns INFO     running normal_operation (1/1)
state_gen.py.vcd
VCD info: dumpfile state_gen.py.vcd opened for output.
     0.00ns INFO     normal_operation passed
     0.00ns INFO     **************************************************************************************
                     ** TEST                          STATUS  SIM TIME (ns)  REAL TIME (s)  RATIO (ns/s) **
                     **************************************************************************************
                     ** state_gen.normal_operation     PASS           0.00           0.00          4.45  **
                     **************************************************************************************
                     ** TESTS=1 PASS=1 FAIL=0 SKIP=0                  0.00           0.00          0.26  **
                     **************************************************************************************

[INFO] Building vcd translator
    Finished release [optimized] target(s) in 0.04s
[INFO] Built vcd translator
[INFO] Translating types in "./build/state_gen/state_gen.py.vcd"
[INFO] Translated VCD: ./build/state_gen/state_gen.py.translated.vcd
test/state_gen.py: PASS
1

The first time you run swim test, it will set up a python environment with the required libraries which requires compiling a separate part of the spade compiler. Don't be alarmed at the time swim test takes, or the amount of output the first time you run it in a new project.

Writing Some Tests

Now we are ready to actually test our module. All spade test functions start with s = SpadeExt(dut) which creates a nice spade interface around the cocotb functions.

Since our entity is clocked, we need to generate a clock for it. This is done by starting a cocotb clock task like this. The exact clock frequency is not really important here, it only decides the mapping between simulation time and real time.

# import the clock generator
from cocotb.clock import Clock

# ...

    clk = dut.clk_i
    await cocotb.start(Clock(clk, 1, units='ns').start())

The design also takes a reset signal which we need to set to get our initial state defined. If we forget to do this, most of the signals will be undefined.

We can access the input ports of our design using s.i.<input_name> and give them values by assigning strings containing spade expressions to them. The following code sets the reset signal to true:

s.i.rst = "true"

The s.i interface does not work well with cocotb built in functions like Clock You can access the raw verilog input ports on the dut via dut.<name>_i as above which is nice if you want to pass them to special cocotb functions like Clock. However, most of the time you should use the spade interface since that doesn't require you to know the spade internal representation of types.

For our design to start running, we need to take it out of reset again, you might think that we can just add another line s.i.rst = false. However, this would give the design no time to see the change in reset. Instead, we need to let the simulation step forward a bit. The easiest way to do that is to let it step forward one clock cycle, which we do by waiting until the next time the clock goes from 1 to 0

# import trigger
from cocotb.triggers import FallingEdge

# ...

    await FallingEdge(clk)
    s.i.rst = "false"

This will create a waveform that looks like this

     ---+   +---+
clk:    |   |   |
        +---+   +---...

     ---+
rst:    |
        +-----------...

In order to let the circuit catch up to the fact that the reset has been turned off, we'll advance the simulation another tiny time step (1 picosecond):

# import timer
from cocotb.triggers import Timer

# ...

    await Timer(1, units='ps')

You can find more things to wait for in the cocotb documentation for triggers.

Now we can do our first test, ensuring that the initial output of the circuit is RET. We can access the output of our dut with s.o, and run assertions on it like this:

s.o.assert_eq("OutputControl::Ret()")

If you return a struct from a unit, you can access them as normal python fields on the s.o field. For example s.o.x.y.assert_eq(...)

Our test file now looks like this:

# top=main::state_gen_10

from spade import SpadeExt

import cocotb
from cocotb.clock import Clock
from cocotb.triggers import FallingEdge, Timer

@cocotb.test()
async def normal_operation(dut):
    s = SpadeExt(dut)

    clk = dut.clk_i
    await cocotb.start(Clock(clk, 1, units='ns').start())

    s.i.rst = "true"
    await FallingEdge(clk)
    s.i.rst = "false"

    await Timer(1, units='ps')
    s.o.assert_eq("OutputControl::Ret()")

and calling swim test should tell us that all our assertions passed.

A failing test

Next, we may want to ensure that we output Ret in the next clock cycle as well. So, we'll advance the clock and assert that.

Changes to our state happens on the rising edge of clocks, so I prefer to do my assertions on the falling edge. That way I don't have to worry about if values have or have not changed right at the RisingEdge.

    await FallingEdge(clk)
    s.o.assert_eq("OutputControl::Ret()")

Calling swim test results in the following output:

...
VCD info: dumpfile state_gen.py.vcd opened for output.
 1.50ns INFO     normal_operation failed
                 Traceback (most recent call last):
                   File "/home/frans/Documents/spade/ws2812-spade/build/state_gen/state_gen.py", line 22, in normal_operation
                     s.o.assert_eq("OutputControl::Ret()")
                   File "/home/frans/Documents/spade/ws2812-spade/spade/spade-python/spade/__init__.py", line 75, in assert_eq
                     assert False, message
                 AssertionError:
                 Assertion failed
                     expected: OutputControl::Ret()
                          got: UNDEF

                    verilog (0XXXXXXXXXXXXXXXXXXXXXXX != xxxxxxxxxxxxxxxxxxxxxxxx)

...

[INFO] Building vcd translator
    Finished release [optimized] target(s) in 0.04s
[INFO] Built vcd translator
[INFO] Translating types in "build/state_gen/state_gen.vcd"
[INFO] Translated VCD: build/state_gen/state_gen.translated.vcd
test/state_gen.py: FAIL [build/state_gen/state_gen.translated.vcd]
	Failed test cases:
	normal_operation

Oh no, something went wrong, why? To debug our tests, the best method by far is to look at the wave dump. It contains the value of all the signals in the design over time and can give plenty of debug information. To see it, we need to install a vcd viewer, and the defacto standard is gtkwave.

Swim translates Verilog values in the wave dump back into spade files and stores the result in a new vcd file which is printed along with the failing tests:

test/state_gen.py: FAIL [build/state_gen/state_gen.translated.vcd]

Let's open build/state_gen/state_gen.translated.vcd in gtkwave:

gtkwave build/state_gen/state_gen.translated.vcd

This should open a window that looks something like this:

The black portion shows the value of the signals we select over time. The left pane contains a list of the units in our design, in this case e_proj_main_state_gen_10. This is the verilog name of our module main::state_gen_10. If you select it, the signal list below will be populated by all the values in that module. In this case, it is just a wrapper around the actual design state_gen, so expand the module and select the submodule. This should give you a lot more signals

Now we have lots of signals to play with! Broadly, we can group them into several categories. Some signals start with p_. These contain the spade value of the corresponding signal, for example p_clk_n... is a spade value, and clk_n... is the raw verilog bits.

Names on the form _e_<numbers> and p_e_<numbers> are subexpressions that are not named in the spade program. Unless you're debugging the compiler, you can ignore those.

Names on the form <name>_n<numbers> and p_<name>_n<numbers> are values which are named in your spade code. These are the values you will actually want to look at

Finally, there are some signals called <name>_i. These are input input values. The spade translation does not translate those, so it is better to look at the corresponding <name>_n<numbers> signals.

To add a signal to the waveform window, double click it. To debug this value, we'll want to look at a few signals clk, rst, state and t, so go ahead and add those to the wave view

Here we get quite a bit of information. We see that our state is defined until the first clock cycle after reset. We also see that all fields of t, our timing struct is "HIGHIMP". The name is a bit confusing, but this is caused by us forgetting to set that parameter.

Going back to the spade code, to compute the next state in Ret, we check if the duration we've been in Ret so far is greater than t_ret. However, we haven't set t, so we are essentially comparing duration to t_ret, which is undefined, resulting in another undefined value.

Spade tries to do its best to avoid undefined values, it is certainly harder to write undefined values in spade than in verilog. However, when forgetting to specify inputs, and when working with memories, they can pop up.

Let's specify the timings to fix this issue. Again, exact timing here isn't important, we'll set some values that make testing possible:

    s.i.t = """Timing$(
        us280: 28,
        us0_4: 4,
        us0_8: 8,
        us0_45: 4,
        us0_85: 8,
        us1_25: 12,
    )"""

    await FallingEdge(clk)
    s.o.assert_eq("OutputControl::Ret()")

With that change, our assertions pass.

More tests

Now we can get to testing the rest of the design. Since our state space is quite small in this case, we can ensure that all state transitions happen as they should. Since this is python, we can write things like loop, helper functions etc.

First, let's ensure that we stay in Ret for the specified amount of time, i.e. us280 clock cycles:

    s.i.t = """Timing$(
        us280: 28,
        us0_4: 4,
        us0_8: 8,
        us0_45: 4,
        us0_85: 8,
        us1_25: 12,
    )"""

    for i in range(0, 28):
        await FallingEdge(clk)
        s.o.assert_eq("OutputControl::Ret()")

After that, we should be emitting the value of the first LED. Here we can write a function to check a whole LED output, since we'll do that quite a few times


async def check_led(clk, s, index):
    # Each bit of the LED should be emitted
    for b in range(0, 24):
        # And each duration from 0 to us1_25 in each bit
        # For simulation performance, we'll just check the first and last bit explicitly
        await FallingEdge(clk)
        s.o.assert_eq(f"OutputControl::Led$(payload: {index}, bit: {b}, duration: 0)")
        for d in range(0, 5):
            await FallingEdge(clk)
        s.o.assert_eq(f"OutputControl::Led$(payload: {index}, bit: {b}, duration: 5)")

We can now test all our LEDs by calling it in a loop, and finally ensure that we go back to the ret state at the right time. The final test bench looks like this:

# top=main::state_gen_10

from spade import SpadeExt

import cocotb
from cocotb.clock import Clock
from cocotb.triggers import FallingEdge, Timer


async def check_led(clk, s, index):
    # Each bit of the LED should be emitted
    for b in range(0, 24):
        # And each duration from 0 to us1_25 in each bit
        # For simulation performance, we'll just check the first and last bit explicitly
        await FallingEdge(clk)
        s.o.assert_eq(f"OutputControl::Led$(payload: {index}, bit: {b}, duration: 0)")
        for d in range(0, 5):
            await FallingEdge(clk)
        s.o.assert_eq(f"OutputControl::Led$(payload: {index}, bit: {b}, duration: 5)")

@cocotb.test()
async def normal_operation(dut):
    s = SpadeExt(dut)

    clk = dut.clk_i
    await cocotb.start(Clock(clk, 1, units='ns').start())

    s.i.rst = "true"
    await FallingEdge(clk)
    s.i.rst = "false"

    await Timer(1, units='ps')
    s.o.assert_eq("OutputControl::Ret()")

    s.i.t = """Timing$(
        us280: 28,
        us0_4: 4,
        us0_8: 8,
        us0_45: 4,
        us0_85: 8,
        us1_25: 12,
    )"""

    for i in range(0, 28):
        await FallingEdge(clk)
        s.o.assert_eq("OutputControl::Ret()")

    # Check all 10 leds
    for i in range(0, 10):
        await check_led(clk, s, i)

    # Ensure we get back to the ret state
    await FallingEdge(clk)
    s.o.assert_eq("OutputControl::Ret()")

Running it gives us another assertion error:

VCD info: dumpfile state_gen.py.vcd opened for output.
    28.50ns INFO     normal_operation failed
                     Traceback (most recent call last):
                       File "/home/frans/Documents/spade/ws2812-spade/build/state_gen/state_gen.py", line 44, in normal_operation
                         await check_led(clk, s, i)
                       File "/home/frans/Documents/spade/ws2812-spade/build/state_gen/state_gen.py", line 13, in check_led
                         s.o.assert_eq(f"OutputControl::Led$(payload: {index}, bit: {b}, duration: {d})")
                       File "/home/frans/Documents/spade/ws2812-spade/spade/spade-python/spade/__init__.py", line 75, in assert_eq
                         assert False, message
                     AssertionError:
                     Assertion failed
                     	 expected: OutputControl::Led$(payload: 0, bit: 1, duration: 0)
                     	      got: proj::main::OutputControl::Led(0,0,12)

                     	verilog (100000000001000000000000 != 100000000000000000001100)
    28.50ns INFO     **************************************************************************************
                     ** TEST                          STATUS  SIM TIME (ns)  REAL TIME (s)  RATIO (ns/s) **
                     **************************************************************************************
                     ** state_gen.normal_operation     FAIL          28.50           0.06        461.47  **
                     **************************************************************************************
                     ** TESTS=1 PASS=0 FAIL=1 SKIP=0                 28.50           0.07        432.88  **
                     **************************************************************************************

[INFO] Building vcd translator
    Finished release [optimized] target(s) in 0.04s
[INFO] Built vcd translator
[INFO] Translating types in "./build/state_gen/state_gen.py.vcd"
[INFO] Translated VCD: ./build/state_gen/state_gen.py.translated.vcd
test/state_gen.py: FAIL [./build/state_gen/state_gen.py.translated.vcd]
	Failed test cases:
	normal_operation

Try to see if you can figure out what happened. Looking at the waves can be helpful, but in this case it might be enough to look at what states it transitioned to.

If you can't figure it out, jump to the next section for the answer

Output Generation

First of all, the cause of the bug mentioned in the end of the last chapter was an incorrect equality check of the duration when transitioning between states. It should be

if duration == trunc(t_bit-1) {

instead of

if duration == t_bit {

Now that our state machine works, we have done most of the heavy lifting. We still need to translate our control signal into an actual LED output, which is what we'll work on next.

Since this will require no internal state, and is fairly simple logic we'll represent it as a function. We'll also represent color as a struct with r, g and b values. The output is a single bool, the actual control signal to be passed to the LEDs.

struct Color {
    r: int<8>,
    g: int<8>,
    b: int<8>
}

fn output_gen(control: OutputControl<Color>, t: Timing) -> bool {
    // TODO
}

The ret output is easy, it is simply a low signal. The 0 and 1 signals are a bit more complex. The output should be 1 initially, and then transition to 0 at t0l or t1l depending on if the current bit is a 0 or a 1.

The OutputControl::Led has information about which of the 24 bits should be emitted. To translate that into a bit value, we'll concatenate the color channels, and "index" the correct bit. (Currently, Spade does not support bit indexing, so we'll extract the bits using shifts and masks instead)

This logic can be written as follows:

struct Color {
    r: int<8>,
    g: int<8>,
    b: int<8>
}

fn output_gen(control: OutputControl<Color>, t: Timing) -> bool {
    let t0h = t.us0_4;
    let t1h = t.us0_8;
    match control {
        OutputControl::Ret => false,
        OutputControl::Led$(payload: color, bit, duration) => {
            let color_concat = (color.g `concat` color.r `concat` color.b);
            let val = ((color_concat >> sext((23-bit))) & 1) == 1;
            let step_time = if val {t1h} else {t0h};
            if duration > step_time {
                false
            }
            else {
                true
            }
        }
    }
}

Testing

Again, it is good practice to test the module. Testing it is very similar to the state machine, except here we don't have a clock. Instead, we'll set a signal value, advance the simulation by a tiny time step, and assert the output. Here is an example of the test bench. Feel free to extend it with more tests that you think are reasonable. Here it might also be helpful to define some helper functions which check that a specific input gives a specific waveform, for example.

# top=main::output_gen

from spade import *

@cocotb.test()
async def ret_works(dut):
    s = SpadeExt(dut)

    s.i.t = """Timing$(
        us280: 2800,
        us0_4: 40,
        us0_8: 80,
        us0_45: 45,
        us0_85: 85,
        us1_25: 125,
    )"""

    s.i.control = "OutputControl::Ret()"
    await Timer(1, units='ps')
    s.o.assert_eq("false")



@cocotb.test()
async def one_at_bit_0(dut):
    s = SpadeExt(dut)

    s.i.t = """Timing$(
        us280: 2800,
        us0_4: 40,
        us0_8: 80,
        us0_45: 45,
        us0_85: 85,
        us1_25: 125,
    )"""

    # Sending 1 @ bit 0, time 0
    s.i.control = "OutputControl::Led(Color$(g: 0b1000_0000, r: 0, b: 0), 0, 0)"
    await Timer(1, units='ps')
    s.o.assert_eq("true")

    # Sending 1 @ bit 0, time 40
    s.i.control = "OutputControl::Led(Color$(g: 0b1000_0000, r: 0, b: 0), 0, 40)"
    await Timer(1, units='ps')
    s.o.assert_eq("true")

    # Sending 1 @ bit 0, time 80
    s.i.control = "OutputControl::Led(Color$(g: 0b1000_0000, r: 0, b: 0), 0, 80)"
    await Timer(1, units='ps')
    s.o.assert_eq("true")

    # Sending 1 @ bit 0, time 81
    s.i.control = "OutputControl::Led(Color$(g: 0b1000_0000, r: 0, b: 0), 0, 81)"
    await Timer(1, units='ps')
    s.o.assert_eq("false")

If you want to see a more fleshed out test test, have a look at https://gitlab.com/TheZoq2/ws2812-spade/-/blob/e3ede5d50abf176f0ea5f0dcf6bfdcfb8b2228d8/test/output_gen.py.

With our tests now passing, we can finally run the code in hardware, which we will discuss in the next and final section of this chapter.

Testing in hardware

We are finally at a point where we think the code is correct, and all the pieces are implemented. It's time to test it on hardware.

To do so, we need to set up a demo entity which instanciates the state and output generators, and selects a nice color for them. We'll do this in a separate file, called src/hw_test.spade

use lib::main::state_gen;
use lib::main::output_gen;
use lib::main::OutputControl;
use lib::main::Timing;
use lib::main::Color;

#[no_mangle]
entity demo(#[no_mangle] clk: clock, #[no_mangle] pmod0: &mut int<6>) {
    reg(clk) rst initial(true) = false;

    // Our target FPGA, the ecpix5 has a 100 MHz clock.
    let t = Timing$(
        us280: 28000,
        us0_4: 40,
        us0_8: 80,
        us0_45: 45,
        us0_85: 85,
        us1_25: 125,
    );
    let ctrl: OutputControl<int<4>> = inst state_gen(clk, rst, 4, t);

    reg(clk) timer: int<32> reset(rst: 0) = if timer > 100_000_000 {
        0
    }
    else {
        trunc(timer+1)
    };

    reg(clk) offset: int<2> reset(rst: 0) = if timer == 0 {
        trunc(offset+1)
    }
    else {
        offset
    };

    let brightness = 64;
    let colors = [
        Color(brightness, 0, 0),
        Color(0, brightness, 0),
        Color(0, 0, brightness),
        Color(0, brightness, brightness),
    ];

    let with_color = match ctrl {
        OutputControl::Ret => OutputControl::Ret(),
        OutputControl::Led$(payload: led_num, bit, duration) => {
            let led_num = trunc(led_num + sext(offset));
            OutputControl::Led$(payload: colors[led_num], bit, duration)
        },
    };

    let pin = output_gen(with_color, t);

    set pmod0 = if pin {0b1} else {0};
}

There is not much going on here. Since we're in a different file, we need to include the stuff defined in the other file. lib refers to the library we are currently building, and since our code is in main.spade, the items are put in the main namespace

Since our top module, demo, is going to connect to the external world, we'll mark both it and its parameters as #[no_mangle]. This tells the spade compiler to name things exactly what they are called in the Spade code. The downside of this is that we might collide with Verilog keywords, and the module demo will not have a namespaced name.

For the output, we also use a &mut int<6>. &mut is a mutable wire, i.e. a wire where we can set a value using set. It is an int<6> because the IO port pmod0 on the ecpix5 board we've been using as an example is 6 bits wide. The physical pins pmod0 is mapped to is specified in the lpf file.

The line reg(clk) rst initial(true) = false; generates a reset signal that is active the first clock cycle after the FPGA has started.

To generate the output, we create our timing struct, this time with correct timings for the 100 MHz FPGA we're targeting. We use an array to look up color values for each of the LEDs we're going to test, and output those signals.

Then we instantiate everything, and finally set the output pin to the resulting value. Here the LED strip is connected to the first pin of pmod0

We also need to tell the synthesis tool what entity should be our top module; to do so, change the synthesis.top value in swim.toml to demo

[synthesis]
top = "demo"

With all that done, we can run swim upload, and look at our new RGB LEDs.

The pattern is static and boring at the moment, so this is a great opportunity to play around a bit and make the LEDs do something more interesting!

All the code for this project can be found at https://gitlab.com/TheZoq2/ws2812-spade

Language Reference

This chapter is a reference for individual features in the language.

Items

Anything that appears at the top level of a Spade file is an item. This includes units, types and (sub)modules etc..

As a user, you will rarely encounter the term Item, though it might appear in parser errors if you write something unexpected at the top level of a file.

Units

Units are the basic building blocks of a Spade project, they correspond to modules in Verilog, and entities in VHDL. Units come in three flavors: functions, pipelines and entities.

Functions

Functions are combinational circuits (or pure, in software terms), that is they have no internal state, and can not read or set mutable wires.

Pipelines

Pipelines have a specified delay between input and output, and have explicit staging statements.

Entities

Finally, entities are the most general units, they can have state, and the input-output delay is arbitrary. They therefore have roughly the same programming model as VHDL and Verilog.

Type Declarations

Struct

struct declaration include a name, optional generic arguments and a list of fields. The fields in turn have a name and a type which may use the generic arguments.

struct Empty {}

struct NonGeneric {
    field_a: int<8>,
    field_b: bool
}

struct Generic<T> {
    field_a: T,
    field_b: bool
}

Enum

enum declarations also include a name and optional generic arguments. Their body consists of a list of variants. Each variant in turn has a name, and an optional list of fields

enum Enum {
    EmptyVariant,
    OneField{val: int<8>}
    TwoFields{val1: bool, val2: bool}
}

enum GenericEnum<T> {
    EmptyVariant,
    OneField{val: T}
}

Statements

The body of any unit, or block is a list of statements followed by a resulting expression. Statements can declare things local to the block and contain expressions to be evaluated

Let bindings

Let bindings bind a pattern to a value.

Those not used to bindings and patterns can view a let binding as assigning a value to a variable.

The pattern has to be an irrefutable pattern

If the type specification is omitted, the type is inferred.

Syntax

let pattern [: type specification] = expression ;

Examples

Binding a value to a variable

let a = some_value;

Binding a value to the result of an if expression

let a = if x {0} else {2};

Unpacking a tuple

let (a, b) = some_value;

Unpacking a struct with an explicit type signature

let Struct$(a, b): Struct<int<8>> = some_value;

Registers

Free-standing (i.e. non-pipelining registers) are defined using reg(clk) ... The register definition is quite complex and includes

  • The clock signal which triggers an update
  • A pattern to bind the current value of the register to. It must be irrefutable
  • An optional type specification. Like let bindings, the type is inferred if the type signature is omitted
  • An optional reset consisting of a reset trigger and a reset value. Whenever the reset trigger is true the value of the register is asynchronously set to the reset value1
  • An expression which gives new value

On the rising edge of the clock signal, the value of the register is updated to the value of the new value. The new value expression can include variables from the register itself.

Syntax

reg( clock: expression ) pattern [: type specification] [reset( reset trigger: expression : reset value expression)] = new value: expression ;

Examples

A register which counts from -128 to 127 (Note that because no initial value is specified, this will be undefined in simulation):

reg(clk) value: int<8> = trunc(value + 1);

A register which counts from 0 to 200 (inclusive) and is reset to 0 by rst:

reg(clk) value reset(rst: 0) =
    if value == 200 {
        0
    } else {
        trunc(value + 1)
    };

Pipeline stage markers

Stage markers (reg;) are used in pipelines to specify where pipeline registers should be inserted. After a reg statement, all variables above the statement will be put in registers and any reference to those variables refer to the registered version.

Syntax

Repeated

In cases where more than one stage should be inserted without any new statements in between, there is a shorthand syntax:

reg * n`

where n is an integer. This is compiled into n simple reg statements, i.e.

reg * 3;

is the same as

reg;
reg;
reg;

Conditioned

A condition for the registers to accept values can also be specified in square brackets

reg[condition]

The semantics of this are explained in the section on dynamic pipelines

Pipeline stage labels

Pipeline stages can be given names to refer to them from other stages. This is done using 'name.

  'first
  let x = ...;
reg;

To refer to a named stage, use a []

Set

Set the value of a mutable wire to the specified value.

set wire = value;

Set statements can only appear at the top block of a unit. This might be surprising as you would expect to be able to write


#![allow(unused_variables)]
fn main() {
if condition {
  set wire = value;
}
}

However, this is not well-defined in hardware because the wire needs some value, but no value is specified if condition does not hold. This particular point isn't true if an else branch is also specified, but the exact hardware that gets generated from imperative code like this is not obvious, particularly with more nesting.

Therefore, if you want to write

if condition {
  set wire = on_true;
} else {
  set wire = on_false
}

you should move the set statement outside to make it unconditional, i.e.

set wire =
  if condition {
    on_true
  } else {
    on_false
  }

Syntax

set expression = expression;

Assert

Takes a boolean condition and evaluates it, raising a runtime error in simulation if it ever evaluates to false. In synthesis, this is ignored

assert this_should_be_0 == 0;

NOTE: Assert statements are currently not supported for synthesis with Verilator, only with Icarus.

Comptime

TODO

Real world example

Expressions

An expression is anything that has a value. Like most languages this includes things like integers literals, instantiations and operators. However, unlike the languages you may be used to, almost everything in Spade is an expression and has a value, for example if-expression and match-blocks.

This means, among other things, that you can assign the 'result' of an if-expression to a variable:

let a = if choose_b {
    b
}
else {
    c
};

Blocks

A block is an expression which can contain sub-statements. They are delimited by {}, contain zero or more statements and usually end with an expression for the whole block's value.

let a = {
    let partial_result = ...; // Bind a partial result to a variable

    // 'return' the result of compute_on as the result of the block
    compute_on(partial_result)
}

Variables defined inside blocks are only visible in the block. For example, you cannot use partial_result outside the block above.

Blocks are required in places like bodies of if-expressions and functions, but can be used in any place where an expression is expected.

if-expressions

Syntax

if expression block else block

The if-expression looks a lot like an if-statement in languages you may be used to, but unlike most languages where if is used to conditionally do something, in Spade, it is used to select values.

For example, the following function returns a if select_a is true, otherwise it returns b.

fn select(select_a: bool, a: int<8>, b: int<8>) -> int<8> {
    if select_a {
        a
    } else {
        b
    }
}

This code makes heavy use of blocks. The body of the function, as well as each if-branch is a block.

In traditional hardware description languages, this would instead look like

fn select(select_a: bool, a: int<8>, b: int<8>) -> int<8> {
    var result;
    if select_a {
        result = a;
    } else {
        result = b;
    }
    return result
}

but the Spade version is much closer to the actual hardware that is generated. Hardware in general does not support conditional execution, it will evaluate both branches and select the result.

match-expression

Syntax

match expression { pattern => expression , ... }

The match-expression is used to select a value based on the value of a single expression. It is similar to case statements in many languages, but supports pattern-matching which allows you to bind sub-values to variables. Typically, match statements are used on enum values:

enum MaybeByte {
    Some{value: uint<8>},
    None
}

fn byte_or_zero(in: MaybeByte) -> uint<8> {
    match in {
        // Bind the inner value to a new variable and return it
        MaybeByte::Some(value) => value,
        MaybeByte::None => 0,
    }
}

but they can also be used on any values

If more than one pattern matches the value, the first pattern will be selected.

A match statement must cover all possible values of the matched expression. If this is not the case, the compiler emits an error.

Instantiation

The three kinds of units are instantiated in different ways in order to highlight to readers of the code what might happen beyond an instantiation. For example if you see a function instantiation, you know that there will be no state or other weird behavior behind the instantiation.

The following syntax is used to instantiate the different kinds of units:

  • Functions: unit()
  • Entities: inst unit()
  • Pipelines inst(<depth>) unit(). The depth is the depth of the pipeline

Instantiation rules

Functions can be instantiated anywhere. Entities and pipelines can only be instantiated in entities or pipelines.

In addition, pipelines instantiated in other pipelines check the delay to make sure that values are ready before they are readable. For example,

    let x = inst(3) subpipe();
    let y = function();
reg;
    read(x); // Compilation error. x takes 3 cycles to compute, but is read after 1
    read(y); // Allowed, function is pure so its output is available immeadietly
reg * 2;
    // Allowed, x has 3 stages internally, this will be the first value out of the pipeline
    read(x)

Array Indexing

Arrays can be indexed using []. Indices can either be single runtime integers such as [i], or compile-time ranges, such as [10:15]. Arrays are written and indexed as most software languages: the leftmost array element is at index 0.

For example, [a, b, c][0:2] returns a new array [a, b]

Single element indexing

Non-range indices can be runtime integers. The size of the index is the smallest power of two that can represent the size of the array. However, if the array size is not an even power of two, indexing outside the range causes undefined behavior.

Range indexing

The indices for range indexing can only be raw integers, i.e. not runtime values. The leftmost, i.e. beginning of the range is included, and the end of the range is exclusive. For example, a[0:1] creates an array with a single element containing the first element of a.

Examples

let array = [10, 11, 12, 13, 14];

let _ = array[0]; // 10
let _ = array[1]; // 11
let _ = array[2]; // 12
let _ = array[5u]; // Out of bounds access (array length is 5), result is undefined

let _ = array[0:1]; // [10]
let _ = array[1:3]; // [11, 12]
let _ = array[0:5]; // [10, 11, 12, 13, 14]

Tuple indexing

Tuples can also be indexed, though tuple indexing uses #, for example tup#0 for the leftmost tuple value. Tuple indices can only be known at compile time

Stage references

TODO

Patterns

Paterns are used to bind values to variables, and as 'conditions' in match-expressions. Patterns match a set of values, and bind (essentially assigns) a set of partial values to variables.

Name patterns

The simplest pattern is a variable name, like x. It matches all values, and binds the value to the name, x in this case.

Literal patterns

Integers and booleans can be matched on literals of their type. For example, true only matches booleans that are true and 10 only matches integers whose value is 10. Literal patterns do not bind any variables.

Tuple patterns

Another simple pattern is the tuple-pattern. It matches tuples of a specific length, and binds all elements of the tuples to sub-patterns. All patterns can be nested

For example

let ((a, b), c) = ((1, 2), 3);

will result in a=1, b=2 and c=3.

If parts of a tuple pattern are conditional, the pattern will only match if the subpatterns do. For example,

match (x, y) {
    (true, _) => true,
    _ => false,
}

will only return true if x is true, and false otherwise

Struct and enum patterns

Named patterns are used to match structs and enum variants. They consist of the name of the type or variant, followed by an argument list if the type has arguments.

Argument lists can be positional: () or named: $(). In a positional argument list, the fields of the type are matched based on the order of the fields. In a named list, patterns are instead bound by name, either field_name: pattern or just field_name which binds a new local variable field_name to field. Argument matching in patterns works the same way as in argument lists during instantiation

This is best shown by examples

struct S {
    x: int<8>,
    y: int<8>,
}

// Positional pattern, binds `a` to the value of `x` and `b` to the value of `y`
S(a, b)
// Named pattern with no shorthand. The whole pattern matches if the `y` field is `0`
// in which case `a` will be bound to the value of `x`
S$(y: 0, x: a)
// Shorthand named. This binds a local variable `y` to the value of the field `y`. The field `x` is ignored.
S$(y, x: _)

enum variants work the same way, but only match the enum of the specified name. For example

enum E {
    A,
    B{val: int<8>}
}

match e {
    E::A => {},
    E::B(0) => {},
    E::B(val) => {}
}

Wildcard

The wildcard pattern _. It matches all values but does not bind the value to any variable. It is useful as a catch-all in match blocks

For example, if we want to do something special for 0 and 1, but don't care about other values we might write:

match integer {
    0 => {},
    1 => {},
    _ => {}
}

Refutability

A pattern which matches all values of its type is irrefutable while one which only matches conditionally is refutable.

For example, a pattern unpacking a tuple is irrefutable because all values of type (T, Y) will match (a, b)

let tuple: (T, Y) = ...;
match tuple {
    (a, b) => {...}
}

while one which matches an enum variant is refutable because the None option will not match

enum Option<T> {
    Some{val: T},
    None,
}
match x {
    Some(x) => {...} // refutable: None not covered
    ...
}

Full documentation of the type system is yet to be written.

Primitive Types

These are the types built into the Spade language which aren't defined in the standard library.

bool

Generics

In a lot of cases, you want code to be generic over many different types, therefore both types and units support generic parameters.

Defining generics

Units and types which are generic have their generic parameters specified inside angle brackets (<>) after the name. The generics can be either integers denoted by #, or types which do not have # sign. In the body of the generic item, the generic types are referred to by their names

For example a struct storing an array of arbitrary length and type is defined as

struct ContainsArray<T, #N> {
    inner: [T, N]
}

Using generics

When specifying generic parameters, angle brackets (<>) are also used. For example, a function which takes a ContainsArray with 5 8-bit integers is defined as

fn takes_array(a: ContainsArray<int<8>, 5>) {
    ...
}

Ports and wires

If you prefer documentation in video form there is a talk available on this topic.

Most types in Spade represent values. However, in digital design it is sometimes beneficial to also reason about connections between modules, ports. Spade separates values from ports because the semantics are a bit different.

The basic building block of ports are immutable wires, denoted by &T, and mutable wires: &mut T.

Because they represent connections rather than values, ports are not delayed by reg statements in pipelines, and cannot be stored in registers.

Immutable wires

An immutable wire can be read using the dereference operator *. Apart from that, they behave very similar to normal values.

Mutable wires

Mutable wires are used to communicate values in the opposite direction than what is usually done. Entities usually receive values from its inputs and produce values from its outputs. On the other hand, an entity which receives a mutable wire can set the value of that wire, and an entity that returns a mutable wire will be able to read values from that wire.

The primary use case for mutable wires is to group related signals together. As an example consider a memory module which takes two addresses and returns the content of the memory at those addresses. Without mutable wires, It looks like this:

entity memory(addr0: Addr, addr1: Addr) -> (Data, Data) {...}

as you can see, there is nothing here that says which address is associated with which output value.

Similar problems exist in the module which uses the memory value, it returns an address and receives data as one of its inputs, but the link between them is not at all obvious:

entity consumer(data: Data) -> Addr {...}

Additionally, if the addres and data are used deep within a module hierarchy, one has to propagate the address and return value manually via the return value of everything in the hierarchy.

With wires, the memory and consumer would instead look like this:

entity memory() -> ((&mut Addr, &Data), (&mut Addr, &Data)) {...}

entity consumer(memory_port: (&mut Addr, &Data));

the whole memory port, here modelled as a tuple, is passed around as a single thing.

Mutable wires must be set

One important property of mutable wires is that once you have access to one, you must make sure that it receives a value. You can either do that by setting the value using the set-statement or by passing the mutable value along to another unit which is then responsible for setting the value. You also are not allowed to set a mutable wire more than once. Doing so would cause ambiguity in which value should actually be connected, since it is essentially a physical wire.

Luckily, the compiler checks both of these properties.

In cases where you want to conditionally assign a value to a wire, you cannot use multiple set statements inside if-expressions, instead you should compute the wire to output using an if- or match-expression, and assign that resulting value to the wire.

struct ports

In the example above, we used tuples to group related wires together, but often you also want to give names to each wires. Then, the struct port construct comes in handy. It behaves like a struct, but contains only wires instead of only values.

For example, the memory port shown in the previous example can be written as a struct port

struct port MemoryPort {
    addr: &mut Addr,
    data: &Data
}

entity memory() -> (MemoryPort, MemoryPort) {...}

entity consumer(memory_port: MemoryPort);

Inverted Ports

The inverse of a port type is written as ~P. On an inverted port, mutable wires are non-mutable and immutable wires are mutable. This is useful when a consumer and a producer of a port both expect that port to be passed as an argument, rather than returned by one of the ports.

The port expression

The only way to construct an inverted port is via the port expression which creates a (P, ~P) tuple as shown below:

entity top() {
    let (p, p_inv) = port;

    let _ = inst consumer(p);
    let _ = inst producer(p_inv)
}

entity consumer(p: P) -> bool {
    // ...
}

entity producer(p: ~P) -> bool {
    // ...
}

Using Inverted Ports

Inverted ports work like their non-inverted counterparts. They are linear types, so their mutable wires must be set exactly once and their non-mutable wires can be read freely.

Accessing a field of an inverted port returns an inverted port if the field is a struct port.

struct port Inner<T> {
    i: &mut T
    o: &T
}

struct port Outer<T> {
    inner: Inner<T>
    raw: &mut T
}

entity inverse_user<bool>(p: ~Outer<bool>) {
    let _: &bool = p.raw;
    let _: ~Inner<bool> = p.inner;
    let _: &bool = p.inner.i;
    let _: &mut bool = p.inner.o;
}

Dynamic Pipelines

For conditionally executing pipelines, an enable condition can be specified on the reg statement. If this condition is false, the old value of all pipeline registers for this stage will be held, rather than being updated to the new values.

The stall condition is specified as follows

pipeline(1) pipe(clk: clock, condition: bool, x: bool) -> bool {
    reg[condition];
       x
}

where condition is a boolean expression which when true updates all the registers for this stage, and when false the register content is undefined1.

The above code is compiled down to the equivalent of

entity pipe(clk: clock, condition: bool, x: bool) -> bool {
    reg(clk) condition_s1 = if condition {condition} else {condition_s1}
    reg(clk) x_s1 = if condition {x} else {x_s1}
    x_s1
}

Pipeline enable conditions propagate to stages above the enabled stage, in order to make sure that values are not flushed. This means that in the following code

pipeline(1) pipe(clk: clock, x: bool) -> bool {
    reg;
    reg[inst check_condition()];
    reg;
        x
}

the first two stages will be disabled and keep their old value when check_condition returns false while the registers in the final stage will update unconditionally.

If several conditions are used, they are combined, i.e. in

pipeline(1) pipe(clk: clock, x: bool) -> bool {
    reg;
    reg[inst check_condition()];
    reg;
    reg[inst check_other_condition()];
    reg;
        x
}

the first two stages will update only if both check_condition() and check_other_condition() are true, and the next two registers are only going to update if check_other_condition is true.

stage.ready and stage.valid

In some cases it is necessary to check if a stage will be updated on the next cycle (ready) or if the values in the current cycle are valid. This is done using stage.valid and stage.ready.

stage.ready is true if the registers directly following the statement will update their values this cycle, i.e. if the condition of it and all downstream registers are met.

stage.valid is true if the values in the current stage were enabled, i.e. if none of the conditions for any registers this value flowed through were false.

NOTE: stage.valid currently initializes as undefined, and needs time to propagate through the pipeline. It is up to the user to ensure that a reset signal is asserted long enough for stage.valid to stabilize.

Example: Processor

This is part of a processor that stalls the pipeline in order to allow 3 cycles for a load instruction. The program_counter entity takes a signal indicating whether it should count up, or stall. This signal is set to stage.ready, to ensure that if the downstream registers don't accept new instructions, the program counter will stall.

pipeline(5) cpu(clk: clock) -> bool {
        let pc = program_counter$(clk, stall: stage.ready)
    reg;
        let insn = inst(1) program_memory(clk)
        let stall = stage(+1).is_load || stage(+2).is_load || stage(+3).is_load;
    reg[stall];
        let is_load = is_load(insn);
    reg;
        let alu_out = alu(insn);
    reg;
    reg;
        let regfile_write = if stage.valid && insn_writes(insn) {Some(alu)} else {None()}

        true // NOTE: Dummy output, we need to return something
}

the last line where regfile_write is set uses stage.valid to ensure that results of an instruction are only written for valid signals, not signals being undefined due to a stalled register.

Example: Latency Insensitive Interface

A common design method in hardware is to use a ready/valid interface. Here, a downstream unit can communicate that it is ready to receive data by asserting a ready signal, and upstream unit indicate that their data is valid using a valid signal. If both ready and valid are set, the upstream unit hands over a piece of data to the downstream unit. What follows is an example of a pipelined multiplier that propagates a ready/valid signal from its downstream unit to its upstream unit

struct port Rv<T> {
    data: &T,
    valid: &bool,
    ready: &mut bool
}

pipeline(4) mul(clk: clock, a: Rv<int<16>>, b: Rv<int<16>>) -> Rv<int<32>> {
        let product = a*b;
        set a.ready = stage.ready;
        set b.ready = stage.ready;
    reg[*a.valid && *b.valid];
    reg;
    reg; 
        let downstream_ready = inst new_mut_wire();
    reg[inst read_mut_wire(downstream_ready)];
        Rv {
            data: &product,
            valid: &stage.valid,
            ready: downstream_ready,
        }
}
1

Currently, the implementation holds the previous value of the register, which will also be done in hardware. However, this might change to setting the value to X for easier debugging, and to give more optimization opportunities for the synthesis tool.

Binding

Constructs by syntax

This is a list of syntax constructs in the language with a link to a description of the underlying language construct. The list is split in two: constructs which start with a keyword and those which do not

Keywords

Symbolic

Config

The main project configuration specified in swim.toml

Summary

# The name of the library. Must be a valid Spade identifier
# Anything defined in this library will be under the `name` namespace
name = "…"
# List of optimization passes to apply in the Spade compiler. The passes are applied
# in the order specified here. Additional passes specified on individual modules with
# #[optimize(...)] are applied before global passes.
optimizations = ["…", …]
# List of commands to run before anything else.
preprocessing = ["…", …] # Optional
# Paths to verilog files to include in all verilog builds (simulation and synthesis).
# Supports glob syntax
extra_verilog = ["…", …] # Optional
# Map of libraries to include in the build.
# 
# Example:
# ```toml
# [libraries]
# protocols = {git = https://gitlab.com/TheZoq2/spade_protocols.git}
# spade_v = {path = "deps/spade-v"}
# ```
libraries = {key: <Library>, …} # Optional
# Plugins to load. Specifies the location as a library, as well
# as arguments to the plugin
# 
# Example:
# ```toml
# [plugins.loader_generator]
# path = "../plugins/loader_generator/"
# args.asm_file = "asm/blinky.asm"
# args.template_file = "../templates/program_loader.spade"
# args.target_file = "src/programs/blinky_loader.spade"
# 
# [plugins.flamegraph]
# git = "https://gitlab.com/TheZoq2/yosys_flamegraph"
# ```
# 
# Plugins contain a `swim_plugin.toml` which describes their behaviour.
# See [crate::plugin::config::PluginConfig] for details
plugins = {key: <Plugin>, …} # Optional

# Where to find the Spade compiler. See [Library] for details
[compiler]
<Library>

[simulation] # Optional
<Simulation>

[synthesis] # Optional
<Synthesis>

# Preset board configuration which can be used instead of synthesis, pnr, packing and upload
[board] # Optional
<Board>

[pnr] # Optional
<Pnr>

[packing] # Optional
<PackingTool>

[upload] # Optional
<UploadTool>

[log_output]
<LogOutputLevel>

name String

The name of the library. Must be a valid Spade identifier Anything defined in this library will be under the name namespace

optimizations [String]

List of optimization passes to apply in the Spade compiler. The passes are applied in the order specified here. Additional passes specified on individual modules with #[optimize(...)] are applied before global passes.

compiler Library

Where to find the Spade compiler. See [Library] for details

preprocessing [String]

List of commands to run before anything else.

extra_verilog [String]

Paths to verilog files to include in all verilog builds (simulation and synthesis). Supports glob syntax

simulation Simulation

synthesis Synthesis

board Board

Preset board configuration which can be used instead of synthesis, pnr, packing and upload

pnr Pnr

packing PackingTool

upload UploadTool

libraries Map[String => Library]

Map of libraries to include in the build.

Example:

[libraries]
protocols = {git = https://gitlab.com/TheZoq2/spade_protocols.git}
spade_v = {path = "deps/spade-v"}

plugins Map[String => Plugin]

Plugins to load. Specifies the location as a library, as well as arguments to the plugin

Example:

[plugins.loader_generator]
path = "../plugins/loader_generator/"
args.asm_file = "asm/blinky.asm"
args.template_file = "../templates/program_loader.spade"
args.target_file = "src/programs/blinky_loader.spade"

[plugins.flamegraph]
git = "https://gitlab.com/TheZoq2/yosys_flamegraph"

Plugins contain a swim_plugin.toml which describes their behaviour. See [crate::plugin::config::PluginConfig] for details

log_output LogOutputLevel

LogOutputLevel

One of these strings:

  • "Full"
  • "Minimal"
Plugin

Summary

args = {key: "…", …}

[lib]
<Library>

lib Library

args Map[String => String]

UploadTool

One of the following:

icesprog

tool = "icesprog"

Fields

iceprog

tool = "iceprog"

Fields

tinyprog

tool = "tinyprog"

Fields

openocd

tool = "openocd"
config_file = "path/to/file"
Fields

config_file FilePath

fujprog

tool = "fujprog"

Fields

custom

Instead of running a pre-defined set of commands to upload, run the specified list of commands in a shell. #packing_result# will be replaced by the packing output

tool = "custom"
commands = ["…", …]
Fields

commands [String]

PackingTool

One of the following:

icepack

tool = "icepack"

Fields

ecppack

tool = "ecppack"
idcode = "…" # Optional
Fields

idcode String

Pnr

One of the following:

ice40

architecture = "ice40"

[device]
<Ice40Device>
package = "…"
# If set, inputs and outputs of the top module do not need a corresponding field
# in the pin file. This is helpful for benchmarking when pin mapping is irreleveant, but
# when running in hardware, it is recommended to leave this off in order to get a warning
# when pins aren't set in the pin file.
allow_unconstrained = true|false
# Continue to the upload step even if the timing isn't met.
# This is helpful when you suspect that the place-and-route tool is conservative
# with its timing requirements, but gives no guarantees about correctness.
allow_timing_fail = true|false
# The path to a file which maps inputs and outputs of your top module to physical pins.
# On ECP5 chips, this is a `pcf` file, and on iCE40, it is an `lpf` file.
pin_file = "path/to/file"
Fields

device Ice40Device

package String

allow_unconstrained bool

If set, inputs and outputs of the top module do not need a corresponding field in the pin file. This is helpful for benchmarking when pin mapping is irreleveant, but when running in hardware, it is recommended to leave this off in order to get a warning when pins aren't set in the pin file.

allow_timing_fail bool

Continue to the upload step even if the timing isn't met. This is helpful when you suspect that the place-and-route tool is conservative with its timing requirements, but gives no guarantees about correctness.

pin_file FilePath

The path to a file which maps inputs and outputs of your top module to physical pins. On ECP5 chips, this is a pcf file, and on iCE40, it is an lpf file.

ecp5

architecture = "ecp5"

[device]
<Ecp5Device>
package = "…"
# If set, inputs and outputs of the top module do not need a corresponding field
# in the pin file. This is helpful for benchmarking when pin mapping is irreleveant, but
# when running in hardware, it is recommended to leave this off in order to get a warning
# when pins aren't set in the pin file.
allow_unconstrained = true|false
# Continue to the upload step even if the timing isn't met.
# This is helpful when you suspect that the place-and-route tool is conservative
# with its timing requirements, but gives no guarantees about correctness.
allow_timing_fail = true|false
# The path to a file which maps inputs and outputs of your top module to physical pins.
# On ECP5 chips, this is a `pcf` file, and on iCE40, it is an `lpf` file.
pin_file = "path/to/file"
Fields

device Ecp5Device

package String

allow_unconstrained bool

If set, inputs and outputs of the top module do not need a corresponding field in the pin file. This is helpful for benchmarking when pin mapping is irreleveant, but when running in hardware, it is recommended to leave this off in order to get a warning when pins aren't set in the pin file.

allow_timing_fail bool

Continue to the upload step even if the timing isn't met. This is helpful when you suspect that the place-and-route tool is conservative with its timing requirements, but gives no guarantees about correctness.

pin_file FilePath

The path to a file which maps inputs and outputs of your top module to physical pins. On ECP5 chips, this is a pcf file, and on iCE40, it is an lpf file.

Ecp5Device

One of these strings:

  • "LFE5U-12F"
  • "LFE5U-25F"
  • "LFE5U-45F"
  • "LFE5U-85F"
  • "LFE5UM-25F"
  • "LFE5UM-45F"
  • "LFE5UM-85F"
  • "LFE5UM5G-25F"
  • "LFE5UM5G-45F"
  • "LFE5UM5G-85F"
Ice40Device

One of these strings:

  • "iCE40LP384"
  • "iCE40LP1K"
  • "iCE40LP4K"
  • "iCE40LP8K"
  • "iCE40HX1K"
  • "iCE40HX4K"
  • "iCE40HX8K"
  • "iCE40UP3K"
  • "iCE40UP5K"
  • "iCE5LP1K"
  • "iCE5LP2K"
  • "iCE5LP4K"
Board

One of the following:

Ecpix5

name = "Ecpix5"
pin_file = "path/to/file" # Optional
config_file = "path/to/file" # Optional
Fields

pin_file FilePath

config_file FilePath

GoBoard

name = "GoBoard"
pcf = "path/to/file" # Optional
Fields

pcf FilePath

tinyfpga-bx

name = "tinyfpga-bx"
pcf = "path/to/file" # Optional
Fields

pcf FilePath

Icestick

name = "Icestick"
pcf = "path/to/file" # Optional
Fields

pcf FilePath

Synthesis

Summary

# The name of the unit to use as a top module for the design. The name must
# be an absolute path to the unit, for example `proj::main::top`, unless the
# module is marked `#[no_mangle]` in which case the name is used.
# 
# Can also be set to the name of a module defined in verilog if a pure verilog top
# is desired.
top = "…"
# The yosys command to use for synthesis
command = "…"
# Extra verilog files only needed during the synthesis process.
# Supports glob syntax
extra_verilog = ["…", …] # Optional

top String

The name of the unit to use as a top module for the design. The name must be an absolute path to the unit, for example proj::main::top, unless the module is marked #[no_mangle] in which case the name is used.

Can also be set to the name of a module defined in verilog if a pure verilog top is desired.

command String

The yosys command to use for synthesis

extra_verilog [String]

Extra verilog files only needed during the synthesis process. Supports glob syntax

Simulation

Summary

# Directory containing all test benches
testbench_dir = "path/to/file"
# Extra dependencies to install to the test venv via pip
python_deps = ["…", …] # Optional
# The simulator to use as the cocotb backend. Currently verified to support verilator and
# icarus, but other simulators supported by cocotb may also work.
# 
# Defaults to 'icarus'
# 
# Requires a relatively recent version of verilator
simulator = "…"
# The C++ version to use when compiling verilator test benches. Anything that
# clang or gcc accepts in the -std= field works, but the verilator wrapper requires
# at least c++17.
# Defaults to c++17
cpp_version = "…" # Optional
# Extra arguments to pass to verilator when building C++ test benches. Supports substituting
# `#ROOT_DIR#` to get project-relative directories
verilator_args = ["…", …] # Optional

testbench_dir FilePath

Directory containing all test benches

python_deps [String]

Extra dependencies to install to the test venv via pip

simulator String

The simulator to use as the cocotb backend. Currently verified to support verilator and icarus, but other simulators supported by cocotb may also work.

Defaults to 'icarus'

Requires a relatively recent version of verilator

cpp_version String

The C++ version to use when compiling verilator test benches. Anything that clang or gcc accepts in the -std= field works, but the verilator wrapper requires at least c++17. Defaults to c++17

verilator_args [String]

Extra arguments to pass to verilator when building C++ test benches. Supports substituting #ROOT_DIR# to get project-relative directories

Library

Location of a library or external code. Either a link to a git repository, or a path relative to the root of the project.

compiler = {git = "https://gitlab.com/spade-lang/spade/"}
path = "compiler/"

One of the following:

Git

Downloaded from git and managed by swim


git = "…"
commit = "…" # Optional
tag = "…" # Optional
branch = "…" # Optional
Fields

git String

commit String

tag String

branch String

Path

A library at the specified path. The path is relative to swim.toml


path = "path/to/file"
Fields

path FilePath

PluginConfig

Summary

# True if this plugin needs the CXX bindings for the spade compiler to be built
requires_cxx = true|false
# Commands required to build the plugin. Run before any project compilation steps
build_commands = ["…", …]
# The files which this plugin produces
builds = [<BuildResult>, …]
# Arguments which must be set in the `swim.toml` of projects using the plugin
required_args = ["…", …]
# Commands to run after building swim file but before anything else
post_build_commands = ["…", …]
# Commands which the user can execute
commands = {key: <PluginCommand>, …}

# Things to do during the synthesis process
[synthesis] # Optional
<SynthesisConfig>

requires_cxx bool

True if this plugin needs the CXX bindings for the spade compiler to be built

build_commands [String]

Commands required to build the plugin. Run before any project compilation steps

builds [BuildResult]

The files which this plugin produces

required_args Set[String]

Arguments which must be set in the swim.toml of projects using the plugin

post_build_commands [String]

Commands to run after building swim file but before anything else

synthesis SynthesisConfig

Things to do during the synthesis process

commands Map[String => PluginCommand]

Commands which the user can execute

PluginCommand

Summary

# List of system commands to run in order to execute the command
# 
# Commands specified by the user, i.e. whatever is after `swim plugin <command>`
# is string replaced into `%args%` in the resulting command string. The arguments
# are passed as strings, to avoid shell expansion
script = ["…", …]

# The build step after which to run this command
[after]
<BuildStep>

script [String]

List of system commands to run in order to execute the command

Commands specified by the user, i.e. whatever is after swim plugin <command> is string replaced into %args% in the resulting command string. The arguments are passed as strings, to avoid shell expansion

after BuildStep

The build step after which to run this command

BuildStep

One of these strings:

  • "Start" Before any other processing takes place
  • "SpadeBuild"
  • "Simulation"
  • "Synthesis"
  • "Pnr"
  • "Upload"
SynthesisConfig

Summary

# Yosys commands to run after the normal yosys flow
yosys_post = ["…", …]

yosys_post [String]

Yosys commands to run after the normal yosys flow

BuildResult

Summary

# The path of a file built by this build step
path = "…"

# The first build step for which this file is required. This will trigger
# a re-build of this build step if the file was changed
[needed_in]
<BuildStep>

path String

The path of a file built by this build step

needed_in BuildStep

The first build step for which this file is required. This will trigger a re-build of this build step if the file was changed

Compiler Internals

This chapter describes some internals of the compiler and details about code generation. Normally, this is not relevant to users of the language.

Naming

This chapter describes the naming scheme used by the compiler when generating Verilog. The goal of the Verilog generator is not to generate readable Verilog, but there should be a clear two-way mapping between signal names in the source Spade code and generated Verilog. This mapping should be clear both to users reading lists of signals, for example, in VCD files, and tools, for example VCD parsers.

Variables

Because Spade does not have the same scoping rules as Verilog, some deconfliction of names internal to a Verilog module is needed.

If a name x only occurs once in a unit, the corresponding Verilog name is \x . (This is using the Verilog raw escape string system, and some tools may report the name as x). If x occurs more than once, subsequent names are given an index ordered sequentially in the order that they are visited during AST lowering1 The kth occurrence of a name is suffixed by _n{k}

Pipelined versions of names are suffixed with _s{n} where n is the absolute stage index of the stage.

Names of port type with mutable wires have an additional variable for the mutable bits. This follows the same naming scheme as the forward name, but is suffixed by _mut

The following is an example of the naming scheme

pipeline(1) pipe(
    x: bool, // "\x "
    y: (&bool, &mut bool) // "\y ", "y_o "
) {
        if true {
            let x = true; // "x_n1"
        } else {
            let x = false; // "x_n2"
        }
        let x = true; // "x_n3"
    reg; // "\x_s1 ", "x_n3_s1
        let z = true; // "\z "
}

Spade makes no guarantees about name uniqueness between generated Verilog modules.

1

This is currently the lexical order of the occurrences, i.e. names which occur early in the module are given lower indices.

Type Representation

Description of the Verilog representation of Spade types

Mixed-direction types

Types with mixed direction wires are split in two separate variables, typically <name> and <name>_mut. The structure of the forward part is the same as if the backward part didn't exist, and the backward part is structured as if it were the forward part.

For example, (int<8>, &mut int<9>, int<2>, &mut int<3>) is stored as (int<8>, int<2>) and (int<9>, int<3>).

Tuples

Tuples are stored with their members packed side to side, with the 0th member on the left.

let x: (int<8>, int<2>, bool) = (a, b, c);

is represented as

logic x[10:0];
assign x = {a,b,c};

Binary representation

aaaaaaaabbc

Enums

Enums are packed with the leftmost bits being the discriminant and the remaining bits being the payload. The payload is packed left-to-right, meaning that the rightmost bits are undefined if a variant is smaller than the largest variant.

enum A {
    V1(a: int<8>),
    V2(b: int<2>),
    V3(c: bool)
}
    9 8 7 6 5 4 3 2 1 0
    t t p p p p p p p p
    -------------------
V1: 0 0 a a a a a a a a
V2: 0 1 b b X X X X X X
V3: 1 0 c X X X X X X X