Wishful Coding

Didn't you ever wish your computer understood you?

A Rust HAL for your LiteX FPGA SoC

ULX3S demo

FPGAs are amazing in their versatility, but can be a real chore when you have to map out a giant state machine just to talk to some chip over SPI. For such cases, nothing beats just downloading an Arduino library and quickly hacking some example code. Or would there be a way to combine the versatility of an FPGA with the ease of Arduino libraries? That is the question I want to explore in this post.

Of course you can use an f32c softcore on your FPGA as an Arduino, but that’s a precompiled core, and basically doesn’t give you the ability to use your FPGA powers. Or you can build your own SoC with custom HDL components, but then you’re back to bare-metal programming.

Unless you can tap into an existing library ecosystem by writing a hardware abstraction layer for your SoC. And that is exactly what I’ve done by writing a Rust embedded HAL crate that works for any LiteX SoC!

LiteX allows you to assemble a SoC by connecting various components to a common Wishbone bus. It supports various RISC-V CPU’s (and more), and has a library of useful components such as GPIO and SPI, but also USB and Ethernet. These all get memory-mapped and can be accessed via the Wishbone bus by the CPU and other components.

The amazing thing is that LiteX can generate an SVD file for the SoC, which contains all the registers of the components you added to the SoC. This means that you can use svd2rust to compile this SVD file into a peripheral access crate.

This PAC crate abstracts away memory addresses, and since the peripherals themselves are reusable components, it is possible to build a generic HAL crate on top of it that supports a certain LiteX peripheral in any SoC that uses it. Once the embedded HAL traits are implemented, you can use these LiteX peripherals with every existing Rust crate.

The first step is to install LiteX. Due to a linker bug in Rust 1.45, I used the 1.46 beta. I’m also installing into a virtualenv to keep my system clean. While we’re going to use Rust, gcc is still needed for compiling the LiteX BIOS and for some objcopy action.

#rustup default beta
virtualenv env
source env/bin/activate
wget https://raw.githubusercontent.com/enjoy-digital/litex/master/litex_setup.py
chmod +x litex_setup.py
./litex_setup.py init install
./litex_setup.py gcc
export PATH=$PATH:$(echo $PWD/riscv64-*/bin/)

Now we need to make some decisions about which FPGA board and CPU we’re going to use. I’m going to be using my ULX3S, but LiteX supports many FPGA boards out of the box, and others can of course be added. For the CPU we have to pay careful attention to match it with an architecture that Rust supports. For example Vexrisc supports the im feature set by default, which is not a supported Rust target, but it also supports an i and imac variant, both of which Rust supports. PicoRV32 only supports i or im, so can only be used in combination with the Rust i target.

So let’s go ahead and make one of those. I’m going with the Vexrisc imac variant, but on a small iCE40 you might want to try the PicoRV32 (or even Serv) to save some space. Of course substitute the correct FPGA and SDRAM module on your board.


cd litex-boards/litex_boards/targets
python ulx3s.py --cpu-type vexriscv --cpu-variant imac --csr-data-width 32 --device LFE5U-85F --sdram-module AS4C32M16 --csr-svd ulx3s.svd --build --load
rustup target add riscv32imac-unknown-none-elf


python ulx3s.py --cpu-type picorv32 --cpu-variant minimal --csr-data-width 32 --device LFE5U-85F --sdram-module AS4C32M16 --csr-svd ulx3s.svd --build --load
rustup target add riscv32i-unknown-none-elf

Most parameters should be obvious. The --csr-data-width 32 parameter sets the register width, which I’m told will be the default in the future, and saves a bunch of bit shifting later on. --csr-svd ulx3s.svd tells LiteX to generate an SVD file for your SoC. You can omit --build and --load and manually do these steps by going to the build/ulx3s/gateware/ folder and running build_ulx3s.sh. I also prefer to use the awesome openFPGALoader rather than the funky ujprog with a sweet openFPGALoader --board ulx3s ulx3s.bit.

Now it is time to generate the PAC crate with svd2rust. This crate is completely unique to your SoC, so there is no point in sharing it. As long as the HAL crate can find it you’re good. Follow these instructions to create a Cargo.toml with the right dependencies. In my experience you may want to update the version numbers a bit. I had to use the latest riscv and riscv-rt to make stuff work, but keep the other versions to not break the PAC crate.

cargo new --lib litex-pac
cd litex-pac/src
svd2rust -i ulx3s.svd --target riscv
cd ..
vim Cargo.toml

Now we can use these instructions to create our first Rust app that uses the PAC crate. I pushed my finished example to this repo. First create the app as usual, and add dependencies. You can refer to the PAC crate as follows.

litex-pac = { path = "../litex-pac", features = ["rt"]}

Then you need to create a linker script that tells the Rust compiler where to put stuff. Luckily LiteX generated the important parts for us, and we only have to define the correct REGION_ALIAS expressions. Since we will be using the BIOS, all our code will get loaded in main_ram, so I set all my aliases to that. It is possible to load code in other regions, but my attempts to put the stack in SRAM failed horribly when the stack grew too large, so better start with something safe and then experiment.


Next, you need to actually tell the compiler about your architecture and linker scripts. This is done with the .cargo/config file. This should match the Rust target you installed, so be mindful if you are not using imac. Note the regions.ld file that LiteX generated, we’ll get to that in the next step.

rustflags = [
  "-C", "link-arg=-Tregions.ld",
  "-C", "link-arg=-Tmemory.x",
  "-C", "link-arg=-Tlink.x",

target = "riscv32imac-unknown-none-elf"

The final step before jumping in with the Rust programming is writing a build.rs file that copies the linker scripts to the correct location for the compiler to find them. I mostly used the example provided in the instructions, but added a section to copy the LiteX file. export BUILD_DIR to the location where you generated the LiteX SoC.

    let mut f = File::create(&dest_path.join("regions.ld"))
        .expect("Could not create file");
    f.write_all(include_bytes!(concat!(env!("BUILD_DIR"), "/software/include/generated/regions.ld")))
        .expect("Could not write file");

That’s it. Now the code you compile will actually get linked correctly. I found these iCEBreaker LiteX examples very useful to get started. This code will actually run with minimal adjustment on our SoC, and is a good start to get a feel for how the PAC crate works. Another helpful command is to run cargo doc --open in the PAC crate to see the generated documentation.

To actually upload the code, you have to convert the binary first.

cargo build --release
cd /target/riscv32imac-unknown-none-elf/release
riscv64-unknown-elf-objcopy litex-example -O binary litex-example.bin
litex_term --kernel litex-example.bin /dev/ttyUSB0

From here we “just” need to implement HAL traits on top of the PAC to be able to use almost any embedded library in the Rust ecosystem. However, one challenge is that the peripherals and their names are not exactly set in stone. The way that I solved it is that the HAL crate only exports macros that generate HAL trait implementations. This way your SoC can have 10 SPI cores and you just have to call the spi macro to generate a HAL for them. I uploaded the code in this repo.

Of course so far we’ve only used the default SoC defined for the ULX3S. The real proof is if we can add a peripheral, write a HAL layer for it, and then use an existing library with it. I decided to add an SPI peripheral for the OLED screen. First I added the following pin definition

    ("oled_spi", 0,
        Subsignal("clk",  Pins("P4")),
        Subsignal("mosi", Pins("P3")),
    ("oled_ctl", 0,
        Subsignal("dc",   Pins("P1")),
        Subsignal("resn", Pins("P2")),
        Subsignal("csn",  Pins("N2")),

and then the peripheral itself

    def add_oled(self):
        pads = self.platform.request("oled_spi")
        pads.miso = Signal()
        self.submodules.oled_spi = SPIMaster(pads, 8, self.sys_clk_freq, 8e6)

        self.submodules.oled_ctl = GPIOOut(self.platform.request("oled_ctl"))

This change has actually been accepted upstream, so now you can just add the --add-oled command line option and you get a brand new SoC with an SPI controller for the OLED display. Once the PAC is generated again and the FullDuplex trait has been implemented for it, it is simply a matter of adding the SSD1306 or SDD1331 crate, and copy-pasting some example code. Just as easy as an Arduino, but on your own custom SoC!

Pepijn de Vos

Open Source Formal Verification in VHDL

I believe in the importance of open source synthesis, and think it’s important that open source tools support both Verilog and VHDL. Even though my GSoC proposal to add VHDL support to Yosys was rejected, I’ve still been contributing small bits and pieces to GHDL and its Yosys plugin.

This week we reached what I think is an important milestone: I was able to synthesize my VHDL CPU and then formally verify the ALU of it using completely open source tools. (and then synthesize it to an FPGA which is not supported by open source tools yet) There is a lot to unpack here, so let’s jump in.

Yosys, Nextpnr, SymbiYosys, GHDL, ghdlsynth-beta

Yosys is an open source synthesis tool that is quickly gaining momentum and supporting more and more FPGAs. Yosys currently supports Verilog, and turns that into various low-level netlist representations.

Nextpnr is a place-and-rout tool, which takes a netlist and turns it into a bitstream for any of the supported FPGA types. These bitstream formats are not publicly documented, so this is a huge reverse-engineering effort.

SymbiYosys is a tool based around Yosys and various SAT solvers to let you do formal verification on your code. More on formal verification later. But important to know is that it works on the netlists generated by Yosys.

GHDL is an open source VHDL simulator, and as far as I know, one of its kind. VHDL is notoriously hard to parse, so many other open source attempts at VHDL simulation and synthesis have faltered. Work is underway to add synthesis to GHDL.

And last but not least, ghdlsynth-beta is a plugin for Yosys that converts the synthesis format of GHDL to the intermediate representation of Yosys, allowing it to be synthesized to various netlist formats and used for FPGA, ASIC, formal verification, and many other uses. It is currently a separate repository, but the goal is to eventually upstream it into Yosys.

Formal Verification

I think formal verification sounds harder and more scary than it is. An alternative description is property testing with a SAT solver. Think Quickcheck, not Coq. This is much simpler and less formal than using a proof assistent.

Basically you describe properties about your code, and SymbiYosys compiles your code an properties to a netlist and from a netlist to Boolean logic. A SAT solver is then used to find inputs to your code that (dis)satisfy the properties you described. This does not “prove” that your code is correct, but it proves that it satisfies the properties you defined.

In hardware description languages you describe properties by assertions and assumptions. An assumption constrains what the SAT solver can consider as valid inputs to your program, and assertions are things you believe to be true about your code.

The powerful thing about formal verification is that it considers all valid inputs at every step, and not just the happy case you might test in simulation. It will find so many edge cases it’s not even funny. Once you get the hang of it, it’s actually less work than writing a testbench. Just a few assertions in your code and the bugs come flying at you.

If you want to learn more about formal verification, Dan Gisselquist has a large number of articles and tutorials about it, mainly using Verilog.


To play along at home, you need to install a fair number of programs, so better get some of your favourite hot beverage.

At this point you should be able to run ghdl --synth foo.vhd -e foo which will output a VHDL representation of the synthesized netlist. You should be able to run yosys -m ghdl and use the Yosys command ghdl foo.vhd -e foo to obtain a Yosys netlist which you can then show, dump, synth, or even write_verilog.

Verifying a bit-serial ALU

To demonstrate how formal verification works and why it is so powerful, I want to walk you through the verification of the ALU of my CPU.

I’m implementing a bit-serial architecture, which means that my ALU operates on one bit at a time, producing one output bit and a carry. The carry out is then the carry in to the next bit. The logic that produces the output and the carry depends on a 3-bit opcode.

  process(opcode, a, b, ci)
    case opcode is
      when "000" => -- add
        y <= a xor b xor ci; -- output
        co <= (a and b) or (a and ci) or (b and ci); -- carry
        cr <= '0'; -- carry reset value
      -- [...]
    end case;
  end process;

  process(clk, rst_n)
    if(rising_edge(clk)) then
      if(rst_n = '0') then
        ci <= cr; -- reset the carry
        ci <= co; -- copy carry out to carry in
      end if;
    end if;
  end process;

Important to note is the carry reset value. For addition, the first bit is added without carry, but for subtraction the carry is 1 because -a = (not a) + 1, and similarly for other different opcodes. So when in reset, the ALU sets the carry in to the reset value corresponding to the current opcode.

So now onward to the verification part. Since VHDL only has assert and none of the SystemVerilog goodies, Property Specification Language is used. (that link contains a good tutorial) PSL not only provides restrict, assume, and cover, but also allows you to express preconditions and sequences.

To make my life easier, I want to specify that I want to restrict valid sequences to those where the design starts in reset, processes 8 bits, back to reset, and repeat, so that the reset will look like 011111111011111111...

restrict { {rst_n = '0'; (rst_n = '1')[*8]}[+]};

Then, I want to specify that when the ALU is active, the opcode will stay constant. Else you’ll just get nonsense.

assume always {rst_n = '0'; rst_n = '1'} |=>
  opcode = last_op until rst_n = '0';

Note that I did not define any clock or inputs. Just limiting the reset and opcode is sufficient. With those assumptions in place, we can assert what the output should look like. I shift the inputs and outputs into 8-bit registers, and then when the ALU goes into reset, we can verify the output. For example, if the opcode is “000”, the output should be the sum of the two inputs.

assert always {opcode = "000" and rst_n = '1'; rst_n = '0'} |->
  y_sr = a_sr+b_sr;

After adding the other opcodes, I wrapped the whole thing in a generate block so I can turn it off with a generic parameter for synthesis

formal_gen : if formal generate
  signal last_op : std_logic_vector(2 downto 0);
  signal a_sr : unsigned(7 downto 0);
  signal b_sr : unsigned(7 downto 0);
  signal y_sr : unsigned(7 downto 0);
-- [...]
end generate;

And now all that’s left to do is write the SymbiYosys script and run it. The script just specifies how to compile the files and the settings for the SAT solver. Note that -fpsl is required for reading --psl code in comments, or --std=08 to use VHDL-2008 which supports PSL as part of the core language.

mode bmc
depth 20

smtbmc z3

ghdl --std=08 alu.vhd -e alu
prep -top alu


To load the GHDL plugin, SymbiYosys has to be run as follows:

$ sby --yosys "yosys -m ghdl" -f alu.sby 
SBY 15:02:25 [alu] Removing direcory 'alu'.
SBY 15:02:25 [alu] Copy 'alu.vhd' to 'alu/src/alu.vhd'.
SBY 15:02:25 [alu] engine_0: smtbmc z3
SBY 15:02:25 [alu] base: starting process "cd alu/src; yosys -m ghdl -ql ../model/design.log ../model/design.ys"
SBY 15:02:25 [alu] base: finished (returncode=0)
SBY 15:02:25 [alu] smt2: starting process "cd alu/model; yosys -m ghdl -ql design_smt2.log design_smt2.ys"
SBY 15:02:25 [alu] smt2: finished (returncode=0)
SBY 15:02:25 [alu] engine_0: starting process "cd alu; yosys-smtbmc -s z3 --presat --noprogress -t 20 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Solver: z3
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Checking assumptions in step 9..
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Checking assertions in step 9..
SBY 15:02:25 [alu] engine_0: ##   0:00:00  BMC failed!
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Assert failed in alu: /179
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 15:02:25 [alu] engine_0: ##   0:00:00  Status: FAILED (!)
SBY 15:02:25 [alu] engine_0: finished (returncode=1)
SBY 15:02:25 [alu] engine_0: Status returned by engine: FAIL
SBY 15:02:25 [alu] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:02:25 [alu] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:02:25 [alu] summary: engine_0 (smtbmc z3) returned FAIL
SBY 15:02:25 [alu] summary: counterexample trace: alu/engine_0/trace.vcd
SBY 15:02:25 [alu] DONE (FAIL, rc=2)

Oh no! We have a bug! Let’s open the trace to see what went wrong.

gtkwave alu/engine_0/trace.vcd

gtkwave trace

So we’re doing a subtraction, and according to my math 29-150=-121 but the ALU output is -122, so we’re off by one. A little head-scratching later, we can see the problem: On the first cycle of the subtraction the carry in is zero rather than one! Why? Because on the previous clock cycle the instruction was exclusive or, which reset the carry in to zero.

Note that this bug would never show up if you did a test bench that executes a fixed instruction from reset. But the SAT solver managed to find a specific sequence of opcodes that cause the carry to be wrong. Awesome.

So how do we fix it? There are two ways. The first is to change the code to asynchronously determine the carry in. The second is to write you code so the opcode is stable before the ALU comes out of reset, which ended up using less logic. In this case we can change the opcode assumption to

assume always {rst_n = '0'; rst_n = '1'} |->
  opcode = last_op until rst_n = '0';

Note that we used the thin arrow |-> rather than the fat arrow |=> now. The fat arrow triggers after the precondition has been met, while the thin arrow overlaps with the end of the precondition. So now we’re saying that when reset became inactive, the opcode is the same as it was while the device was in reset. Let’s try again.

$ sby --yosys "yosys -m ghdl" -f alu.sby 
SBY 15:31:36 [alu] Removing direcory 'alu'.
SBY 15:31:36 [alu] Copy 'alu.vhd' to 'alu/src/alu.vhd'.
SBY 15:31:36 [alu] engine_0: smtbmc z3
SBY 15:31:36 [alu] base: starting process "cd alu/src; yosys -m ghdl -ql ../model/design.log ../model/design.ys"
SBY 15:31:36 [alu] base: finished (returncode=0)
SBY 15:31:36 [alu] smt2: starting process "cd alu/model; yosys -m ghdl -ql design_smt2.log design_smt2.ys"
SBY 15:31:36 [alu] smt2: finished (returncode=0)
SBY 15:31:36 [alu] engine_0: starting process "cd alu; yosys-smtbmc -s z3 --presat --noprogress -t 20 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:31:36 [alu] engine_0: ##   0:00:00  Solver: z3
SBY 15:31:36 [alu] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 15:31:36 [alu] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 15:31:37 [alu] engine_0: ##   0:00:01  Checking assumptions in step 19..
SBY 15:31:37 [alu] engine_0: ##   0:00:01  Checking assertions in step 19..
SBY 15:31:37 [alu] engine_0: ##   0:00:01  Status: PASSED
SBY 15:31:37 [alu] engine_0: finished (returncode=0)
SBY 15:31:37 [alu] engine_0: Status returned by engine: PASS
SBY 15:31:37 [alu] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:01 (1)
SBY 15:31:37 [alu] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:01 (1)
SBY 15:31:37 [alu] summary: engine_0 (smtbmc z3) returned PASS
SBY 15:31:37 [alu] DONE (PASS, rc=0)


Debugging tips

It should be said that all of this is very experimental and you are therefore likely to run into bugs and missing features. I would say that at this point it is feasible to write new code and work around GHDL’s current limitations (or fix them!), but running large existing codebases is unlikely to be successful. (but very much the goal!)

When you run into errors, the first step is to find out if it is a bug in the plugin or GHDL itself.

If you see Unsupported(1): instance X of Y. this means the plugin does not know how to translate a GHDL netlist item to Yosys. These are usually pretty easy to fix. See this pull request for an example. Good to know: Id_Sub is defined in ghdlsynth_gates.h which is generated from netlists-gates.ads. module->addSub is defined in rtlil.h.

If you just see ERROR: vhdl import failed. this likely means GHDL crashed. Run GHDL outside Yosys (ghdl --synth) to see the actual error. Usually it’ll show something like some_package: cannot handle IIR_KIND_SOMETHING (mycode.vhd:26:8) which means that some_pacakge in the src/synth part of GHDL can’t handle some language construct yet. This can be anything from a missing operator to whole language constructs, and the fix can be anything for copy-pasting another operator to a serious project. See this pull request for an example on how to add a missing operator.

If it’s not obvious what is going on, it’s time to break out gdb. It’s important to know that in the GHDL repo there is a .gdbinit that you can source inside gdb. This enables catching exceptions and includes utilities for printing IIR values. If you want to debug inside Yosys, it is helpful to first run the program without breakpoints so all the libraries are loaded and gdb understands there is Ada code involved. Then source .gdbinit, set breakpoints, and run again. (note: GHDL/Yosys command line arguments are passed to run and not gdb)

Happy debugging!

Pepijn de Vos


When learning to program FPGAs using VHDL or Verilog, you also learn that these hardware description languages can be used to design ASICs (application specific integrated circuit). But this is only something big corporations with millions of dollars can afford, right? Even though I later learned it only costs thousands, not millions, to make an ASIC on an older process, it is still far away from hobby budgets.

I had been keeping an eye on Yosys, the open source HDL synthesis tool, which can apparently do ASIC by giving it a liberty file that specifies the logic cells your foundry supports. Meanwhile I also toyed with the idea of making a 7400 series computer, and I wondered if you could write a liberty file for 7400 chips. I had kind of dismissed the idea, but then ZirconiumX came along and did it.

It suffices to say this revived my interest in the idea and a lively discussion and many pull requests followed. First some small changes, then simulations to verify the synthesized result is still correct, and finally a KiCad netlist generator.

You see, generating a Yosys netlist is nice, but eventually these 7400 chips have to end up on a PCB somehow. Normally you draw your schematic in Eeschema, generate a netlist, and import that to Pcbnew. But instead I used skidl to generate the netlist directly. Then all there is to do is add the inputs and outputs and run the autorouter (or do it manually of course).

I decided to do a proof-of-concept “application specific interconnected circuit”, with the goal of making something fun in under 10 chips. (a Risc-V CPU currently sits at about 850) I settled on a fading PWM circuit to drive an LED. I manually added a 555-based clock, and ordered a PCB for a few bucks. A few weeks later, this was the result. It worked on the first try! This feeling is even more amazing than with software, and shows that as long as there are no compiler/library bugs or DRC errors, logic simulations are a good way to prove your PCB design.

To follow along at home you need to install Yosys. A recent release might work, but it’s getting better every day, so building from source is recommended. Then you can just git clone 74xx-liberty and go. There are a number of Verilog programs in benchmarks in case you’d rather make PicoRV32 in 7400 chips.

cd stat
make pwmled.stat # synthesize and run stat
../ic_count.py pwmled.stat # count number of chips used
cd ../sim
make pwmled.vcd # synth to low-level verilog and simulate
gtkwave pwmled.vcd # show test bench results
cd ../kicad
make pwmled.net # generate kicad netlist

But this was all done in Verilog, so where is the VHDL, you might wonder. Well, Yosys does not really support VHDL yet, but Tristan Gingold is hard at work making GHDL synthesize VHDL as a Yosys plugin. I think this is very important work, so I’ve been contributing there as well. After some pull requests I was able to port the breathing LED to VHDL.

Getting VHDL to work in Yosys is a bit of effort. First you need to compile GHDL, which requires installing a recent version of GNAT. Then you need to install ghdlsynth-beta as a plugin, allowing you to run yosys -m ghdl. My fork of 74xx-liberty contains additional make rules for doing the above synthesization for VHDL files, which does something like this before calling the 7400 synthesis script.

cd stat
ghdl -a ../benchmarks/pwmled.vhd # analyse VHDL file
yosys -m ghdl -p "ghdl pwmled; show" # load pwmled entity, show graph

yosys dot graph

A huge thank you to all the people working tirelessly to make open source hardware design a reality. You’re awesome!

Pepijn de Vos