SymbiYosys tutorial · Chapter 5 of 10 · 15 min
Verify the wb2axip skid buffer
ZipCPU's wb2axip repository contains AXI bus components by Dan Gisselquist, each with SymbiYosys proofs. This chapter proves its skid buffer and explains two techniques from its job file and its formal properties.
What does a skid buffer do?
A skid buffer is a circuit that holds one transfer of a valid/ready handshake, so that the sender can be stalled one cycle late without losing data. In a valid/ready handshake, the sender raises valid when it has data, and the transfer happens in a cycle in which the receiver also has ready high.
The comments in rtl/skidbuffer.v explain why AXI designs need one: high-throughput AXI code registers its outputs, so a stall from downstream reaches the upstream side one cycle later. The skid buffer stores the transfer that arrives in that cycle. The figure shows its ports.
The skid buffer's ports. i_ signals are inputs and o_ signals are outputs; r_valid and r_data are the internal buffer.Get the wb2axip repository
Clone the repository and check out the commit this chapter uses, so that your results match the output below:
$ cd ~/formal
$ git clone https://github.com/ZipCPU/wb2axip
$ cd wb2axip
$ git checkout 2e8d3bc
At this commit the repository has 63 Verilog files in rtl/ and 42 job files in bench/formal/. The components are licensed under the Apache License 2.0.
Run the skid buffer proofs
$ cd bench/formal
$ sby -f skidbuffer.sby
output (summary lines)
SBY 23:14:46 [skidbuffer_prfc] summary: successful proof by k-induction.
SBY 23:14:46 [skidbuffer_prfc] DONE (PASS, rc=0)
SBY 23:14:46 [skidbuffer_prfo] summary: successful proof by k-induction.
SBY 23:14:46 [skidbuffer_prfo] DONE (PASS, rc=0)
SBY 23:14:46 [skidbuffer_lpc] summary: successful proof by k-induction.
SBY 23:14:46 [skidbuffer_lpc] DONE (PASS, rc=0)
SBY 23:14:46 [skidbuffer_lpo] summary: successful proof by k-induction.
SBY 23:14:46 [skidbuffer_lpo] DONE (PASS, rc=0)
SBY 23:14:46 [skidbuffer_cvr] DONE (PASS, rc=0)
The job runs five tasks in about one second: four unbounded proofs, each completed by k-induction, and one cover task.
How does one job file prove four parameter combinations?
The skid buffer has two options. OPT_OUTREG registers its outputs, and OPT_LOWPOWER forces the data outputs to zero whenever their valid signal is low. The four proof tasks cover the four combinations:
skidbuffer.sby
[tasks]
prfc prf
prfo prf opt_outreg
lpc prf opt_lowpower
lpo prf opt_lowpower opt_outreg
cvr
[options]
prf: mode prove
prf: depth 12
cvr: mode cover
cvr: depth 20
[engines]
smtbmc
[script]
read -define SKIDBUFFER
read -formal skidbuffer.v
--pycode-begin--
cmd = "hierarchy -top skidbuffer"
cmd += " -chparam OPT_LOWPOWER %d" % (1 if "opt_lowpower" in tags else 0)
cmd += " -chparam OPT_OUTREG %d" % (1 if "opt_outreg" in tags else 0)
output(cmd);
--pycode-end--
prep -top skidbuffer
[files]
../../rtl/skidbuffer.v
- Each task line names a task and its tags:
lpo prf opt_lowpower opt_outreg defines the task lpo with three tags. - The block between
--pycode-begin-- and --pycode-end-- is Python that sby runs for each task. It reads the task's tags and outputs one hierarchy command that sets both parameters with -chparam. - The result is one job file that proves every parameter combination, instead of four copies of the same file.
Why do the input rules switch between assume and assert?
The skid buffer's formal properties include rules about its inputs, for example: once i_valid is high and the buffer is stalled, i_valid stays high and i_data stays stable. The file writes these rules with a macro instead of assume:
rtl/skidbuffer.v (lines 244–272, shortened)
`ifdef FORMAL
`ifdef SKIDBUFFER
`define ASSUME assume
`else
`define ASSUME assert
`endif
...
always @(posedge i_clk)
if (!f_past_valid)
begin
`ASSUME(!i_valid || !OPT_INITIAL);
end else if ($past(i_valid && !o_ready && !i_reset) && !i_reset)
`ASSUME(i_valid && $stable(i_data));
- When the skid buffer is proved on its own, the job runs
read -define SKIDBUFFER, so ASSUME means assume: the proof assumes the sender follows the handshake rules. - When the skid buffer is part of a larger design,
SKIDBUFFER is not defined, so ASSUME means assert: the proof checks that the surrounding design follows the rules. Chapter 6 uses this.
The same file also contains concurrent SVA versions of some rules, inside `ifdef VERIFIC. The free front end does not define VERIFIC, so Yosys compiles only the immediate assertions, which state the same rules.
Run sby from the folder that holds the job file
[files] names ../../rtl/skidbuffer.v. sby resolves that relative path from your current folder, not from the folder of the job file. From the repository root, the same job fails:
$ cd ~/formal/wb2axip
$ sby -f bench/formal/skidbuffer.sby prfc
output (last line)
FileNotFoundError: [Errno 2] No such file or directory: '../../rtl/skidbuffer.v'