Three steps instead of 4,895 cycles

In The Debug Loop the beat-counter bug, B3, took a 60-seed sweep, a probe and a hypothesis to pin down: a DMA run longer than 255 words stops early because a 10-bit length is cast into an 8-bit counter. The random test reached that corner once in 400 runs.

Now a colleague cuts the counter out of the DMA engine, writes one property, and runs a bounded model check. It fails in under a second and hands back a file called cex.vcd. What is in it, and how do you read it?

What people usually do, and why it fails

Two habits waste a counterexample. One is to read only the verdict, Assert failed, and search the RTL as if formal had only said "something is wrong". The other is to distrust the trace because it looks strange, with inputs toggling in reset and a length of 513, and to waive it as "an unrealistic case".

Both miss what a counterexample is: a legal input sequence, under your assumptions, that breaks the property in the fewest possible cycles: the best failing test you will ever get. Where it looks odd, either the oddness does not matter or an assumption is missing. Both take a minute to check. (Setting up formal belongs to the RTL course's first formal run; this lesson is about debugging with what it gives you.)

The method: a counterexample is a failing test

• Read it from reset, one step per clock. Each step is one cycle. Find the step where the assertion fails, then walk back to the first step where the design did something you did not intend: the first wrong cycle, as in any waveform.

• Separate signal from noise. In steps where an input cannot matter (in reset, while busy), the solver picks any value. Pin those inputs with assumptions and run again. If the check still fails at the same depth, they were noise.

• Move the property towards the cause. An end-of-run property fails when the damage shows. An invariant on the state that went wrong fails the cycle it goes wrong.

• Replay it in simulation. The trace is a stimulus. Drive it into the RTL, confirm the same failure, then widen it into a sweep or a directed test.

• Prove the fix with the same check, and know what a bounded pass covers.

On the debug loop this is Observe and Localise: formal does the reproducing, and the trace is what you observe.

The design and the property

beat_ctr is the counter from dbglab's dma_engine at commit 13, with the same widths: a 10-bit len, an 8-bit left_q, and the CW'() cast between them. The chunking, the FIFO and the bus are left out; beat stands for "the bus accepted one write". The formal block counts the beats of each run in seen and asserts that when done pulses, seen equals the length asked for. The same listing ends with the simulation replay used later, which the course checker runs.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

`timescale 1ns/1ps
// beat_ctr: the beat counter of dbglab's DMA engine (commit 13, bug B3), cut out with its
// widths unchanged. start loads the 10-bit length into the counter; each accepted write
// (beat) counts it down; done pulses after the last beat.
// CW = 8 is the bug: the length is cast into 8 bits. CW = 10 is the fix.
module beat_ctr #(parameter int CW = 8) (
  input  logic       clk, rst_n,
  input  logic       start,          // ignored while busy
  input  logic [9:0] len,
  input  logic       beat,           // the bus accepted one write
  output logic       busy, done
);
  logic [CW-1:0] left_q;             // words still to write
  always_ff @(posedge clk)
    if (!rst_n) begin
      busy <= 1'b0; done <= 1'b0; left_q <= '0;
    end else begin
      done <= 1'b0;
      if (!busy && start) begin
        left_q <= CW'(len);
        if (len == 10'd0) done <= 1'b1;
        else              busy <= 1'b1;
      end else if (busy && beat) begin
        left_q <= left_q - 1'b1;
        if (left_q == CW'(1)) begin busy <= 1'b0; done <= 1'b1; end
      end
    end

`ifdef FORMAL
  // The property, in words: when a run ends, it wrote exactly the words it was asked for.
  logic       past_valid = 1'b0;
  logic [9:0] len_f;                 // the length of the current run
  logic [10:0] seen;                 // beats accepted in the current run
  always_ff @(posedge clk) begin
    past_valid <= 1'b1;
    if (!rst_n) begin len_f <= '0; seen <= '0; end
    else if (!busy && start) begin len_f <= len; seen <= '0; end
    else if (busy && beat) seen <= seen + 1'b1;
  end
  always @(*) if (!past_valid) assume (!rst_n);          // start in reset
  always @(*) if (past_valid && rst_n && done) a_len: assert (seen == {1'b0, len_f});
`ifdef HELPER
  // While a run is busy, words written plus words left is the length asked for.
  always @(*) if (past_valid && rst_n && busy) a_left: assert (left_q != 0 && seen + 11'(left_q) == {1'b0, len_f});
`endif
`ifdef CLEAN
  // Trace clean-up: no back-pressure, and one run only.
  logic started = 1'b0;
  always_ff @(posedge clk) if (rst_n && start) started <= 1'b1;
  always @(*) if (past_valid) assume (beat == busy);
  always @(*) if (started) assume (!start);
`endif
`endif
endmodule

seen and len_f are formal-only bookkeeping, so the property says nothing about how the counter works inside. The one assumption is that the run starts in reset; start, len and beat are free in every step. HELPER and CLEAN are switched on with -D for two experiments below. Yosys reads the module part of the listing, saved as beat_ctr.sv.

Do it: the bounded check fails in three steps

$ yosys -q -p "read_verilog -formal -sv beat_ctr.sv; prep -top beat_ctr; async2sync; write_smt2 -wires bug.smt2"
$ yosys-smtbmc -s z3 -t 20 --dump-vcd cex.vcd bug.smt2

##   0:00:00  Solver: z3
##   0:00:00  Checking assertions in step 0..
##   0:00:00  Checking assertions in step 1..
##   0:00:00  Checking assertions in step 2..
##   0:00:00  Checking assertions in step 3..
##   0:00:00  BMC failed!
##   0:00:00  Assert failed in beat_ctr: a_len
##   0:00:00  Writing trace to VCD file: cex.vcd
##   0:00:00  Status: FAILED

The check was allowed 20 steps and needed 3. Because it checks step 0, then step 1, and so on, the first failure it reports is at the smallest depth any failure exists: no input sequence breaks a_len in fewer cycles. That is the first half of minimising, done for free.

Read the trace as a table

cex.vcd has every signal at every step. With no waveform viewer installed here, a few lines of Python print it as a table. Each row is one step; registers show their value in that step, and the inputs in a row act at the clock edge that ends it.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

# not-run: reads cex.vcd, which yosys-smtbmc writes (commands above)
# cextable.py: print a yosys-smtbmc counterexample VCD as a table, one row per solver step.
# usage: python3 cextable.py cex.vcd sig1 sig2 ...   (multi-bit values in decimal)
import sys

path, names = sys.argv[1], sys.argv[2:]
ids, rows, cur = {}, [], None
with open(path) as f:
    for line in f:
        tok = line.split()
        if not tok:
            continue
        if tok[0] == "$var" and tok[4] in names:
            ids[tok[3]] = tok[4]                     # VCD id code -> signal name
        elif tok[0].startswith("#"):
            if cur is not None and int(tok[0][1:]) % 10 == 0:
                rows.append(dict(cur))               # a step ends every 10 ns (the last edge adds none)
        elif tok[0].startswith("b") and len(tok) == 2 and tok[1] in ids:
            cur = cur or {}
            v = tok[0][1:]
            cur[ids[tok[1]]] = str(int(v, 2)) if set(v) <= {"0", "1"} else v
        elif tok[0][0] in "01xz" and len(tok[0]) > 1 and tok[0][1:] in ids:
            cur = cur or {}
            cur[ids[tok[0][1:]]] = tok[0][0]
print("step  " + "  ".join(f"{n:>7}" for n in names))
for i, r in enumerate(rows):
    print(f"{i:>4}  " + "  ".join(f"{r.get(n, '-'):>7}" for n in names))

$ python3 -I cextable.py cex.vcd rst_n start len beat busy left_q seen len_f done
step    rst_n    start      len     beat     busy   left_q     seen    len_f     done
   0        0        1      513        1        0        0        0      513        0
   1        1        1      513        1        0        0        0        0        0
   2        1        0        0        1        1        1        0      513        0
   3        1        1      513        1        0        0        1      513        1

• Step 0: reset, as assumed. start and beat are high, but nothing reacts in reset.

• Step 1: start with len = 513; the counter loads at the edge that ends the step.

• Step 2: busy is 1 and left_q is 1, not 513: the first wrong value. 513 is 0x201 and the 8-bit cast kept 0x01. A beat arrives.

• Step 3: that was the "last" beat, so done pulses with seen = 1 and len_f = 513. a_len fails, one step after the cause.

Any length whose low eight bits are 1 gives this shortest trace; 513 is simply the one the solver found. The len of 0 in step 2 is a don't-care: the counter is busy and ignores it.

The same trace as a waveform

Replayed in simulation, with a correct three-word run after it for contrast, it looks like any failing waveform:

Slot n is just after clock edge n; slots 0 to 2 are the trace's steps 1 to 3. Read left_q against len.

• Slots 0 and 1: start with len = 201 (hex, 513), then busy with left_q = 1.

• Slot 2: done after one beat, where 513 words were asked for.

• Slots 3 to 7: len = 3 counts 3, 2, 1 and finishes correctly. Short runs hide the bug.

Minimise it: pin the noise, then fail closer to the cause

Pin the noise. The raw trace has start high in reset and in step 3, and beat high when nothing is busy. The CLEAN assumptions forbid that: beats only while busy, one run only. If the depth or the failing assertion changed, one of those inputs was part of the bug.

$ yosys -q -p "read_verilog -formal -sv -DCLEAN beat_ctr.sv; prep -top beat_ctr; async2sync; write_smt2 -wires clean.smt2"
$ yosys-smtbmc -s z3 -t 20 --dump-vcd clean.vcd clean.smt2 | tail -3
##   0:00:00  Assert failed in beat_ctr: a_len
##   0:00:00  Writing trace to VCD file: clean.vcd
##   0:00:00  Status: FAILED
$ python3 -I cextable.py clean.vcd rst_n start len beat busy left_q seen len_f done
step    rst_n    start      len     beat     busy   left_q     seen    len_f     done
   0        0        0      513        0        0        0        0      513        0
   1        1        1      513        0        0        0        0        0        0
   2        1        0        0        1        1        1        0      513        0
   3        1        0      513        0        0        0        1      513        1

Same depth, same assertion, and only two input events: one start with len = 513 and one beat. Assumptions used like this are an experiment, not sign-off setup, because each one hides behaviour (assumption discipline).

Fail closer to the cause. a_len fires when the damage shows. The HELPER invariant watches the state: while busy, the counter is never 0, and words written plus words left equals the length.

$ yosys-smtbmc -s z3 -t 20 --dump-vcd bugh.vcd bugh.smt2 | tail -3      # built with -DHELPER
##   0:00:00  Assert failed in beat_ctr: a_left
##   0:00:00  Writing trace to VCD file: bugh.vcd
##   0:00:00  Status: FAILED
$ python3 -I cextable.py bugh.vcd rst_n start len beat busy left_q seen len_f done
step    rst_n    start      len     beat     busy   left_q     seen    len_f     done
   0        0        1      512        0        0        0        0        0        0
   1        1        1      512        0        0        0        0        0        0
   2        1        1      512        0        1        0        0      512        0

The trace now stops on the load itself: 512 loaded as 0, no beat needed. The stronger property names the cause, the counter's value, not the symptom, the run's length: the same move as an assertion at the point of use instead of the scoreboard.

Replay it in simulation, then generalise

The trace says "513 fails", not which other lengths fail. That is cheap to ask in simulation: replay_tb drives the trace's inputs into both counters, then runs every length from 1 to 1023:

$ iverilog -g2012 -o lf.vvp lesson_formal.sv && vvp -n lf.vvp
replay step 3: bug done=1 busy=0   fix done=0 busy=1 left_q=512
len  257: bug wrote 1 words, then done
len  258: bug wrote 2 words, then done
len  259: bug wrote 3 words, then done
len  512: bug wrote 256 words, then done
len 1023: bug wrote 255 words, then done
bug: 767 of 1023 lengths wrong (first 257, last 1023); fix: 0 wrong
PASS: the counterexample replays in simulation; every length above 256 fails with CW = 8, none with CW = 10

The first line confirms the replay matches the trace: the buggy counter is done at step 3, the fixed one still has 512 words to go. The sweep generalises it: in this model every length above 256 writes the wrong number of words, its length modulo 256 (512 wraps through 0 and writes 256), as the probe found in dbglab's real runs. Verilator 5.048 prints the same lines. The replay is now a directed test in the regression.

Fix it, and run the same check

$ yosys -q -p "read_verilog -formal -sv beat_ctr.sv; chparam -set CW 10 beat_ctr; prep -top beat_ctr; async2sync; write_smt2 -wires fix.smt2"
$ yosys-smtbmc -s z3 -t 20 fix.smt2
##   0:00:00  Solver: z3
##   0:00:00  Checking assertions in step 0..
...
##   0:00:03  Checking assertions in step 19..
##   0:00:05  Status: PASSED
$ yosys-smtbmc -s z3 -i -t 20 fix.smt2 | tail -3
##   0:00:00  Temporal induction failed!
##   0:00:00  Assert failed in beat_ctr: a_len
##   0:00:00  Status: FAILED
$ yosys-smtbmc -s z3 -i -t 20 fixh.smt2 | tail -3                      # CW = 10 with -DHELPER
##   0:00:00  Trying induction in step 19..
##   0:00:00  Temporal induction successful.
##   0:00:00  Status: PASSED

With a 10-bit counter, no run of up to 20 cycles breaks a_len, but a 1023-word run lasts a thousand cycles. Induction closes the gap only with the helper invariant; without it the solver starts from unreachable states, as your first formal run shows on a FIFO. The bounded check with the helper also passed, so both properties hold for every cycle, under the reset assumption.

What the evidence says

Formal reproduced in three steps a bug that random simulation reached once in 400 runs, because the solver searches for the failing input instead of waiting for it. Two input events matter; the rest is noise. The first wrong value is left_q the cycle after start, and the stronger property moved the failure onto that cycle. The replay showed the bug's full extent, which the trace alone did not.

Traps

Related topics

• Part 6 · Debug by Stage

• RTL: Your first formal run

• SystemVerilog: assertion debug

• The debug loop: B3 found by simulation