Two days before the freeze, a timing ECO touches one datapath and the equivalence check that passed now fails on a handful of outputs. The designer says only one mode changed; the signoff owner must decide whether that is true.
Job of this lesson: separate setup mistakes from real differences with the minimal counterexample, pin the difference to its mode, prove the intended difference, and state what equivalence does not say.
Trap | What the candidate does | Why it fails |
|---|---|---|
Debug the failure as a design bug | Reads the mismatch as wrong logic. | Most ECO mismatches are setup: reset, constants, modes or latency alignment. Setup is checked first. |
Constrain the differing mode away | Adds the mode condition and re-reports passing. | A constraint that hides a mode needs its own run per mode; one miter over all modes proves little about each. |
Claim the passing miter proves correctness | Ships on equivalence alone. | Equivalence proves the twins agree, never that either is right; the specification proof must still exist. |
A miter feeds both implementations the same inputs and asserts equal outputs every cycle. Triage starts from the failing trace: one vector, the differing bits, the earliest failing cycle. Then the setup questions in order: shared reset sequence, matched constants and black boxes, comparison aligned in time, failing case inside the intended mode. A real difference confined to that mode is covered by an intended-difference property: equal outside the mode, different exactly as specified inside it. Everything else must still prove equal, mode by mode.
The golden is the behavioural sum of two 4-bit operands. The twin is the same adder built from full-adder cells, so the miter compares two different structures. The ECO drops bit 3 of one operand from the twin. A combinational miter needs depth 2: step 0 is the reset step, step 1 the first checked step. Run A finds no counterexample to depth 4 for the unmodified twin. Run B plants the ECO: depth 1 passes, depth 2 fails. The solver returns one failing vector, not the smallest value; what is minimal is the cycle.
// formal: bmc 4 expect pass slang top adder_miter
`define FORMAL
// Lesson-local demo: behavioural adder against its ripple-carry twin; BUG=1 drops y[3] from the twin.
module adder_miter #(parameter BUG = 0, parameter DOC = 0) (
input wire clk, input wire rst, input wire [3:0] x, input wire [3:0] y, output wire same
);
wire [4:0] golden = x + y;
wire [3:0] yy = (BUG == 1) ? {1'b0, y[2:0]} : y;
wire [4:0] c; wire [3:0] s;
assign c[0] = 1'b0;
genvar i;
generate for (i = 0; i < 4; i = i + 1) begin : g_fa
assign s[i] = x[i] ^ yy[i] ^ c[i];
assign c[i+1] = (x[i] & yy[i]) | (c[i] & (x[i] ^ yy[i]));
end endgenerate
assign same = (golden == {c[4], s});
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (DOC == 0) begin : g_eq
always @(*) if (!init) a_equiv: assert (same == 1'b1);
end else begin : g_doc
always @(*) if (!init) a_doc: assert (same == !y[3]);
end endgenerate
`endif
endmodule// formal: bmc 1 expect pass slang top adder_miter define BUG=1
`define FORMAL
// Lesson-local demo: behavioural adder against its ripple-carry twin; BUG=1 drops y[3] from the twin.
module adder_miter #(parameter BUG = 0, parameter DOC = 0) (
input wire clk, input wire rst, input wire [3:0] x, input wire [3:0] y, output wire same
);
wire [4:0] golden = x + y;
wire [3:0] yy = (BUG == 1) ? {1'b0, y[2:0]} : y;
wire [4:0] c; wire [3:0] s;
assign c[0] = 1'b0;
genvar i;
generate for (i = 0; i < 4; i = i + 1) begin : g_fa
assign s[i] = x[i] ^ yy[i] ^ c[i];
assign c[i+1] = (x[i] & yy[i]) | (c[i] & (x[i] ^ yy[i]));
end endgenerate
assign same = (golden == {c[4], s});
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (DOC == 0) begin : g_eq
always @(*) if (!init) a_equiv: assert (same == 1'b1);
end else begin : g_doc
always @(*) if (!init) a_doc: assert (same == !y[3]);
end endgenerate
`endif
endmodule// formal: bmc 2 expect fail slang top adder_miter define BUG=1
`define FORMAL
// Lesson-local demo: behavioural adder against its ripple-carry twin; BUG=1 drops y[3] from the twin.
module adder_miter #(parameter BUG = 0, parameter DOC = 0) (
input wire clk, input wire rst, input wire [3:0] x, input wire [3:0] y, output wire same
);
wire [4:0] golden = x + y;
wire [3:0] yy = (BUG == 1) ? {1'b0, y[2:0]} : y;
wire [4:0] c; wire [3:0] s;
assign c[0] = 1'b0;
genvar i;
generate for (i = 0; i < 4; i = i + 1) begin : g_fa
assign s[i] = x[i] ^ yy[i] ^ c[i];
assign c[i+1] = (x[i] & yy[i]) | (c[i] & (x[i] ^ yy[i]));
end endgenerate
assign same = (golden == {c[4], s});
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (DOC == 0) begin : g_eq
always @(*) if (!init) a_equiv: assert (same == 1'b1);
end else begin : g_doc
always @(*) if (!init) a_doc: assert (same == !y[3]);
end endgenerate
`endif
endmoduleRun C writes the designer's story as a property: the twins agree exactly when bit 3 is clear. It passes on the ECO twin, pinning the difference to its mode. Run D is its failing partner: the same property on the unmodified twin fails at depth 2, because there the twins agree when bit 3 is set, so the story property can itself be refuted.
// formal: bmc 4 expect pass slang top adder_miter define BUG=1 define DOC=1
`define FORMAL
// Lesson-local demo: behavioural adder against its ripple-carry twin; BUG=1 drops y[3] from the twin.
module adder_miter #(parameter BUG = 0, parameter DOC = 0) (
input wire clk, input wire rst, input wire [3:0] x, input wire [3:0] y, output wire same
);
wire [4:0] golden = x + y;
wire [3:0] yy = (BUG == 1) ? {1'b0, y[2:0]} : y;
wire [4:0] c; wire [3:0] s;
assign c[0] = 1'b0;
genvar i;
generate for (i = 0; i < 4; i = i + 1) begin : g_fa
assign s[i] = x[i] ^ yy[i] ^ c[i];
assign c[i+1] = (x[i] & yy[i]) | (c[i] & (x[i] ^ yy[i]));
end endgenerate
assign same = (golden == {c[4], s});
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (DOC == 0) begin : g_eq
always @(*) if (!init) a_equiv: assert (same == 1'b1);
end else begin : g_doc
always @(*) if (!init) a_doc: assert (same == !y[3]);
end endgenerate
`endif
endmodule// formal: bmc 2 expect fail slang top adder_miter define DOC=1
`define FORMAL
// Lesson-local demo: behavioural adder against its ripple-carry twin; BUG=1 drops y[3] from the twin.
module adder_miter #(parameter BUG = 0, parameter DOC = 0) (
input wire clk, input wire rst, input wire [3:0] x, input wire [3:0] y, output wire same
);
wire [4:0] golden = x + y;
wire [3:0] yy = (BUG == 1) ? {1'b0, y[2:0]} : y;
wire [4:0] c; wire [3:0] s;
assign c[0] = 1'b0;
genvar i;
generate for (i = 0; i < 4; i = i + 1) begin : g_fa
assign s[i] = x[i] ^ yy[i] ^ c[i];
assign c[i+1] = (x[i] & yy[i]) | (c[i] & (x[i] ^ yy[i]));
end endgenerate
assign same = (golden == {c[4], s});
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (DOC == 0) begin : g_eq
always @(*) if (!init) a_equiv: assert (same == 1'b1);
end else begin : g_doc
always @(*) if (!init) a_doc: assert (same == !y[3]);
end endgenerate
`endif
endmoduleRead the runs together: A shows the flow proves equality across two structures, B gives the witness, C proves the story exhaustively, D shows the story is falsifiable. Root cause: the ECO drops a bit outside its intended mode. If the mode allows it, C plus per-mode equality elsewhere closes signoff; if not, B is the bug report. Either way equivalence never says the adder is correct.
The same flow runs on the four-requester arbiter: the golden holds its pointer when requester 0 wins, the revised fix updates it on every grant. The proof is agree-outside, with the pointer correspondence as its helper; a revised design with an extra change fails it. The full lesson is ECO equivalence flow.
// formal: prove 5 expect pass slang top eco_miter
`define FORMAL
module rr_core #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output reg [1:0] last
);
wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
(last == 2'd1) ? 4'b1100 :
(last == 2'd2) ? 4'b1000 : 4'b0000;
wire [3:0] hi_req = req & hi_mask;
wire [3:0] lo_req = (BUG == 3) ? (req | (4'b0001 << last)) : req;
function [3:0] lowest;
input [3:0] v;
lowest = v & (~v + 4'd1);
endfunction
wire [3:0] g_hi = lowest(hi_req);
wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0)}};
assign grant = g_hi | g_lo;
wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
always @(posedge clk) begin
if (rst) last <= 2'd3;
else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
end
endmodule
module eco_miter #(parameter REV = 0, parameter CONSTRAIN = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g_old, g_new;
wire [1:0] l_old, l_new;
// golden: the arbiter before the fix (pointer held when requester 0 wins)
rr_core #(.BUG(1)) u_old (.clk(clk), .rst(rst), .req(req), .grant(g_old), .last(l_old));
// revised: the fix (REV = 0), or the fix plus an unintended extra change (REV = 3)
rr_core #(.BUG(REV)) u_new (.clk(clk), .rst(rst), .req(req), .grant(g_new), .last(l_new));
assign same = (g_old == g_new);
// touched: the golden has granted requester 0 at least once, the condition the fix acts on
reg touched;
always @(posedge clk) if (rst) touched <= 1'b0; else if (g_old[0]) touched <= 1'b1;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (CONSTRAIN == 1) assume (req != 4'b0000);
always @(*) if (!init) a_agree_outside: assert (touched || same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same_ptr: assert (touched || (l_old == l_new));
end endgenerate
always @(*) if (!init) c_intended: cover (touched && !same);
`endif
endmodule// formal: bmc 2 expect fail slang top eco_miter define REV=3
`define FORMAL
module rr_core #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output reg [1:0] last
);
wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
(last == 2'd1) ? 4'b1100 :
(last == 2'd2) ? 4'b1000 : 4'b0000;
wire [3:0] hi_req = req & hi_mask;
wire [3:0] lo_req = (BUG == 3) ? (req | (4'b0001 << last)) : req;
function [3:0] lowest;
input [3:0] v;
lowest = v & (~v + 4'd1);
endfunction
wire [3:0] g_hi = lowest(hi_req);
wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0)}};
assign grant = g_hi | g_lo;
wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
always @(posedge clk) begin
if (rst) last <= 2'd3;
else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
end
endmodule
module eco_miter #(parameter REV = 0, parameter CONSTRAIN = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g_old, g_new;
wire [1:0] l_old, l_new;
// golden: the arbiter before the fix (pointer held when requester 0 wins)
rr_core #(.BUG(1)) u_old (.clk(clk), .rst(rst), .req(req), .grant(g_old), .last(l_old));
// revised: the fix (REV = 0), or the fix plus an unintended extra change (REV = 3)
rr_core #(.BUG(REV)) u_new (.clk(clk), .rst(rst), .req(req), .grant(g_new), .last(l_new));
assign same = (g_old == g_new);
// touched: the golden has granted requester 0 at least once, the condition the fix acts on
reg touched;
always @(posedge clk) if (rst) touched <= 1'b0; else if (g_old[0]) touched <= 1'b1;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (CONSTRAIN == 1) assume (req != 4'b0000);
always @(*) if (!init) a_agree_outside: assert (touched || same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same_ptr: assert (touched || (l_old == l_new));
end endgenerate
always @(*) if (!init) c_intended: cover (touched && !same);
`endif
endmoduleThe calculator counts how much of the input space the ECO touches: dropping operand bit 3 changes 128 of 256 vectors, always by exactly 8. A wrong mask is caught by the same call.
def census(mask):
touched, total, diffs = 0, 0, set()
for x in range(16):
for y in range(16):
total += 1
golden = (x + y) & 0x1F
twin = (x + (y & mask)) & 0x1F
if golden != twin:
touched += 1
diffs.add((golden - twin) & 0x1F)
return touched, total, diffs
touched, total, diffs = census(0x7)
assert total == 256, total
assert touched == 128, touched
assert diffs == {8}, diffs
# The failing variant: the same call with a mask that drops nothing touches no vector.
try:
assert census(0xF)[0] == 128
raise SystemExit("accepted an ECO that changes nothing")
except AssertionError:
pass
print("PASS: 128 of 256 vectors differ, always by exactly 8")A strong answer states the equivalence contract first (same encoding, scan off, consistent constants and black boxes, comparison after the defined point, latency asserted separately if timing differs), then reads the mismatch for shape: a constant offset is a dropped bit, a first-cycles mismatch is reset, failure everywhere is alignment. It closes by saying what the miter does not prove.
Dimension | Strong (3 to 4) | Weak (0 to 2) |
|---|---|---|
Assumption | Reset, constants, modes, alignment stated before reading the failure. | Assumes the setup is fine. |
Mechanism | Miter read at cycle level; mismatch shape classified. | Failure means the logic is wrong. |
Trade-off | Per-mode runs costed against one constrained run. | One run with the difference waived. |
Evidence | Minimal witness plus the intended-difference property, shown falsifiable. | The passing re-run alone. |
Alignment and reset, not logic: a constant time shift or a mismatched reset fails everywhere, while a logic bug fails on specific vectors. Prove the latency separately, align, then rerun.