SymbiYosys tutorial · Chapter 3 of 10 · 35 min

Run your first proofs on a counter

This chapter runs six SymbiYosys jobs on a counter that counts from 0 to 9. The first job checks a fixed number of cycles. The second finds a bug injected into the design. The third shows that the counter reaches its last value. The last three prove a property for every cycle, first without and then with a helper assertion. Each job finishes in under a second.

Create the counter design

Create a folder for the project. In a new terminal, activate the suite first (Chapter 2, Step 3).

$ mkdir -p ~/formal/counter
$ cd ~/formal/counter

Save the following file as counter.sv. The counter has an enable input en and a flag tc (terminal count) that is high exactly when count is 9. The design stores tc in its own flip-flop, so the wrap-around test reads one bit instead of comparing four.Run 4 shows why this choice makes the proof harder.

counter.sv

// Modulo-10 counter with a registered terminal-count flag.
// tc is high exactly when count is 9, so the wrap test is one flip-flop.
module counter (
    input  wire       clk,
    input  wire       rst,
    input  wire       en,
    output reg  [3:0] count,
    output reg        tc
);
    always @(posedge clk) begin
        if (rst) begin
            count <= 4'd0;
            tc    <= 1'b0;
        end else if (en) begin
            if (tc) begin
                count <= 4'd0;
                tc    <= 1'b0;
            end else begin
`ifdef BUG
                count <= count + 4'd2;   // injected bug: skips values
`else
                count <= count + 4'd1;
`endif
                tc    <= (count == 4'd8);
            end
        end
    end

`ifdef FORMAL
    // Start in reset.
    initial assume (rst);

    // Registers hold arbitrary values until the first clock edge
    // applies the reset, so check properties only after that edge.
    reg f_past_valid = 1'b0;
    always @(posedge clk) f_past_valid <= 1'b1;

    // Safety property: the counter never leaves 0..9.
    always @(*) if (f_past_valid) assert (count <= 4'd9);

`ifdef HELPER
    // Helper invariant: tc agrees with count.
    always @(*) if (f_past_valid) assert (tc == (count == 4'd9));
`endif

    // Reachability: the counter can reach its terminal count.
    always @(*) if (f_past_valid) cover (tc);
`endif
endmodule

Lines 19 to 23 contain a deliberate bug, compiled only when the macro BUG is defined: the counter then adds 2 instead of 1. The bug task in the job file defines it.

What must every formal block contain?

The code between `ifdef FORMAL and the last `endif exists only for the proof. Three of its parts are needed in almost every design. Each item below states what fails without it.

`ifdef FORMAL. read -formal defines FORMAL, so the properties are compiled for the proof and excluded from synthesis and simulation.
initial assume (rst); starts the proof in reset. Without it, the solver may start in any state with rst low, and both the assertion and the cover are decided at step 1 from a state that no start-up produces.
f_past_valid. In the formal model every register starts with an arbitrary value, and the reset takes effect only at the first clock edge. Without the guard, the assertion fails at step 0 with count = 12, and the cover is reached at step 0 from an arbitrary starting state. Both results describe the moment before reset has any effect.

Create the job file

Save the following file as counter.sby. It defines five tasks. A line that starts with a task name and a colon applies only to that task; every other line applies to all tasks.

counter.sby

[tasks]
bmc
cover
prove_weak
prove
bug

[options]
bmc: mode bmc
bmc: depth 20
cover: mode cover
cover: depth 20
prove_weak: mode prove
prove: mode prove
bug: mode bmc
bug: depth 20

[engines]
smtbmc

[script]
bmc:        read -formal counter.sv
cover:      read -formal counter.sv
prove_weak: read -formal counter.sv
prove:      read -formal -DHELPER counter.sv
bug:        read -formal -DBUG counter.sv
prep -top counter

[files]
counter.sv

The program that reads each section of the job file. Chapter 1, “How does a proof run, step by step?” shows the same steps as a flow.

sby counter.sby runs all five tasks; sby counter.sby bmc runs one. Each task writes its own work folder: counter_bmc/, counter_bug/, and so on.

Run 1. Check the first 20 cycles with bmc

$ sby -f counter.sby bmc

output (last lines)

SBY 23:10:17 [counter_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 23:10:17 [counter_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 23:10:17 [counter_bmc] summary: engine_0 (smtbmc) returned pass
SBY 23:10:17 [counter_bmc] summary: engine_0 did not produce any traces
SBY 23:10:17 [counter_bmc] DONE (PASS, rc=0)

Every task ends with a DONE line; read it first. PASS in bmc mode means that no assertion can fail in the first 20 cycles after reset, for any sequence of en values. It makes no claim about cycle 21 or later.

The -f option deletes the work folder of an earlier run before starting. Without it, sby refuses to overwrite the folder:

$ sby counter.sby bmc

output

ERROR: Directory 'counter_bmc' already exists, use -f to overwrite the existing directory.

Run 2. Find the injected bug and read the counterexample

The bug task reads the design with -DBUG, which compiles the add-by-2 bug:

$ sby -f counter.sby bug

output (excerpt)

SBY 23:10:17 [counter_bug] engine_0: ##   0:00:00  BMC failed!
SBY 23:10:17 [counter_bug] engine_0: ##   0:00:00  Assert failed in counter: counter.sv:39.35-39.57 (_witness_.check_counter_sv_39_assert_6)
SBY 23:10:17 [counter_bug] summary: counterexample trace: counter_bug/engine_0/trace.vcd
SBY 23:10:17 [counter_bug] summary:   failed assertion counter._witness_.check_counter_sv_39_assert_6 at counter.sv:39.35-39.57 step 6
SBY 23:10:17 [counter_bug] DONE (FAIL, rc=2)
SBY 23:10:17 The following tasks failed: ['bug']

Read the output from the bottom up:

DONE (FAIL, rc=2): an assertion can fail. This is a bug that the design can reach from reset.
counter.sv:39.35-39.57: the failing assertion is on line 39, columns 35 to 57, which is assert (count <= 4'd9).
step 6: the assertion fails six clock cycles after the start.
counter_bug/engine_0/trace.vcd: the waveform of the failure.

Open the waveform with gtkwave counter_bug/engine_0/trace.vcd, and add clk, rst, en, count and tc to the waveform view. The figure shows the same trace.

The counterexample from trace.vcd. Reset is high in step 0; en is high from step 1. The counter takes the values 0, 2, 4, 6 and 8, and at step 6 it holds 10, which violates count <= 9.

The faulty counter holds only even values, so from 8 it adds 2 and reaches 10 without passing through 9. bmc checks the steps in order, so step 6 is the earliest step at which any input sequence breaks the assertion. The solver found that sequence without being given test inputs.

Run 3. Show that the counter reaches 9 with cover

An assertion that never fails proves nothing if the design never does anything. A cover statement asks whether the design can reach a condition. Line 47 covers tc.

$ sby -f counter.sby cover

output (excerpt)

SBY 23:10:18 [counter_cover] engine_0: ##   0:00:00  Reached cover statement in step 10 at counter: counter.sv:47.35-47.45 (_witness_.check_counter_sv_47_cover_9)
SBY 23:10:18 [counter_cover] summary: cover trace: counter_cover/engine_0/trace0.vcd
SBY 23:10:18 [counter_cover] DONE (PASS, rc=0)

The cover trace from trace0.vcd: reset, then en high for nine cycles. tc rises in step 10, the earliest step at which it can.

A cover also tests your assumptions. If a cover that should pass fails, an assumption excludes behaviour the design should have, and every assertion then passes in a set of states that is too small to matter.

Run 4. Try to prove the property for all time

bmc checks a fixed number of cycles. mode prove tries to show that the assertion holds in every cycle. With smtbmc, the proof uses k-induction, which has two parts:

Base case: no assertion fails in the first k cycles after reset. This is a bmc check, with k set by depth (20 by default).
Induction step: from any k consecutive states in which the assertions hold, the next state also satisfies them. "Any" includes states that reset can never produce.

$ sby -f counter.sby prove_weak

output (excerpt)

SBY 23:10:18 [counter_prove_weak] engine_0.induction: ##   0:00:00  Temporal induction failed!
SBY 23:10:18 [counter_prove_weak] engine_0.induction: ##   0:00:00  Assert failed in counter: counter.sv:39.35-39.57 (_witness_.check_counter_sv_39_assert_6)
SBY 23:10:18 [counter_prove_weak] summary: engine_0 (smtbmc) returned pass for basecase
SBY 23:10:18 [counter_prove_weak] summary: engine_0 (smtbmc) returned FAIL for induction
SBY 23:10:18 [counter_prove_weak] summary: counterexample trace [induction]: counter_prove_weak/engine_0/trace_induct.vcd
SBY 23:10:18 [counter_prove_weak] DONE (UNKNOWN, rc=4)
SBY 23:10:18 The following tasks failed: ['prove_weak']

UNKNOWN is not a bug report, even though sby lists the task as failed. The base case passed, so no assertion fails within 20 cycles of reset. The induction step failed, so the proof is incomplete. The induction trace shows where the step started:

The last five steps of trace_induct.vcd. Steps 0 to 19 all hold count = 9 with tc = 0. en is high in step 19, so in step 20 the counter holds 10.

The solver chose the state count = 9, tc = 0. Reset never produces this state, because tc is always 1 when count is 9. The assertion states only count <= 9, which this state satisfies, so the induction step may start there. While en is low the state does not change, so a deeper induction does not help: the solver can hold the state for as many steps as the depth requires. When en rises, tc is 0, so the counter increments to 10.

The counter's 32 states. The induction step may start in any state the assertions allow; the helper assertion reduces that set to the states reset can reach.

Run 5. Add a helper assertion to complete the proof

To complete the proof, state a fact that the designer knows: tc agrees with count. That is the assertion on line 43, inside `ifdef HELPER, which the prove task enables with -DHELPER:

$ sby -f counter.sby prove

output (excerpt)

SBY 23:10:18 [counter_prove] engine_0.induction: ##   0:00:00  Temporal induction successful.
SBY 23:10:18 [counter_prove] summary: engine_0 (smtbmc) returned pass for basecase
SBY 23:10:18 [counter_prove] summary: engine_0 (smtbmc) returned pass for induction
SBY 23:10:18 [counter_prove] summary: successful proof by k-induction.
SBY 23:10:18 [counter_prove] DONE (PASS, rc=0)

The helper is an assertion, not an assumption, so the proof checks it together with the original assertion. If it were false in any state that reset can reach, the proof could not pass. A helper assertion can therefore make a proof possible, but it cannot hide a bug.

Run 6. Let IC3/PDR engines find the invariant

IC3/PDR engines construct the missing invariant themselves. Save the following file as engines.sby. It runs the design without the helper through eight engines, one task each:

engines.sby

[tasks]
yices
bitwuzla
z3
boolector
pdr
ric3
avy
suprove

[options]
mode prove

[engines]
yices:     smtbmc yices
bitwuzla:  smtbmc bitwuzla
z3:        smtbmc z3
boolector: smtbmc boolector
pdr:       abc pdr
ric3:      aiger rIC3
avy:       aiger avy
suprove:   aiger suprove

[script]
read -formal counter.sv
prep -top counter

[files]
counter.sv

$ sby -f engines.sby

output (DONE lines)

SBY 23:10:19 [engines_yices] DONE (UNKNOWN, rc=4)
SBY 23:10:19 [engines_bitwuzla] DONE (UNKNOWN, rc=4)
SBY 23:10:19 [engines_z3] DONE (UNKNOWN, rc=4)
SBY 23:10:19 [engines_boolector] DONE (UNKNOWN, rc=4)
SBY 23:10:19 [engines_pdr] DONE (PASS, rc=0)
SBY 23:10:19 [engines_avy] DONE (PASS, rc=0)
SBY 23:10:19 [engines_ric3] DONE (PASS, rc=0)
SBY 23:10:19 [engines_suprove] DONE (PASS, rc=0)

The tasks finish in parallel, so the order of the DONE lines can differ in your run. The table groups the results by algorithm:

Engine line	Algorithm	Result
`smtbmc yices`	k-induction	UNKNOWN
`smtbmc bitwuzla`	k-induction	UNKNOWN
`smtbmc z3`	k-induction	UNKNOWN
`smtbmc boolector`	k-induction	UNKNOWN
`abc pdr`	IC3/PDR	PASS
`aiger rIC3`	IC3	PASS
`aiger avy`	Interpolation combined with PDR	PASS
`aiger suprove`	super_prove, a prover built on ABC	PASS

Changing the SMT solver does not change a k-induction result. Changing the algorithm does.

Why write helper assertions when an engine can find the invariant?

A helper assertion records a fact about the design, and the proof checks it. It documents the design.
IC3/PDR has to discover every invariant itself. On larger designs that can take much longer than checking invariants you state.
When a proof ends UNKNOWN, asking whether the induction trace's starting state can occur is how you find a missing invariant, and sometimes a real bug.