"No functional change intended"

dbglab's commit 9 is a tidy-up: the register reset values move from literals in csr_block into a table in dbglab_pkg, and the message says No functional change intended. A claim like that is exactly what an equivalence check is for: compare the block before and after, and every output and register should match.

The check fails. It reports 280 points proven and 2 unproven, and ends with ERROR. The block has a register map, an interrupt and the DMA's configuration. Where do you start, and is it even a real difference?

What people usually do, and why it fails

Three habits. Rerun with more effort or a different engine, hoping the unproven points turn green. Treat it as tool noise because "it is only a refactor" and waive it. Or open both versions side by side and diff the code by eye, which for this commit means reading a package table and a reset branch and missing that one value changed.

All three throw away what the tool already did. An equivalence check that leaves two points unproven out of 282 has localised the problem to two signals, without a test, a seed or a waveform. The work left is to ask the right two questions: where exactly, and is the difference real. This lesson is about those questions. How to set up the check, pair designs and read a passing run is in the RTL course's ECO lesson, and the synthesis course covers failures in a production LEC flow.

The method: localise, separate, decide

• Read the setup before the verdict. How many compare points, and is that the number you expect? Any constant on an input, any point with no partner? A check of a different design than you meant will "fail" for reasons that have nothing to do with the change.

• Start at the unproven point nearest the inputs. Each point is proved assuming its own inputs already match. So a real difference shows at the first point it reaches, and the points it feeds usually prove, because they are compared with that difference assumed away.

• Get the input sequence that separates them. A miter of the two designs, handed to a solver, returns the shortest input sequence that makes them differ. Read it like a formal counterexample: which inputs matter, which step.

• Decide whether it is real. A real difference has a counterexample from reset. If there is none, and the unproven point's cone holds a register with no partner (added, duplicated, renamed, re-encoded), the check is missing a mapping. Add it; the mapping is then proved like any other point.

On the debug loop this is Localise and Hypothesise: the tool localises to a compare point, and the counterexample or the bounded check tests the hypothesis that the difference is real.

Do it: the refactor against the commit before it

The gold design is csr_block at commit 8, the gate is commit 9. Yosys 0.69 cannot parse dbglab's module csr_block import dbglab_pkg::*; ( header, so each version is saved as one scratch file with the package first and the import moved above the module; nothing else changes. The script is the RTL course's, pointed at the two files:

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

$ D=../dbglab                # the history built with dbglab/build-history.sh
$ git -C $D show 2e63466:rtl/csr_block.sv > csr_2e63466.sv; git -C $D show 2e63466:rtl/dbglab_pkg.sv > pkg_2e63466.sv
$ git -C $D show 026f8bf:rtl/csr_block.sv > csr_026f8bf.sv; git -C $D show 026f8bf:rtl/dbglab_pkg.sv > pkg_026f8bf.sv
$ for c in 2e63466 026f8bf; do { cat pkg_$c.sv; echo 'import dbglab_pkg::*;';
    sed 's/^module csr_block import dbglab_pkg::\*; (/module csr_block (/' csr_$c.sv; } > y_$c.sv; done
$ cat eq.ys
read_verilog -sv y_2e63466.sv
prep -top csr_block
rename csr_block gold
design -stash gold
read_verilog -sv y_026f8bf.sv
prep -top csr_block
rename csr_block gate
design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
equiv_make gold gate equiv
hierarchy -top equiv
async2sync
equiv_simple
equiv_induct
equiv_status -assert
$ yosys -s eq.ys > eq.log; echo "exit $?"

Read the setup first

5. Executing EQUIV_MAKE pass (creating equiv checking module).
...
Presumably equivalent wires: ctrl_q_gold (\ctrl_q_gold), ctrl_q_gate (\ctrl_q_gate) -> ctrl_q
...
Presumably equivalent wires: dma_ctrl_gold (\ctrl_q_gold), dma_ctrl_gate (\ctrl_q_gate) -> dma_ctrl
...
Presumably equivalent wires: irq_gold (\irq_gold), irq_gate (\irq_gate) -> irq
...
8. Executing EQUIV_SIMPLE pass.
Found 282 unproven $equiv cells (21 groups) in equiv:

Thirty-one wires pair up by name, every port and register of both versions, with no constants and nothing left over. That gives 282 single-bit compare points in 21 groups. The setup is the one intended, so a failure means the designs differ, or the check is too weak to show they do not.

Read the verdict from the first unproven point

 Grouping SAT models for \dma_ctrl:
  Trying to prove $equiv for \dma_ctrl [0]:ezsat
ezsat
 failed.
...
 Grouping SAT models for \ctrl_q:
  Trying to prove $equiv for \ctrl_q [0]:ezsat
ezsat
 failed.
...
Proved 280 previously unproven $equiv cells.

9. Executing EQUIV_INDUCT pass.
...
  Proof for induction step failed. Trying to prove individual $equiv from workset.
  Trying to prove $equiv for \ctrl_q [0]: failed.
  Trying to prove $equiv for \dma_ctrl [0]: failed.
Proved 0 previously unproven $equiv cells.

10. Executing EQUIV_STATUS pass.
ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
Found 282 $equiv cells in equiv:
  Of those cells 280 are proven and 2 are unproven.
  Unproven $equiv $auto$equiv_make.cc:258:find_same_wires$369: \dma_ctrl_gold [0] \dma_ctrl_gate [0]
  Unproven $equiv $auto$equiv_make.cc:295:find_same_wires$361: \ctrl_q_gold [0] \ctrl_q_gate [0]
exit 1

Two points out of 282, and they are the same bit: dma_ctrl is a wire driven by ctrl_q, so ctrl_q[0] is the first point and dma_ctrl[0] its copy at the port. Notice what did prove: irq uses ctrl_q[0] as the done-interrupt enable, but it is compared with ctrl_q assumed equal in both, so it proves. A real difference stops at the first point it reaches. The search is now one flip-flop bit: CTRL bit 0, the done-interrupt enable. equiv_induct failing too means the difference is not an artefact of looking only one cycle back.

Get the input that separates them

A miter joins the two designs on the same inputs and raises trigger when any output differs. The solver is asked to prove trigger stays 0 for two steps from an all-zero start:

$ sed -n '11,$p' miter.ys                 # lines 1-10 read and stash the two designs, as in eq.ys
miter -equiv -flatten -make_outputs gold gate miter
hierarchy -top miter
async2sync
sat -verify -prove trigger 0 -set-init-zero -seq 2 -show-inputs -show-outputs miter
$ yosys -s miter.ys > miter.log; grep -E "proof finished|^ +1 .(in_rst_n|in_req|in_write|in_addr|gold_dma_ctrl|gate_dma_ctrl|trigger)" miter.log
SAT proof finished - model found: FAIL!
     1 \gate_dma_ctrl                                     1         1                            00000001
     1 \gold_dma_ctrl                                     0         0                            00000000
     1 \in_addr                                          28        1c    00000000000000000000000000011100
     1 \in_req                                            1         1                                   1
     1 \in_rst_n                                          0         0                                   0
     1 \in_write                                          1         1                                   1
     1 \trigger                                           1         1                                   1

One step is enough, and in that step rst_n is 0. In reset every other input is ignored, so the request, the write and the address are don't-cares the solver filled in. The only thing that can differ in reset is a reset value: commit 8 resets CTRL to 00, commit 9 to 01. One line of the new package table says so:

// snippet: rtl/dbglab_pkg.sv at commit 9, line 39
  localparam logic [7:0]  CTRL_RST    = 8'h01;

This is dbglab's bug B1, the one that bisection in history finds by bisecting from the irq_w1c failure at HEAD, seven commits later. Here it is found at the commit itself, by the check the commit message invited, without any test. With CTRL_RST = 8'h00 the same script reports Of those cells 282 are proven and 0 are unproven and Equivalence successfully proven!.

A correct change that fails anyway

Now a second change on top of the fixed refactor, for timing: the two interrupt enables are copied into a small register ie_q placed next to the interrupt logic, so irq no longer reaches across the block for ctrl_q. The copy is written whenever CTRL is, and reset from the same table. It is correct by design. The check disagrees:

1
2
3
4
5

// snippet: the change, in csr_block
  logic [1:0]  ie_q;                      // copy of the two interrupt enables, next to irq
      scratch_q <= SCRATCH_RST; ctrl_q <= CTRL_RST; ie_q <= {CTRL_RST[CTRL_ERR_IE], CTRL_RST[CTRL_DONE_IE]}; done_q <= 1'b0;
          CSR_CTRL:    begin ctrl_q <= wdata[7:0]; ie_q <= {wdata[CTRL_ERR_IE], wdata[CTRL_DONE_IE]}; end
  assign irq      = (done_q & ie_q[0]) | (err_q & ie_q[1]);

  Trying to prove $equiv for \irq:ezsat
ezsat
 failed.
...
  Proof for induction step failed. Trying to prove individual $equiv from workset.
  Trying to prove $equiv for \irq: failed.
...
ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'.
Found 282 $equiv cells in equiv:
  Of those cells 281 are proven and 1 are unproven.
  Unproven $equiv $auto$equiv_make.cc:258:find_same_wires$530: \irq_gold \irq_gate

Same 282 points, one unproven: irq. Read the setup again and the reason is visible: ie_q exists only in the gate design, so nothing pairs with it, and irq's cone now starts at a register the check knows nothing about. equiv_simple treats its value as free, and induction fails because it may start from a state where ie_q and ctrl_q disagree, which no run from reset reaches. That is a hypothesis, so test it: look for a separating input from reset.

$ tail -1 miter_dup.ys                    # the same miter on the fixed and the duplicated versions
sat -verify -prove trigger 0 -set-init-zero -set-at 1 in_rst_n 0 -seq 12 -show-inputs -show-outputs miter
$ yosys -s miter_dup.ys > miter_dup.log; grep -E "Solving|proof finished" miter_dup.log
Solving problem with 155413 variables and 421090 clauses..
SAT proof finished - no model found: SUCCESS!

Twelve cycles from reset, any inputs, and the outputs never differ. That is evidence, not proof, so close it properly: tell the check that ie_q corresponds to ctrl_q[1:0]. In Yosys that is one equiv_add after hierarchy -top equiv:

$ grep -A2 "^hierarchy" eq_dup_map.ys
hierarchy -top equiv
cd equiv
equiv_add ctrl_q_gold[1:0] ie_q_gate
$ yosys -s eq_dup_map.ys > eq_dup_map.log; echo "exit $?"; grep -A3 "EQUIV_STATUS" eq_dup_map.log
exit 0
10. Executing EQUIV_STATUS pass.
Found 284 $equiv cells in equiv:
  Of those cells 284 are proven and 0 are unproven.
  Equivalence successfully proven!

284 points now: the 282 and the two new ones, ie_q against ctrl_q[1:0]. Those two are proved, not assumed, like every other point; had the copy been written with the wrong bits, the mapping itself would have failed. Production LEC tools report "unmapped" or "unmatched" points for exactly this case and let you map them by rule or by hand.

What the evidence says

Both failures named a single point. They differed in the one question that matters: is there an input sequence from reset that makes the designs disagree? For B1 the solver found one in a single step; for the duplicated register it found none, and the mapping turned that evidence into a proof.

Traps

Related topics

• Part 6 · Debug by Stage

• RTL: Proving an ECO with equivalence and GLS

• Synthesis: key points and black boxes

• Bisection in history: B1 found from a failing test