Retiming moves the multiplier across the register cut: stage 2 held one 8-bit product, and now holds two 4-bit operands with the multiply pushed into stage 3. The outputs must agree every cycle from reset, while the middle registers agree nowhere. A register-by-register comparison fails everywhere on a correct design. This lesson proves the pair equivalent the honest way.
This lesson has one job: prove output equivalence across a moved register cut, and show the exact mismatch when an operand bit is dropped in the moved logic.
Both pipelines leave reset together, see identical inputs, and the miter asserts equal outputs every cycle. The induction step still needs help: from arbitrary states the reference product p and the twin operands s2, c2 are unrelated, so the step can start with p different from s2 * c2 and diverge at the output. The cut invariant asserts exactly that relation: the stage-2 register of the reference equals the twin pre-multiplier registers multiplied. With it the proof closes at k = 2; without it, a longer window of k = 3 forces the relation to hold anyway. Both are full proofs; the invariant is the cheaper one.
The numbers are measured: the pipeline latency is 3 cycles, the good miter proves at k = 2 with the helper and k = 3 without, and every run completes well under a second.
The reference computes y as ((a + b) low 4 bits times c low 4 bits) + 1 over three stages. The twin keeps stage 1, splits stage 2 into the two operands, and multiplies in stage 3. The miter below is the complete file:
// formal: prove 5 expect pass slang top pipe3_eq
`define FORMAL
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module pipe3_retimed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [3:0] dbg_s2,
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmoduleRemove the helper and the base case still passes while the step fails: the CTI starts with the product register disagreeing with the twin operands, a pair no shared stimulus produces. That is the measured expect unproven at k = 2:
// formal: prove 2 expect unproven slang top pipe3_eq define HELPER=0
`define FORMAL
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module pipe3_retimed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [3:0] dbg_s2,
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmoduleThe injected twin bug ignores bit 3 of the c operand in the moved multiplier: a dropped operand bit, not a lost stage, and nothing differs until a vector with that bit set reaches the output. Steps and cycles are numbered alike: the first input vector is cycle 1 and step 1. The shortest counterexample needs one input vector at step 1 with bit 3 of c set and a non-zero low nibble of a + b; it reaches the output at step 4, so depth 4 passes and depth 5 fails, which is the pipeline latency plus the trigger:
// formal: bmc 5 expect fail slang top pipe3_eq define BUG=1
`define FORMAL
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module pipe3_retimed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [3:0] dbg_s2,
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmoduleHow to read it: values are in hexadecimal, so 24 is 36, 88 is 136 and 10 is 16. Step 0 is the reset step; the outputs are unknown until the reset edge has acted. The first input vector, a 3, b 4, c 5, is applied at step 1, and the second, a 10, b 5, c 9, at step 2; a, b and c are zero afterwards. Both outputs read 0 at step 1 and 1 at steps 2 and 3. At step 4 both read 36, from the first vector, and same is high. At step 5 y_ref reads 136 and y_twin reads 16, from the second vector whose c has bit 3 set, and same falls. The two outputs agree at every step up to step 4 and differ at step 5, the first output that depends on the second vector.
The replay used for reading the trace applies inputs of 3, 4, 5 at cycle 1 and 10, 5, 9 at cycle 2. The first vector has bit 3 of c clear, so both pipelines give 36 at cycle 4; the second has it set, so the split appears one cycle after the shortest counterexample, at cycle 5. The Python model below reproduces that trace, the cut invariant on every reachable cycle, and the split of the buggy twin:
def run(stim, bug):
ref = dict(s=0, c1=0, p=0, y=0)
tw = dict(s=0, c1=0, s2=0, c2=0, y=0)
rows = []
for a, b, c in stim:
rows.append((ref["y"], tw["y"], ref["p"], tw["s2"] * tw["c2"]))
c2 = (tw["c2"] & 7) if bug else tw["c2"]
ref = dict(s=(a + b) & 255, c1=c & 15, p=(ref["s"] & 15) * ref["c1"], y=(ref["p"] + 1) & 255)
tw = dict(s=(a + b) & 255, c1=c & 15, s2=tw["s"] & 15, c2=tw["c1"], y=(tw["s2"] * c2 + 1) & 255)
return rows
stim = [(3, 4, 5), (10, 5, 9), (0, 0, 0), (0, 0, 0), (0, 0, 0)]
good = run(stim, False)
assert [r[0] for r in good] == [0, 1, 1, 36, 136]
assert [r[1] for r in good] == [0, 1, 1, 36, 136]
assert all(r[2] == r[3] for r in good)
assert (3 + 4) * 5 + 1 == 36 and (10 + 5) * 9 + 1 == 136
bad = run(stim, True)
assert [r[1] for r in bad] == [0, 1, 1, 36, 16]
assert (10 + 5) * (9 & 7) + 1 == 16
first = [i + 1 for i, r in enumerate(bad) if r[0] != r[1]][0]
assert first == 5
print("PASS: both pipelines give 36 then 136; the bit-3 twin gives 16 at cycle 5")# not-run: illustrative trace, not executable here
inputs at cycle 1: a=3 b=4 c=5 | at cycle 2: a=10 b=5 c=9
cycle 4: y = (3+4) x 5 + 1 = 36 on both | cycle 5: reference (10+5) x 9 + 1 = 136
bug twin at cycle 5: 15 x (9 AND 7) + 1 = 16 (bit 3 of c ignored)
shortest counterexample: one vector at step 1 with c[3] = 1 -> split at step 4
bmc 4 passes (bug still in flight) | bmc 5 fails at step 4The cut invariant is stated in the proof, proved alongside the outputs, and tied to the moved logic by name.
The depth discussion names the latency: a bound shorter than reset plus trigger plus latency cannot see the bug.
The twin debug ports exist precisely so the miter needs no hierarchical references.
Replay the failing inputs in simulation on both pipelines and confirm the 136-versus-16 split. Then check the alignment: both outputs must be compared at the same cycle counted from the same reset. A mismatch in the first three cycles is an alignment or reset artefact until proven otherwise; the bug shows once its input has crossed the full latency.
Setup until proven otherwise: the first cycles after reset are the alignment and reset-value region. Confirm both pipelines leave the same reset values, align the comparison after the defined point, and rerun.