Latency, equivalence and a scoped change are three claims about the same few registers, and each has a window below which the proof is inconclusive and above which it closes. This lesson measures the windows, reads the twin fault in numbers, gives the two pipeline mutants, and shows why the scoped ECO claim is true by construction and so needs a partner that makes it fail.
The latency property reads inputs three cycles back, so a window of two is inconclusive and three proves. pipe3 has no valid signal, so a valid-propagation property is not available for it; the latency and reset properties are the whole set.
// formal: prove 2 expect unproven slang top pipe3
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmodule// formal: prove 3 expect pass slang top pipe3
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmoduleMutant | Change | Killer | Smallest depth |
|---|---|---|---|
| the output stage drops the plus-one |
| 5 |
| the output register resets to 1 |
| 3 |
// formal: bmc 5 expect fail slang top pipe3
`define FORMAL
// mutant pipe-m-plus-one: the output stage drops the plus-one
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmodule// formal: bmc 3 expect fail slang top pipe3
`define FORMAL
// mutant pipe-m-reset-zero: the output register resets to 1
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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'd1; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmoduleVariant | Cause in the listing | Fix | Fails (step), smallest depth |
|---|---|---|---|
W1 | The twin's multiplier uses | Use all of |
|
One input vector at step 1, with bit 3 of c set and a non-zero sum, reaches the outputs at step 4. In the simulation example of the running designs (inputs at cycles 1 and 2, results at cycles 4 and 5) the reference gives 136 and the faulty twin 16 for the second vector; the solver finds its own vector, at step 1, which reaches the output at step 4.
def pipe(inputs, twin=False, bug=False):
s = c1 = p = y = 0
s2 = c2 = 0
out = []
for a, b, c in inputs:
out.append(y)
if not twin:
y, p, s, c1 = p + 1, (s & 15) * c1, (a + b) & 255, c & 15
else:
y = s2 * ((c2 & 7) if bug else c2) + 1
s2, c2, s, c1 = s & 15, c1, (a + b) & 255, c & 15
return out
INPUTS = [(3, 4, 5), (10, 5, 9)] + [(0, 0, 0)] * 6
ref, good, bad = pipe(INPUTS), pipe(INPUTS, twin=True), pipe(INPUTS, twin=True, bug=True)
assert ref[:5] == good[:5] == [0, 1, 1, 36, 136], "reference and correct twin agree at every cycle"
assert bad[3] == 36 and bad[4] == 16, "the faulty twin gives 16 where the reference gives 136"
assert ref[3] == bad[3], "the first vector has bit 3 of c clear, so it still agrees"
first = next(i + 1 for i in range(len(ref)) if ref[i] != bad[i])
assert first == 5, "the first disagreement is the second vector, at cycle 5"
print("PASS: the faulty twin agrees on 5 and disagrees on 9: 16 against 136")The reference and the faulty twin agree on the first vector (c = 5, bit 3 clear) and disagree on the second (c = 9, bit 3 set). The model mirrors the listing and reproduces both numbers.
Without the helper a window of two is inconclusive and three proves; with the helper a window of one fails on the helper itself and two proves. The faulty twin passes at depth 4, because the bound ends where the evidence begins, and fails at depth 5.
// formal: prove 1 expect unproven slang top pipe3_eq
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmodule// formal: prove 2 expect pass slang top pipe3_eq
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmodule// formal: prove 2 expect unproven slang top pipe3_eq define HELPER=0
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmodule// formal: prove 3 expect pass slang top pipe3_eq define HELPER=0
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmodule// formal: bmc 4 expect pass slang top pipe3_eq define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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
endmodule// formal: bmc 5 expect fail slang top pipe3_eq define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
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 // stage-2 register, exposed for the miter's helper assertion
);
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
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
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, // stage-2 registers, exposed for the miter's helper assertion
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);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
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 two revisions differ in the reset value of the pointer. The miter fails in the first cycle, which is the change doing what the note says. The scoped claim has three parts: when the pointers agree the grants agree, once the pointers agree they stay equal, and each revision still grants whenever a request is present and grants one at a time. The first part holds by construction, because the grant is the same function of the request and the pointer in both revisions; the claim therefore needs a partner that can make it fail. The partner changes the second revision more than the note allows, so that it never uses its low-priority search; with the work properties dropped, the scoped claim itself fails at depth 3.
// formal: prove 2 expect pass slang top arb_eco_scope
`define FORMAL
// lesson-local revision before the change: the pointer resets to 3, so requester 0 is served first
module rr_arbiter_gold (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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(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) last <= gidx;
end
endmodule
// lesson-local revision after the change: the pointer resets to 0, so requester 1 is served first
module rr_arbiter_eco (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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(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'd0;
else if (|grant) last <= gidx;
end
endmodule
module arb_eco_scope (
input wire clk,
input wire rst,
input wire [3:0] req
);
wire [3:0] g1, g2;
wire [1:0] l1, l2;
rr_arbiter_gold u1 (.clk(clk), .rst(rst), .req(req), .grant(g1), .dbg_last(l1));
rr_arbiter_eco u2 (.clk(clk), .rst(rst), .req(req), .grant(g2), .dbg_last(l2));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_cond: assert (l1 != l2 || g1 == g2);
a_onehot_gold: assert ((g1 & (g1 - 4'd1)) == 4'd0);
a_onehot_eco: assert ((g2 & (g2 - 4'd1)) == 4'd0);
a_work_gold: assert (!(|req) || (|g1));
a_work_eco: assert (!(|req) || (|g2));
end
// once the pointers agree, they stay equal
always @(posedge clk) if (!init && !$past(rst) && $past(l1 == l2)) a_stay: assert (l1 == l2);
// the pointers can agree while a request is present
always @(*) if (!init) c_agree: cover (l1 == l2 && |req);
`endif
endmodule// formal: bmc 3 expect fail slang top arb_eco_scope
`define FORMAL
// the revision after the change also loses its low-priority search; the work-conservation assertions are dropped so the scope claim alone must notice
// lesson-local revision before the change: the pointer resets to 3, so requester 0 is served first
module rr_arbiter_gold (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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(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) last <= gidx;
end
endmodule
// lesson-local revision after the change: the pointer resets to 0, so requester 1 is served first
module rr_arbiter_eco (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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 = 4'b0000 & lowest(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'd0;
else if (|grant) last <= gidx;
end
endmodule
module arb_eco_scope (
input wire clk,
input wire rst,
input wire [3:0] req
);
wire [3:0] g1, g2;
wire [1:0] l1, l2;
rr_arbiter_gold u1 (.clk(clk), .rst(rst), .req(req), .grant(g1), .dbg_last(l1));
rr_arbiter_eco u2 (.clk(clk), .rst(rst), .req(req), .grant(g2), .dbg_last(l2));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_cond: assert (l1 != l2 || g1 == g2);
a_onehot_gold: assert ((g1 & (g1 - 4'd1)) == 4'd0);
a_onehot_eco: assert ((g2 & (g2 - 4'd1)) == 4'd0);
x_a_work_gold: cover (!(|req) || (|g1));
x_a_work_eco: cover (!(|req) || (|g2));
end
// once the pointers agree, they stay equal
always @(posedge clk) if (!init && !$past(rst) && $past(l1 == l2)) a_stay: assert (l1 == l2);
// the pointers can agree while a request is present
always @(*) if (!init) c_agree: cover (l1 == l2 && |req);
`endif
endmoduleThe revisions do not agree for every stimulus. With all four requests held high the pointers differ in every cycle; with a single requester they meet after the first grant. A cover shows the second case is reachable.
// formal: cover 6 expect reached slang top arb_eco_scope
`define FORMAL
// lesson-local revision before the change: the pointer resets to 3, so requester 0 is served first
module rr_arbiter_gold (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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(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) last <= gidx;
end
endmodule
// lesson-local revision after the change: the pointer resets to 0, so requester 1 is served first
module rr_arbiter_eco (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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(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'd0;
else if (|grant) last <= gidx;
end
endmodule
module arb_eco_scope (
input wire clk,
input wire rst,
input wire [3:0] req
);
wire [3:0] g1, g2;
wire [1:0] l1, l2;
rr_arbiter_gold u1 (.clk(clk), .rst(rst), .req(req), .grant(g1), .dbg_last(l1));
rr_arbiter_eco u2 (.clk(clk), .rst(rst), .req(req), .grant(g2), .dbg_last(l2));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_cond: assert (l1 != l2 || g1 == g2);
a_onehot_gold: assert ((g1 & (g1 - 4'd1)) == 4'd0);
a_onehot_eco: assert ((g2 & (g2 - 4'd1)) == 4'd0);
a_work_gold: assert (!(|req) || (|g1));
a_work_eco: assert (!(|req) || (|g2));
end
// once the pointers agree, they stay equal
always @(posedge clk) if (!init && !$past(rst) && $past(l1 == l2)) a_stay: assert (l1 == l2);
// the pointers can agree while a request is present
always @(*) if (!init) c_agree: cover (l1 == l2 && |req);
`endif
endmoduledef run(reset, masks):
last, out = reset, []
for m in masks:
g = next((i for i in ((last + o) % 4 for o in range(1, 5)) if m >> i & 1), None)
out.append((last, g))
if g is not None:
last = g
return out
all_req = [15] * 8
gold, eco = run(3, all_req), run(0, all_req)
assert all(g[0] != e[0] for g, e in zip(gold, eco)), "with all requests held the pointers never meet"
assert all(g[1] != e[1] for g, e in zip(gold, eco))
single = [1] * 4
gold, eco = run(3, single), run(0, single)
assert gold[0][0] != eco[0][0] and gold[1:] == eco[1:], "with one requester the pointers meet after the first grant"
assert all(g[1] == e[1] for g, e in zip(gold[1:], eco[1:]))
print("PASS: all requests keep the revisions apart; a single requester brings them together after one grant")Every window is measured: with and without each helper, with the failing assertion named.
A bounded pass one depth short of a fault is filed beside the counterexample, never alone.
The scoped claim has a failing partner, because a claim that holds by construction proves nothing until it can fail.
Compare the revisions textually before the miter: one line differs. If the scope claim fails on the good revisions, the condition is too weak; if it never fails, the partner changed nothing the claim reads.
The first input vector enters at step 1 and its result is first visible at step 4; a run that ends at depth 4 checks steps 0 to 3, one before the evidence.
It shows the revisions agree where they should, not that either revision is correct; the work and one-hot properties on each revision supply the other half.