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
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!
