"Is it proven?"

The beat-counter fix from the previous lesson is in review: CW = $bits(cfg_len) in dma_engine. Seed 10 passes. Your lead asks the question that matters before the ticket closes: is it proven? You could say "the test passes". What would you have to show for the answer to be yes?

What people usually do, and why it fails

The usual proof is the failing test plus a regression run, both green. Both draw from the same stimulus, so together they answer one question: does the design now pass the cases we already had? The cases you had are the ones that let the bug in. A sweep run only after the fix is no better: if it shows 21 failures, you cannot tell whether the fix added any of them.

And there is a deeper gap. The fix makes a claim about every length from 0 to 1023. Simulation samples; it cannot check every input unless you enumerate them. The previous lesson met a fix (CW = 9) that was wrong only above 511. Watch which rungs below can see that.

The method: four rungs, each answering one question

1. The failing test passes, in every simulator that failed. Same command, same seed. This shows the fix reaches the failing path. It does not show the fix is the cause.

2. The minimal repro passes. The shrunk test has none of the random test's noise, so a pass shows the mechanism is fixed, not that the timing moved.

3. A seed sweep, before and after, sorted by signature. The bug's signature must be gone, the other signatures unchanged, nothing new. Count how often the sweep reached the condition, not how many seeds ran; that number feeds the rule of three.

4. A formal check where the claim is "for every input". If the property is local (a register, a counter, a handshake) and its input space is wide, a bounded check plus induction on the real RTL settles in seconds what no sweep can.

Run them in this order: each is more expensive than the last and only worth running if the cheaper one passed.

The picture: three versions of the DMA up the ladder

Do it: climbing the ladder

Rung 1: the failing command, in both simulators

$ cwfix/tb/run.sh random 10
dbglab: test=random seed=10
PASS test=random seed=10 cycles=21581 time=215806 ns
$ cwfix/tb/run.sh random 10 verilator
dbglab: test=random seed=10
PASS test=random seed=10 cycles=21581 time=215806 ns

The same command that failed at cycle 4895 now runs to the end, in both simulators, with the same cycle count. Necessary, and nowhere near enough.

Rung 2: the minimal repro

Shrinking took seed 10 down to one 308-word copy from word 378 to word 711. As a directed test:

1
2
3
4
5
6
7

// not-run: a task for dbglab's bench (tb/tests.svh); it needs the bench's helpers
// dma_copy_308: the shrunk repro of random seed 10, one 308-word copy from word 378 to word 711.
task automatic t_dma_copy_308();
  csr_wr(CSR_CTRL, 32'h0);
  run_copy(378, 711, 308);
  for (int i = 0; i < 308; i++) ram_check(711 + i);
endtask

$ head/tb/run.sh dma_copy_308 1
dbglab: test=dma_copy_308 seed=1
FAIL test=dma_copy_308 seed=1 cycle=606: SCOREBOARD: RAM word 763 (address 00001bec) read 2ed308c1, expected 6a130454 (last written by DMA run #1)
$ cwfix/tb/run.sh dma_copy_308 1
dbglab: test=dma_copy_308 seed=1
PASS test=dma_copy_308 seed=1 cycles=3419 time=34186 ns

Word 763 is 711 + 52: the first word the broken copy never wrote. The repro fails at HEAD for the same reason as seed 10, in an eighth of the cycles, and passes with the fix. (The shrunk replay failed earlier, at cycle 447, mainly because its final sweep compares the RAM through the backdoor in zero time; this task reads the copied words one by one over the bus and reaches word 763 after 52 reads.) Always run the repro at HEAD too: a repro that passes before the fix proves nothing after it.

Rung 3: the sweep, before and after

Two hundred seeds, at HEAD and with the fix, in both simulators. Each sweep keeps only the FAIL lines, so the files can be compared:

1
2
3
4

for v in head cwfix; do
  (cd $v; for s in $(seq 1 200); do tb/run.sh random $s | grep FAIL; done > ../sweep200-$v.txt)
  (cd $v; for s in $(seq 1 200); do tb/run.sh random $s verilator | grep FAIL; done > ../vsweep200-$v.txt)
done

$ for v in head cwfix; do echo "$v: icarus $(wc -l < sweep200-$v.txt | tr -d " ") fail, $(grep -c xxxxxxxx sweep200-$v.txt) with X; verilator $(wc -l < vsweep200-$v.txt | tr -d " ") fail"; done
head: icarus 70 fail, 21 with X; verilator 51 fail
cwfix: icarus 21 fail, 21 with X; verilator 0 fail
$ diff <(grep xxxxxxxx sweep200-head.txt) sweep200-cwfix.txt && echo "same 21 lines"
same 21 lines

Read it as a before-and-after table, one signature at a time:

• The bug's signature is gone in both simulators: 49 and 51 failures to none.

• The other signature is unchanged, line for line. The fix did not touch B4, and it did not turn any B3 seed into a new failure.

• The simulators disagree by two seeds, and that matters. Seeds 16 and 51 fail on B3 in Verilator but on the X first in Icarus, so the Icarus sweep says nothing about B3 on them:

$ grep -E "seed=(16|51) " sweep200-head.txt
FAIL test=random seed=16 cycle=686: SCOREBOARD: RAM word 759 (address 00001bdc) read xxxxxxxx, expected 00000000 (last written by DMA run #3)
FAIL test=random seed=51 cycle=1155: SCOREBOARD: RAM word 929 (address 00001e84) read xxxxxxxx, expected 00000000 (last written by DMA run #7)
$ grep -E "seed=(16|51) " vsweep200-head.txt
FAIL test=random seed=16 cycle=12811: STREAM: word #203 = 5484683d, expected 3caa023d
FAIL test=random seed=51 cycle=11722: SCOREBOARD: RAM word 322 (address 00001508) read 15d021ca, expected 00000000 (last written by DMA run #75)

A seed that dies early on another bug never reaches yours. Verilator, which cannot see B4, runs those seeds to the end, and with the fix they pass. One more number makes the sweep honest: how often did it reach the condition at all? A probe that counts finished DMA runs longer than 255 words:

$ ../probes/probe-sweep.sh cwfix ../probes/long_runs.sv random 1 200 > long200.txt
$ awk '{n=$NF; t+=n; if ($3=="PASS") p+=n; if (n>0) s++} END {print "long runs finished:", t, " in passing seeds:", p, " seeds with one:", s}' long200.txt
long runs finished: 57  in passing seeds: 57  seeds with one: 49

Two hundred seeds, but only 57 trials of the condition. With no failure in 57, the exact bound on the per-run failure rate is 1 − 0.05^(1/57), about 5.1% at 95% confidence. Good enough to say the fix works for long runs the random test makes; useless for lengths it never makes. Finally the regression: tb/regress.sh icarus 1 2 3 prints the same nine failing runs for HEAD and the fix (diff is empty), all from three other known bugs.

Rung 4: a formal check for every length

The fix claims that the counter holds the programmed length after a start, for every LEN from 0 to 1023. That is a local property with a wide input, which is exactly where formal is cheap. Yosys 0.69 cannot parse dbglab as is, so this runs on scratch copies of dma_engine.sv (package names written out in full) and sync_fifo.sv (an early return rewritten as an assignment), with the property included under FORMAL:

1
2
3
4
5
6
7
8
9

// snippet: dma_props.svh, included at the end of the scratch copy of dma_engine for formal runs only
// The rule from the register map: after a start, the beat counter holds the programmed LEN,
// for every LEN from 0 to 1023.
  logic f_past = 1'b0;
  always @(posedge clk) f_past <= 1'b1;
  always @(*) if (!f_past) assume (!rst_n);          // the run begins in reset
  always @(posedge clk)
    if (f_past && rst_n && $past(rst_n) && $past(start && !busy))
      a_len_load: assert (left_q == $past(cfg_len));

Every input of dma_engine is free: LEN, the bus responses, dreq, start. The solver may choose any of them on any cycle.

$ cd cw9 && yosys -q -p "read_verilog -formal -sv -I.. ../dbglab_pkg.sv ../sync_fifo.sv dma_engine.sv; prep -top dma_engine; async2sync; dffunmap; write_smt2 -wires dma.smt2"
Warning: Replacing memory \mem with list of registers. See ../sync_fifo.sv:67
$ yosys-smtbmc -s z3 -t 12 --dump-vcd cex.vcd dma.smt2
...
##   0:00:00  Checking assertions in step 3..
##   0:00:00  BMC failed!
##   0:00:00  Assert failed in dma_engine: a_len_load
##   0:00:00  Writing trace to VCD file: cex.vcd
##   0:00:00  Status: FAILED
$ python3 -I ../cextable.py cex.vcd rst_n start busy cfg_len left_q
step    rst_n    start     busy  cfg_len   left_q
   0        0        0        0        4        0
   1        1        1        0      512        0
   2        1        1        1       64        0
...

That is the instance fix, CW = 9, which passed rungs 1 to 3. The solver needed three steps: reset, a start with LEN 512, and a counter holding 0. It found the length no test makes, because it does not sample; it searches. (cextable.py prints a trace one step per row, as in formal counterexamples as traces.) The real fix, after the same yosys command in its own folder:

$ cd ../cwfix && yosys-smtbmc -s z3 -t 12 dma.smt2
...
##   0:00:00  Checking assertions in step 11..
##   0:00:00  Status: PASSED
$ yosys-smtbmc -s z3 -i -t 12 dma.smt2
...
##   0:00:00  Trying induction in step 10..
##   0:00:00  Temporal induction successful.
##   0:00:00  Status: PASSED

Bounded to 12 cycles, and then by induction for every cycle: from any state where the property held on two consecutive steps, it holds on the next (the solver closed the induction at step 10 of 12, a depth of two). The property is shallow (one cycle after a start), so induction closes it without a helper invariant. For the whole check, from the Yosys run to the proof, the solver took well under a second.

What the evidence says

Each rung ruled out something different. Rung 1 showed the fix reaches the failing path; rung 2 that it fixes the mechanism; rung 3 that the whole signature is gone with nothing new, across 57 real trials of the condition and in two simulators; rung 4 that the counter loads correctly for all 1024 lengths, from any reachable state. Rungs 1 to 3 could not tell the real fix from CW = 9. Only a rung that does not depend on the stimulus could.

Write the proof down where the bug lives: the commands, the before and after counts, the formal status. That record is what lets someone trust the fix next year, and what the bug write-up is built from.

Traps

Related topics

• Part 9 · Fix, Prove, Prevent

• Next: the regression test that pins the bug

• Statistics of rare failures

• Formal counterexamples as traces

• RTL: your first formal run