One cell changed, and two ways to prove it

The tag-match block below shipped with a polarity bug: it reports a hit while flush is high, not only while it is low. The netlist is frozen, so the fix goes in as an engineering change order (ECO) that changes one cell out of 16. A second one-cell change that looks just as right fails on 128 of 4,096 simulated cycles, and an equivalence run rejects it and names the failing net.

Equivalence-friendly RTL covers planning compare points, and ECO regression and release lists what to rerun. This lesson runs the two checks that carry most of the weight for a logic ECO: logical equivalence checking (LEC) of the fixed RTL against the patched netlist, then gate-level simulation (GLS).

The bug and the RTL fix

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

// Tag match unit: hit_q is 1 the cycle after a valid lookup whose tag
// matches ref_tag, unless flush is high. Bug: flush polarity is inverted.
module tag_match (
  input  wire       clk,
  input  wire       rst_n,
  input  wire       valid,
  input  wire       flush,
  input  wire [3:0] tag,
  input  wire [3:0] ref_tag,
  output reg        hit_q
);
  wire match = (tag == ref_tag);
  wire hit_d = valid & match & flush;   // bug: should be ~flush

  always @(posedge clk or negedge rst_n)
    if (!rst_n) hit_q <= 1'b0;
    else        hit_q <= hit_d;
endmodule

The RTL fix is one character:

// snippet
wire hit_d = valid & match & ~flush;  // fixed

The netlist and the one-cell ECO

Synthesis built the shipped RTL from 16 cells: six $_ORNOT_ and one $_XNOR_ for the 4-bit compare, eight $_AND_ for the AND tree, and one flop. The ECO engineer looks for the cell where flush enters. It is _16_, an AND of flush and valid whose output _02_ joins the compare in the AND tree.

\$_AND_  _16_ (
    .A(flush),
    .B(valid),
    .Y(_02_)
  );

The fix swaps it for an AND-NOT cell (Y = A & ~B) and swaps the pins, so flush lands on the inverted input. That is the whole diff against the golden netlist:

43,45c43,45
<   \$_AND_  _16_ (
<     .A(flush),
<     .B(valid),
---
>   \$_ANDNOT_  _16_ (
>     .A(valid),
>     .B(flush),

Read each row as one version of the same cell: its type, its two pins, and the function it gives _02_.

• Golden: _02_ = flush & valid, exactly the shipped bug, so this netlist matches the buggy RTL.

• ECO: the cell type changes and the pins swap, so _02_ = valid & ~flush, the fixed RTL.

• Wrong ECO: a NAND looks like adding the missing NOT, but it inverts the whole product, so valid is inverted too.

Proving the ECO with an equivalence run

The gold design is the fixed RTL; the gate design is the patched netlist. The script pairs them by name, proves every pair, and exits with an error if any pair is left unproven.

read_verilog tag_match_fixed.v
prep -top tag_match
rename tag_match gold
design -stash gold
read_verilog -icells eco_netlist.v
prep -top tag_match
rename tag_match 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

5. Executing EQUIV_MAKE pass (creating equiv checking module).
Presumably equivalent wires: clk_gold (\clk_gold), clk_gate (\clk_gate) -> clk
Presumably equivalent wires: flush_gold (\flush_gold), flush_gate (\flush_gate) -> flush
Presumably equivalent wires: hit_d_gold (\hit_d_gold), hit_d_gate (\hit_d_gate) -> hit_d
Presumably equivalent wires: hit_q_gold (\hit_q_gold), hit_q_gate (\hit_q_gate) -> hit_q
...
Changing input D of cell hit_q_reg_gate ($_DFF_PN0_): \hit_d_gate -> \hit_d
Changing input D of cell $procdff$11_gold ($adff): \hit_d_gold -> \hit_d
...
8. Executing EQUIV_SIMPLE pass.
Found 2 unproven $equiv cells (2 groups) in equiv:
  Trying to prove $equiv for \hit_q:ezsat
 success!
  Trying to prove $equiv for \hit_d:ezsat
 success!
Proved 2 previously unproven $equiv cells.
...
10. Executing EQUIV_STATUS pass.
Found 2 $equiv cells in equiv:
  Of those cells 2 are proven and 0 are unproven.
  Equivalence successfully proven!

Read the log from the top:

• equiv_make pairs wires that have the same name in both designs. The inputs pair up, and so do hit_d and hit_q: those two are the compare points.

• The two Changing input D lines cut both flops at hit_d. Each flop now reads the same net, so the proof splits into the logic before the flop and the flop itself.

• equiv_simple proves each compare point with a SAT solver, which covers all 1,024 combinations of the ten data inputs at once. equiv_status -assert turns any unproven point into a failing exit code, so a script or a CI job can gate on it.

A wrong ECO and how to find the failing point

Now apply the plausible mistake: change the AND to a NAND and leave the pins alone. Only line 43 of the netlist changes. The same script fails:

8. Executing EQUIV_SIMPLE pass.
Found 2 unproven $equiv cells (2 groups) in equiv:
  Trying to prove $equiv for \hit_q:ezsat
 success!
  Trying to prove $equiv for \hit_d:ezsat
 failed.
Proved 1 previously unproven $equiv cells.
...
  Trying to prove $equiv for \hit_d: failed.
Proved 0 previously unproven $equiv cells.

10. Executing EQUIV_STATUS pass.
ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'.
Found 2 $equiv cells in equiv:
  Of those cells 1 are proven and 1 are unproven.
  Unproven $equiv $auto$equiv_make.cc:295:find_same_wires$12: \hit_d_gold \hit_d_gate

hit_q still proves, because both flops were cut at the same hit_d. The unproven point is hit_d, named as a gold and gate pair, so the debug starts in its input cone and not in the whole block. On a large netlist that localisation is what makes the fix fast. To see the failing input, build a miter of the two designs and ask the solver for a two-cycle counterexample:

miter -equiv -flatten -make_outputs gold gate miter
hierarchy -top miter
sat -verify -prove trigger 0 -set-init-zero -seq 2 -show-inputs -show-outputs miter

SAT proof finished - model found: FAIL!
...
  Time Signal Name                                                   Dec       Hex           Bin
  ---- ----------------------------------------------------- ----------- --------- -------------
...
     1 \in_flush                                                       0         0             0
     1 \in_ref_tag                                                     8         8          1000
     1 \in_rst_n                                                       1         1             1
     1 \in_tag                                                         8         8          1000
     1 \in_valid                                                       0         0             0
...
     2 \gate_hit_q                                                     1         1             1
     2 \gold_hit_q                                                     0         0             0

In step 1 valid is 0, flush is 0 and the tags match (8 and 8). The NAND gives 1 whenever valid is 0, so the patched netlist registers a hit for a lookup that never happened: gate_hit_q is 1 in step 2 while gold_hit_q is 0.

Gate-level simulation of the patched netlist

Equivalence proves the function. GLS runs the block's RTL testbench on the netlist, with the synthesis tool's cell models in place of the RTL. The bench applies every input combination four times and checks hit_q against valid & ~flush & match after each edge.

iverilog -g2005 -o gls.vvp tb_tag_match.v eco_netlist.v $(yosys-config --datdir)/simcells.v
vvp -n gls.vvp

== tag_match_fixed.v
before reset: hit_q = x
in reset:     hit_q = 0
PASS: 4096 cycles, 64 hits, hit_q matches valid & ~flush & match
== eco_netlist.v
before reset: hit_q = x
in reset:     hit_q = 0
PASS: 4096 cycles, 64 hits, hit_q matches valid & ~flush & match
== eco_wrong_netlist.v
before reset: hit_q = x
in reset:     hit_q = 0
MISMATCH t=26000 valid=0 flush=0 tag=0 ref=0 hit_q=1 expected 0
MISMATCH t=196000 valid=0 flush=0 tag=1 ref=1 hit_q=1 expected 0
MISMATCH t=366000 valid=0 flush=0 tag=2 ref=2 hit_q=1 expected 0
FAIL: 128 mismatches in 4096 cycles

The fixed RTL and the ECO netlist agree on every cycle. The wrong ECO fails on 128 cycles: the 32 combinations with valid low and matching tags, applied four times each. All three start at x before reset.

Here GLS repeats what LEC already proved. Its value lies in the questions LEC does not ask:

So the usual recipe for a logic ECO is: LEC passes with zero unproven points, then a short GLS run of reset and the changed function, with delays once layout is updated.

Common mistakes

An equivalence pass is only as good as its compare points and its assumptions. Tie valid to 1 in both designs, as a constraint copied from a streaming mode might, and the wrong NAND ECO passes:

Presumably equivalent wires: valid_gold (1'1), valid_gate (1'1) -> valid
...
12. Executing EQUIV_STATUS pass.
Found 2 $equiv cells in equiv:
  Of those cells 2 are proven and 0 are unproven.
  Equivalence successfully proven!

With valid fixed at 1, ~(flush & valid) is ~flush and the bug cannot show. The pairing line says so: a primary input became the constant 1'1. Compare points fail the same way: with the internal name hit_d removed from the netlist, the run found one compare point instead of two and could only report the failure at hit_q.

Testbench

The fixed RTL and the patched netlist side by side, with small models of the five generic cells the netlist uses. The bench applies all 1,024 input combinations and compares both designs against valid & ~flush & match.

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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

`timescale 1ns/1ps
// Fixed RTL: the reference for the ECO.
module tag_match (
  input  wire       clk,
  input  wire       rst_n,
  input  wire       valid,
  input  wire       flush,
  input  wire [3:0] tag,
  input  wire [3:0] ref_tag,
  output reg        hit_q
);
  wire match = (tag == ref_tag);
  wire hit_d = valid & match & ~flush;

  always @(posedge clk or negedge rst_n)
    if (!rst_n) hit_q <= 1'b0;
    else        hit_q <= hit_d;
endmodule

// Generic cell models used by the netlist (same behaviour as the synthesis tool's cell library).
module \$_AND_    (input A, B, output Y); assign Y = A & B;    endmodule
module \$_ANDNOT_ (input A, B, output Y); assign Y = A & ~B;   endmodule
module \$_ORNOT_  (input A, B, output Y); assign Y = A | ~B;   endmodule
module \$_XNOR_   (input A, B, output Y); assign Y = ~(A ^ B); endmodule
module \$_DFF_PN0_ (input C, D, R, output reg Q);
  always @(posedge C or negedge R) if (!R) Q <= 1'b0; else Q <= D;
endmodule

// ECO'd gate netlist, one cell per line. The only change from the golden netlist is cell _16_.
module tag_match_eco (
  input  wire       clk,
  input  wire       rst_n,
  input  wire       valid,
  input  wire       flush,
  input  wire [3:0] tag,
  input  wire [3:0] ref_tag,
  output wire       hit_q
);
  wire _00_, _01_, _02_, _03_, _04_, _05_, _06_, _07_, _08_, _09_, _10_, _11_, _12_, _13_, hit_d;
  \$_ORNOT_  _14_ (.A(tag[2]),     .B(ref_tag[2]), .Y(_00_));
  \$_ORNOT_  _15_ (.A(ref_tag[0]), .B(tag[0]),     .Y(_01_));
  \$_ANDNOT_ _16_ (.A(valid),      .B(flush),      .Y(_02_));  // ECO: was \$_AND_ (.A(flush), .B(valid))
  \$_ORNOT_  _17_ (.A(tag[1]),     .B(ref_tag[1]), .Y(_03_));
  \$_ORNOT_  _18_ (.A(ref_tag[2]), .B(tag[2]),     .Y(_04_));
  \$_AND_    _19_ (.A(_03_),       .B(_04_),       .Y(_05_));
  \$_ORNOT_  _20_ (.A(tag[0]),     .B(ref_tag[0]), .Y(_06_));
  \$_ORNOT_  _21_ (.A(ref_tag[1]), .B(tag[1]),     .Y(_07_));
  \$_AND_    _22_ (.A(_06_),       .B(_07_),       .Y(_08_));
  \$_XNOR_   _23_ (.A(tag[3]),     .B(ref_tag[3]), .Y(_09_));
  \$_AND_    _24_ (.A(_00_),       .B(_02_),       .Y(_10_));
  \$_AND_    _25_ (.A(_09_),       .B(_10_),       .Y(_11_));
  \$_AND_    _26_ (.A(_01_),       .B(_05_),       .Y(_12_));
  \$_AND_    _27_ (.A(_08_),       .B(_12_),       .Y(_13_));
  \$_AND_    _28_ (.A(_11_),       .B(_13_),       .Y(hit_d));
  \$_DFF_PN0_ hit_q_reg (.C(clk), .D(hit_d), .Q(hit_q), .R(rst_n));
endmodule

module tb_tag_match_eco;
  reg clk = 0, rst_n = 0, valid = 0, flush = 0;
  reg [3:0] tag = 0, ref_tag = 0;
  wire hit_rtl, hit_gate;
  integer i, errors = 0, hits = 0;
  tag_match     u_rtl  (.clk(clk), .rst_n(rst_n), .valid(valid), .flush(flush), .tag(tag), .ref_tag(ref_tag), .hit_q(hit_rtl));
  tag_match_eco u_gate (.clk(clk), .rst_n(rst_n), .valid(valid), .flush(flush), .tag(tag), .ref_tag(ref_tag), .hit_q(hit_gate));
  always #5 clk = ~clk;
  initial begin
    #100000 $fatal(1, "FAIL: watchdog");
  end
  initial begin
    #12 rst_n = 1;
    for (i = 0; i < 1024; i = i + 1) begin
      @(negedge clk) {valid, flush, tag, ref_tag} = i[9:0];   // every input combination once
      @(posedge clk) #1;
      if (hit_gate !== hit_rtl || hit_rtl !== (valid & ~flush & (tag == ref_tag))) errors = errors + 1;
      if (hit_gate === 1'b1) hits = hits + 1;
    end
    if (errors == 0 && hits == 16) $display("PASS: ECO netlist matches the fixed RTL on all 1024 input combinations (16 hits)");
    else $fatal(1, "FAIL: %0d mismatches, %0d hits", errors, hits);
    $finish;
  end
endmodule

Related topics

• Equivalence-friendly RTL

• ECO regression and release

• Complete equivalence checking course

• ECO levers: sizing and buffering