A team cut the multiplier stage out of the pipeline to speed up a proof and got a counterexample at step 4 that the real stage can never produce. Job of this lesson: cut a stage free, tell a false counterexample from a real one by replaying it on the real stage, and write the smallest contract that removes it.
Three mechanisms shrink a proof, and only one is exact. Cone-of-influence reduction removes logic that cannot affect any property or assumption: never changes a verdict. An assumption removes behaviours: it can hide a fault. A cut point adds behaviours: the stage's output becomes a free input, so passing proofs stay valid and failures may be spurious. A cut failure is not an induction failure. A counterexample to the induction step starts from an unreachable state: the bounded check passes and only the step fails. A cut counterexample fails the bounded check, using a free value the real stage could not produce.
Mechanism | Effect on behaviours | Exact? | How it goes wrong |
|---|---|---|---|
Cone reduction | Removes logic outside every cone | Yes | Never |
Assumption | Removes behaviours | No | Hides a fault: a false pass |
Cut point | Adds behaviours (free output) | Passes stay valid | False counterexample, or a false pass if the contract is only assumed |
The pipeline with stage 2 cut (CUT=1) loads a free value pf into the stage-2 register instead of the product. With no contract, the end-to-end property fails at step 4 (depth 4 passes). Replayed on the real stage (CUT=0) the same property proves, and so does the contract itself: the product register equals the product of the stage-1 registers one cycle earlier.
// formal: bmc 5 expect fail slang top pipe3c define CUT=1 define CONTRACT=0 define BUG=0
`define FORMAL
// pipe3c: pipe3 with stage 2 optionally cut free. CUT=1: the stage-2 register loads the free input pf instead of the
// product. CONTRACT=1 assumes pf equals the product of the stage-1 registers. BUG=1 plants a fault in the real stage 2
// (the product plus one). E2E=0 switches the end-to-end property off.
module pipe3c #(parameter CUT = 0, parameter CONTRACT = 0, parameter BUG = 0, parameter E2E = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] pf,
output reg [7:0] y
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
wire [7:0] real_p = s[3:0] * c1 + ((BUG == 1) ? 8'd1 : 8'd0);
always @(posedge clk) begin
if (rst) begin s <= 0; c1 <= 0; p <= 0; y <= 0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= (CUT == 1) ? pf : real_p;
y <= p + 8'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// clean cycles since reset, and the inputs three cycles ago
reg [1:0] hist;
always @(posedge clk) if (rst) hist <= 0; else if (hist != 3) hist <= hist + 1;
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;
generate if (E2E) begin : g_e2e
always @(*) if (!init && hist == 3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
end endgenerate
// a local relation of stage 3, true with the stage cut or not
always @(posedge clk) if (!init && !$past(rst)) a_stage3: assert (y == $past(p) + 8'd1);
// the contract on the stage-2 value: assumed on the free input when the stage is cut ...
generate if (CUT == 1 && CONTRACT == 1) begin : g_c
always @(*) if (!init) assume (pf == s[3:0] * c1);
end endgenerate
// ... and asserted on the real stage otherwise (each operand's past first, then the product, in eight bits)
generate if (CUT == 0) begin : g_p
always @(posedge clk) if (!init && !$past(rst)) a_contract: assert (p == $past(s[3:0]) * $past(c1));
end endgenerate
`endif
endmoduleStep | Inputs and the free value | What happens |
|---|---|---|
1 | a 0, b 1, c 0 (for example) | Stage 1 holds sum 1 and operand 0 |
2 | pf = 255 | The real stage would load 1 x 0 = 0; the cut stage loads 255 |
4 | - | y is 0 (255 + 1 wraps), the specification says 1: |
// formal: prove 5 expect pass slang top pipe3c define CUT=0 define CONTRACT=0 define BUG=0
`define FORMAL
// pipe3c: pipe3 with stage 2 optionally cut free. CUT=1: the stage-2 register loads the free input pf instead of the
// product. CONTRACT=1 assumes pf equals the product of the stage-1 registers. BUG=1 plants a fault in the real stage 2
// (the product plus one). E2E=0 switches the end-to-end property off.
module pipe3c #(parameter CUT = 0, parameter CONTRACT = 0, parameter BUG = 0, parameter E2E = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] pf,
output reg [7:0] y
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
wire [7:0] real_p = s[3:0] * c1 + ((BUG == 1) ? 8'd1 : 8'd0);
always @(posedge clk) begin
if (rst) begin s <= 0; c1 <= 0; p <= 0; y <= 0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= (CUT == 1) ? pf : real_p;
y <= p + 8'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// clean cycles since reset, and the inputs three cycles ago
reg [1:0] hist;
always @(posedge clk) if (rst) hist <= 0; else if (hist != 3) hist <= hist + 1;
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;
generate if (E2E) begin : g_e2e
always @(*) if (!init && hist == 3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
end endgenerate
// a local relation of stage 3, true with the stage cut or not
always @(posedge clk) if (!init && !$past(rst)) a_stage3: assert (y == $past(p) + 8'd1);
// the contract on the stage-2 value: assumed on the free input when the stage is cut ...
generate if (CUT == 1 && CONTRACT == 1) begin : g_c
always @(*) if (!init) assume (pf == s[3:0] * c1);
end endgenerate
// ... and asserted on the real stage otherwise (each operand's past first, then the product, in eight bits)
generate if (CUT == 0) begin : g_p
always @(posedge clk) if (!init && !$past(rst)) a_contract: assert (p == $past(s[3:0]) * $past(c1));
end endgenerate
`endif
endmoduleThe minimal contract is that stage 2 output equals the stage-1 product one cycle later. Assumed on the free value, it removes the false counterexample and the proof passes; the real stage proved it in the run above, so the cut result is valid.
// formal: prove 5 expect pass slang top pipe3c define CUT=1 define CONTRACT=1 define BUG=0
`define FORMAL
// pipe3c: pipe3 with stage 2 optionally cut free. CUT=1: the stage-2 register loads the free input pf instead of the
// product. CONTRACT=1 assumes pf equals the product of the stage-1 registers. BUG=1 plants a fault in the real stage 2
// (the product plus one). E2E=0 switches the end-to-end property off.
module pipe3c #(parameter CUT = 0, parameter CONTRACT = 0, parameter BUG = 0, parameter E2E = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] pf,
output reg [7:0] y
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
wire [7:0] real_p = s[3:0] * c1 + ((BUG == 1) ? 8'd1 : 8'd0);
always @(posedge clk) begin
if (rst) begin s <= 0; c1 <= 0; p <= 0; y <= 0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= (CUT == 1) ? pf : real_p;
y <= p + 8'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// clean cycles since reset, and the inputs three cycles ago
reg [1:0] hist;
always @(posedge clk) if (rst) hist <= 0; else if (hist != 3) hist <= hist + 1;
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;
generate if (E2E) begin : g_e2e
always @(*) if (!init && hist == 3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
end endgenerate
// a local relation of stage 3, true with the stage cut or not
always @(posedge clk) if (!init && !$past(rst)) a_stage3: assert (y == $past(p) + 8'd1);
// the contract on the stage-2 value: assumed on the free input when the stage is cut ...
generate if (CUT == 1 && CONTRACT == 1) begin : g_c
always @(*) if (!init) assume (pf == s[3:0] * c1);
end endgenerate
// ... and asserted on the real stage otherwise (each operand's past first, then the product, in eight bits)
generate if (CUT == 0) begin : g_p
always @(posedge clk) if (!init && !$past(rst)) a_contract: assert (p == $past(s[3:0]) * $past(c1));
end endgenerate
`endif
endmoduleOne trap hides in the contract itself. Written as $past(s[3:0] * c1) the product is evaluated in four bits (the operands' width), so it wraps and the contract fails on the good real stage at step 4 (depth 4 passes). The form that works takes the past of each operand and multiplies after, in eight bits:
// formal: bmc 5 expect fail slang top pipe3c define CUT=0 define CONTRACT=0 define BUG=0
`define FORMAL
// pipe3c: pipe3 with stage 2 optionally cut free. CUT=1: the stage-2 register loads the free input pf instead of the
// product. CONTRACT=1 assumes pf equals the product of the stage-1 registers. BUG=1 plants a fault in the real stage 2
// (the product plus one). E2E=0 switches the end-to-end property off.
module pipe3c #(parameter CUT = 0, parameter CONTRACT = 0, parameter BUG = 0, parameter E2E = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] pf,
output reg [7:0] y
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
wire [7:0] real_p = s[3:0] * c1 + ((BUG == 1) ? 8'd1 : 8'd0);
always @(posedge clk) begin
if (rst) begin s <= 0; c1 <= 0; p <= 0; y <= 0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= (CUT == 1) ? pf : real_p;
y <= p + 8'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// clean cycles since reset, and the inputs three cycles ago
reg [1:0] hist;
always @(posedge clk) if (rst) hist <= 0; else if (hist != 3) hist <= hist + 1;
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;
generate if (E2E) begin : g_e2e
always @(*) if (!init && hist == 3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
end endgenerate
// a local relation of stage 3, true with the stage cut or not
always @(posedge clk) if (!init && !$past(rst)) a_stage3: assert (y == $past(p) + 8'd1);
// the contract on the stage-2 value: assumed on the free input when the stage is cut ...
generate if (CUT == 1 && CONTRACT == 1) begin : g_c
always @(*) if (!init) assume (pf == s[3:0] * c1);
end endgenerate
// ... and asserted on the real stage otherwise (narrow form: the product inside $past, evaluated in four bits)
generate if (CUT == 0) begin : g_p
always @(posedge clk) if (!init && !$past(rst)) a_contract: assert (p == $past(s[3:0] * c1));
end endgenerate
`endif
endmoduleThe assumed contract is sound only when something proves it on the real stage. Assume-Guarantee Contracts and Black Boxes show the proof and the false pass that follows when it is skipped.
The contract is minimal: it states only what the downstream property needs, in one line.
Every false counterexample was replayed on the real stage before the contract was written.
Each cut has a written contract and the proof of that contract on the real block, or the cut is not signed off.
After every failure on a cut model, replay the same property on the real stage before reading further: here the real stage proves to depth 5, so the trace used the free value. Only then write the contract, and rerun with it assumed. If the contract itself fails on the real stage, the contract is wrong, as the four-bit product trap shows at step 4. Never tighten an unrelated assumption to make a cut counterexample disappear.
No. A cut adds behaviours, so a pass stays valid for the real design. The failure is spurious: the real stage passes the same property.