Wishful Coding

Didn't you ever wish your computer understood you?

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.

Installation

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)
  begin
    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)
  begin
    if(rising_edge(clk)) then
      if(rst_n = '0') then
        ci <= cr; -- reset the carry
      else
        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);
begin
-- [...]
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.

[options]
mode bmc
depth 20

[engines]
smtbmc z3

[script]
ghdl --std=08 alu.vhd -e alu
prep -top alu

[files]
alu.vhd

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)

Yay!

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

VHDL to PCB

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

Google Summer of Code is excluding half the world from participating

I recently came across someone who wanted to mentor a Yosys VHDL frontent as a Google Summer of Code project. This sounded fun, so I wrote a proposal, noting that GSoC starts before my summer holiday, and planning accordingly. Long story short, there are limited spots and my proposal was not accepted. I have confirmed with the mentoring organization that my availability was the primary factor in this.

While I understand their decision, it seems odd from an organizational viewpoint. Surely others would have the same problem? Indeed I heard from one person that they coped by just working ridiculous hours, while another said they never applied because of the mismatch. Google seems to be aware that this is an issue, stating in their FAQ:

Can the schedule be adjusted if my school ends late/starts early? No. We know that the schedule doesn’t work for some students, but it’s impossible to make a single timeline that works for everyone. Some organizations may allow a participant to start a little early or end a little late – but this is usually measured in days, not weeks. The monthly evaluation dates cannot be changed.

But how big is this problem, and where do accepted proposals come from? I decided to find out. Wikipedia has a long page of summer vacation dates for each country, and there is also this pdf which contains the following helpful graphic.

holidays holidays

Most summer vacations are from July to August, while GSoC runs from May 27 to August 19, excluding most of Europe and many other countries from participating. (unless you lie in your proposal or work 70 hours per week)

The next question is if this is reflected in accepted proposals. Since country of origin is not disclosed, this requires some digging. I scraped a few hundred names from the GSoC website, and scraped their location from a Linkedin search. This is of course not super reliable, but should give some indication.

      1 Argentina
      5 Australia
      1 Bangladesh
      6 Brazil
      1 Canada
      1 Chile
      7 China
      1 Denmark
      3 Egypt
      5 France
      9 Germany
      2 Ghana
      4 Greece
      2 Hong Kong
    212 India
      4 Indonesia
      1 Israel
      4 Italy
      2 Kazakhstan
      2 Kenya
      1 Lithuania
      2 Malaysia
      2 Mexico
      1 Nepal
      2 Nigeria
      1 Paraguay
      1 Peru
      3 Poland
      1 Portugal
      2 Qatar
      4 Romania
      4 Russian Federation
      1 Serbia
      4 Singapore
      1 South Africa
     10 Spain
      8 Sri Lanka
      2 Sweden
      2 Switzerland
      1 Tank
      2 Turkey
      4 Ukraine
      2 United Arab Emirates
      1 United Kingdom
     78 United States
     70 unknown
      1 Uruguay
      1 Uzbekistan
      3 Vietnam

Holy moly, so many Indians(212), followed by a large number of Americans(78), and then Spain(10), Germany(9), and the rest of the world. No Dutchies in this subset. For all European countries I counted a combined 51 participants, still a reasonable number. Even though Spain and Germany have the same holiday mismatch as the Netherlands. Tell me your secret! Interestingly, Wikipedia states that India has very short holidays, but special exceptions for summer programmes:

Summer vacation lasts for no more than six weeks in most schools. The duration may decrease to as little as three weeks for older students, with the exception of two month breaks being scheduled to allow some high school and university students to participate in internship and summer school programmes.

Anyway, I think a big international company like Google could try to be a bit more flexible, and for example let students work for a subset of the monthly evaluation periods that align with their holiday.

Appendix

To scrape the names, I scrolled down on the project page until I got bored, and then entered some JS in the browser console.

Array.prototype.map.call(document.querySelectorAll(".project-card h2"), function(x) { return x.innerText })

I saved this to a file and wrote a Selenium script to search Linkedin. Likedin was being really annoying by serving me different versions of various pages with completely different html tags, so this only works half of the time.

from selenium import webdriver
from selenium.common.exceptions import NoSuchElementException
import json
import time
from urllib.parse import urlencode

with open('data.json') as f:
    data = json.load(f)

driver = webdriver.Firefox()
driver.implicitly_wait(5)
driver.get('https://www.linkedin.com')

username = driver.find_element_by_id('login-email')
username.send_keys('email')
password = driver.find_element_by_id('login-password')
password.send_keys('password')
sign_in_button = driver.find_element_by_id('login-submit')
sign_in_button.click()

for name in data:
    try:
        first, last = name.split(' ', 1)
    except ValueError:
        continue
    if last.endswith('-1'):
        last = last[:-2]
    params = urlencode({"firstName": first, "lastName": last})
    driver.get("https://www.linkedin.com/search/results/people/?" + params)
    try:
        location = driver.find_element_by_css_selector('.search-result--person .subline-level-2').text
        print('"%s", "%s"' % (name, location))
    except NoSuchElementException:
        print('"%s", "%s"' % (name, 'unknown'))
        continue

And finally some quick Bash hax to count the countries. (All US locations only list their state)

cat output.csv | cut -d\" -f 4 | sed "s/Area$/Area, United States/i" | awk -F, '{print $NF}' | awk '{$1=$1};1' | sort | uniq -c
Pepijn de Vos