SymbiYosys tutorial · Chapter 10 of 10 · 15 min

Read the results and fix common errors

This chapter is a reference for reading a SymbiYosys run. It explains each verdict in each mode, the files sby writes, three ways to read a trace, and the cause and fix of every error that appears in this tutorial.

What does the DONE line mean?

The last line of every task has the form DONE (VERDICT, rc=N). The return code is also sby's exit status, so a script or a Makefile can test it without reading the log. The table lists the five verdicts:

Line	Exit status	Meaning	File to open next
`DONE (PASS, rc=0)`	0	bmc: no assertion fails within the depth. prove: no assertion fails in any cycle. cover: every `cover` statement was reached.	cover: `engine_0/trace*.vcd`
`DONE (FAIL, rc=2)`	2	An assertion fails on a trace from reset (a bmc failure or a failed base case), or a `cover` statement cannot be reached within the depth.	`engine_0/trace.vcd`
`DONE (UNKNOWN, rc=4)`	4	prove with k-induction: the base case passed and the induction step failed. This is not necessarily a bug.	`engine_0/trace_induct.vcd`
`DONE (TIMEOUT, rc=8)`	8	The engine ran longer than the `timeout` option, in seconds, allows.	`logfile.txt`
`DONE (ERROR, rc=16)`	16	The task did not run: a missing file, a syntax error or an invalid job file.	The `ERROR:` line above it

When a job file has several tasks, sby prints one DONE line per task, then The following tasks failed: [...] if any task did not pass. Tasks that ended UNKNOWN appear in that list too.

Why does an UNKNOWN need a closer look than a FAIL?

A FAIL describes reachable behaviour: its trace starts from reset, and you can replay it. An UNKNOWN's trace starts from a state the solver chose. Before changing the design, check whether that starting state can occur. In Chapter 3, Run 5 it could not, and one helper assertion completed the proof.

What does sby write in the work folder?

Each task writes a folder named after the job file and the task. This is counter_bug/ fromChapter 3, Run 2:

File or folder	Contents
`FAIL`	The verdict, as a file name; the file holds the summary.
`config.sby`	This task's job, with the other tasks removed.
`counter_bug.xml`	A JUnit XML report, for CI systems.
`logfile.txt`	The full log of the run.
`status, status.path`	sby's status database.
`src/`	Copies of the files listed in [files].
`model/`	The Yosys scripts, their logs and the exported models.
`engine_0/logfile.txt`	The engine's own log.
`engine_0/trace.vcd`	The counterexample waveform.
`engine_0/trace.yw`	The same trace as a Yosys witness file.
`engine_0/trace_tb.v`	A Verilog testbench that replays the trace.
`engine_0/trace.smtc`	The trace as smtbmc constraints.

An induction failure writes the same files with trace_induct in their names. A cover task writes trace0.vcd, trace1.vcd and so on, one per cover statement reached. The verdict file is the simplest thing for a script to check, for example test -e counter_bmc/PASS. The XML file lets a CI system, such as GitHub Actions, show each property as a test case.

How do you view or replay a trace?

Open the trace in a waveform viewer

$ cd ~/formal/counter
$ gtkwave counter_bug/engine_0/trace.vcd

Add the signals you need to the waveform view. GTKWave can save that layout as a .gtkw file, which it loads as a second argument; the FIFO example's noskip.gtkw in Chapter 4 is one. One step of an sby trace is one clock cycle.

Print the trace as text

On a machine without a desktop, yosys-witness prints the starting state and the inputs that the solver chose at each step:

$ yosys-witness display counter_bug/engine_0/trace.yw

output (first lines)

Reading Yosys witness trace 'counter_bug/engine_0/trace.yw'...
*** RTLIL bit-order below may differ from source level declarations ***
=== Clock Signals ===
  posedge clk[0]
=== Initial State ===
  #0 clk[0] = 0
  #0 en[0] = 0
  #0 rst[0] = 1
  #0 count[3:0] = 0000
  #0 tc[0] = 0
=== Step 1 ===
  #1 clk[0] = 0
  #1 en[0] = 1
  #1 rst[0] = 0

Replay the trace in simulation

trace_tb.v drives the design with the trace's inputs, which turns the failure into an ordinary simulation to which you can add $display statements. Compile it with the task's macros and with FORMAL: the testbench sets the formal-only register f_past_valid, so it does not compile without FORMAL.

$ iverilog -g2012 -DFORMAL -DBUG -o replay counter.sv counter_bug/engine_0/trace_tb.v
$ vvp -n replay +vcd=replay.vcd

output

ERROR: counter.sv:31:
       Time: 0  Scope: testbench.UUT
VCD info: dumpfile replay.vcd opened for output.
ERROR: counter.sv:39:
       Time: 65  Scope: testbench.UUT

The second error is the counterexample: Icarus Verilog evaluates the assertion on line 39, and it fails at time 65, in the seventh clock cycle, which is step 6. The first error does not indicate a problem. It is the initial assume (rst) on line 31, evaluated at time 0, before the testbench drives rst at time 1. replay.vcd holds the replayed waveform.

How do you fix common errors?

The table lists every error in this tutorial, its cause and its fix.

Message or symptom	Cause	Fix
`ERROR: Directory '…' already exists, use -f to overwrite the existing directory.`	An earlier run left its work folder.	Add `-f`: `sby -f job.sby task`.
`FileNotFoundError: [Errno 2] No such file or directory`	sby resolves relative paths in `[files]` from the current folder.	`cd` into the folder that contains the `.sby` file.
ERROR: File `x.sv' not found, then `DONE (ERROR, rc=16)`	A file named in `[script]` is missing from `[files]`, or misspelled.	List every file the script reads under `[files]`.
`syntax error, unexpected '@'` on an `assert property` line	`read -formal` does not accept concurrent assertions.	Write an immediate assertion in a clocked block with `$past` (Chapter 1, “Which properties can the free tools check?”).
`encountered unsupported SVA feature`	`read_slang` does not accept sequence operators such as `\|->` and `##`.	Express the sequence with registers and immediate assertions, or use Tabby CAD Suite.
An assertion fails, or a cover is reached, at step 0	Registers start with arbitrary values before the first clock edge.	Guard the checks with `f_past_valid` (Chapter 3, “What must every formal block contain?”).
A failure at step 1 from a state that reset never produces	The proof does not start in reset.	`initial assume (rst);`
`DONE (UNKNOWN, rc=4)`	The k-induction step started from a state that reset cannot reach.	Read `trace_induct.vcd`; add a helper assertion, or try `abc pdr` (Chapter 3, Run 6).
`DONE (TIMEOUT, rc=8)`	The engine needed longer than the `timeout` option allows.	Raise the timeout, lower the depth, or try another engine.
`DONE (FAIL, rc=0)`	The job file sets `expect` to accept FAIL.	Read the DONE line or the summary file, not only the exit status.
A property about asynchronous reset behaves unexpectedly	sby converts asynchronous logic to synchronous logic (`async2sync`).	Add `multiclock on` to `[options]`, so sby models clocks and asynchronous events explicitly.
A cover PASS on a design that violates an assertion	Cover mode does not check assertions.	Check assertions in a bmc or prove task.
A `Latch inferred` warning	Yosys found a value held in an `always @*` block; in NERV, `for` loop variables.	For loop variables, no action is needed. For other signals, check the combinational logic.
`awk: line 2: function gensub never defined`	Ubuntu's default `awk` is `mawk`.	`sudo apt install -y gawk`, then `bash cexdata.sh` (Chapter 7).
Install errors: an empty download, `command not found`, `GLIBC_2.43`	Each has its own cause.	See Chapter 2, “How do you fix install errors?”.

Where should you go next?

You can now install the tools, run every mode, verify real designs and read what the tools report. To continue:

Practise with graded exercises in the browser. The Hardware Formal Verification course continues from this tutorial with katas that run on formal.org's proof runner. The AXI Formal Verification course works through the wb2axip components from Chapters 5 and 6.
Learn how the engines work. Decision Procedures for Hardware Formal Verification covers SAT, SMT, BMC, k-induction and IC3/PDR.
Read the reference. The .sby file reference in the SymbiYosys documentation lists every section and option.