SymbiYosys tutorial · Chapter 4 of 10 · 15 min
Verify the SymbiYosys FIFO example
The OSS CAD Suite includes the FIFO example from the SymbiYosys documentation. This chapter runs it, explains its properties and its job file, and then removes the logic that keeps the FIFO's pointers consistent, so that a proof fails and produces a counterexample.
What does a FIFO do?
A FIFO (first in, first out) is a circuit that stores data and returns it in the order it was written, like a queue. This one stores up to 16 bytes. A write (wen) stores wdata at the write pointer waddr; a read (ren) returns the byte at the read pointer raddr. Both pointers wrap around after entry 15. The output count is the number of stored bytes, and full and empty report the two limits.
The design also defines what happens at those limits. Writing to a full FIFO overwrites the oldest byte and moves the read pointer; reading from an empty FIFO moves the write pointer with the read pointer. These two adjustments, rskip and wskip, keep the pointers consistent with count.
Copy the example out of the suite
Copy the example out of the suite and work on the copy. sby creates its work folders in the current folder, and the suite's own folder should stay unchanged.
$ cp -r ~/tools/oss-cad-suite/examples/fifo ~/formal/
$ cd ~/formal/fifo
$ ls
output
fifo.sby
fifo.sv
fifo_extra_tests.sby
golden
noskip.gtkw
What does the example check?
The formal block of fifo.sv gives every assertion and cover a label, such as a_count_diff: assert (...). sby uses the label in its log, so a failure reads Assert failed in fifo: a_count_diff instead of a generated name such as _witness_.check_counter_sv_39_assert_6 from Chapter 3, Run 2. The main properties are:
| Label | Kind | What it states |
|---|
a_oflow | assert | count never exceeds 16. |
a_count_diff | assert | count equals the distance from the read pointer to the write pointer, or is 16 when the pointers are equal. |
a_counts | assert | count changes by at most 1 per cycle. |
a_full, a_empty | assert | full implies count is 16; empty implies count is 0. |
w_full, w_empty | cover | The FIFO can become full and can become empty. |
w_underfill, w_overfill | cover | A pointer moves in a cycle after its enable was low, which only the two adjustments cause. |
The file also shows how to rewrite an SVA property for the free front end. w_underfill is written twice: as a concurrent SVA property when the Verific front end is available, and as an immediate cover with one helper register otherwise. With read -formal, the macro VERIFIC is not defined, so Yosys compiles the second form.
fifo.sv (lines 152–180, shortened)
`ifdef VERIFIC
property write_skip;
@(posedge clk) disable iff (rst)
!wen |=> $changed(waddr);
endproperty
w_underfill: cover property (write_skip);
`else // !VERIFIC
reg past_nwen;
initial past_nwen <= 0;
always @(posedge clk) begin
if (rst) past_nwen <= 0;
if (!rst) begin
w_underfill: cover (past_nwen && $changed(waddr));
past_nwen <= !wen;
end
end
`endifRun the default tasks
$ sby fifo.sby
output (DONE lines)
SBY 23:14:45 [fifo_cover] DONE (PASS, rc=0)
SBY 23:14:45 [fifo_basic] DONE (PASS, rc=0)
Two tasks run. basic is a bounded check of 20 cycles, and every assertion holds. cover reaches every cover statement. The file fifo_cover/PASS lists the trace that reaches each one. For example, w_full needs 15 stored bytes and a further write, and it is reached at step 16.
How do task tags and default tasks work?
fifo.sby
[tasks]
basic bmc
nofullskip prove
cover
noverific cover
basic cover : default
[options]
cover:
mode cover
--
prove:
mode prove
--
bmc:
mode bmc
--
[engines]
smtbmc boolector
[script]
nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
read -formal fifo.sv
prep -top fifo
[files]
fifo.sv
- Tags. In
[tasks], the line nofullskip prove defines the task nofullskip and gives it the tag prove. A line or block written for a tag applies to every task with that tag, so prove: sets mode prove for nofullskip. - Blocks. A line ending in a colon, such as
cover:, starts a block that applies to that task or tag and ends at --. - Default tasks. The line
basic cover : default adds the tag default to basic and cover. Run without task names, sby runs only the tasks tagged default; without that line it would run all four. noverific. This task runs read -noverific first, which makes the following read commands skip the Verific front end that only Tabby CAD Suite has. With the free tools it reaches the same covers at the same steps as cover.
sby --dumptasks fifo.sby lists all tasks, and sby --dumpdefaults fifo.sby lists the default ones.
Remove the pointer protection and find the bug
The nofullskip task defines NO_FULL_SKIP, which sets rskip and wskip to 0 and so removes both pointer adjustments. It then attempts an unbounded proof:
$ sby -f fifo.sby nofullskip
output (excerpt)
SBY 23:14:31 [fifo_nofullskip] engine_0.basecase: ## 0:00:00 Assert failed in fifo: a_count_diff
SBY 23:14:31 [fifo_nofullskip] engine_0.basecase: Status returned by engine for basecase: FAIL
SBY 23:14:31 [fifo_nofullskip] summary: engine_0 (smtbmc boolector) returned FAIL for basecase
SBY 23:14:31 [fifo_nofullskip] summary: counterexample trace [basecase]: fifo_nofullskip/engine_0/trace.vcd
SBY 23:14:31 [fifo_nofullskip] summary: failed assertion fifo.a_count_diff at fifo.sv:106.13-107.71 step 2
SBY 23:14:31 [fifo_nofullskip] DONE (FAIL, rc=2)
SBY 23:14:31 The following tasks failed: ['nofullskip']
This time the base case fails. Unlike the UNKNOWN in Chapter 3, Run 4, this is a real counterexample: a sequence of inputs from the initial state that breaks a_count_diff at step 2.
Read the counterexample
Open the trace with the signal layout that ships with the example:
$ gtkwave fifo_nofullskip/engine_0/trace.vcd noskip.gtkw
trace.vcd. In step 0, ren is high while the FIFO is empty. The read pointer moves to 1, the count stays 0, and the pointers are now 15 entries apart.The solver read from the empty FIFO. With wskip removed, the read moves the read pointer but not the write pointer, and the count stays 0 because nothing was stored. addr_diff, the distance between the pointers, becomes 15 while count is 0, so a_count_diff fails. The design's original wskip logic prevents exactly this case.