A team boxed the multiplier stage, assumed that it returns the product, and reported the pipeline proved. The real stage had a fault. Job of this lesson: say what a black box keeps and adds, show the failure and the pass it can produce, and show why the assumption on its output is sound only when proved on the real block.
Boxing a block makes its outputs free inputs. That adds behaviours, so a proof that passes with the box stays valid for the real design. A failure may use a value the real block cannot produce. A contract on the box's outputs removes the false failure, but an assumption is a promise: it is sound only if the same statement is proved on the real block.
Run | Stage 2 | Contract | Result |
|---|---|---|---|
Local stage-3 relation | Boxed | None | Proven: a pass with the box is valid |
End to end | Boxed | None | Fails at step 4: a false failure |
End to end | Boxed | Assumed | Proven |
End to end, real stage has a fault | Boxed | Assumed only | Proven: a false pass |
Contract on the real stage | Real, with the fault | Asserted | Fails at step 3: the discharge |
// formal: prove 5 expect pass slang top pipe3c define CUT=1 define CONTRACT=0 define E2E=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
endmodule// 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
endmodule// 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
endmoduleThe first run proves a relation of stage 3 that does not look at the boxed value, so it stays true of the real design. The second is the false failure (depth 4 passes). The third assumes the contract. Now the real stage gets a fault: its product is one too high.
// formal: prove 5 expect pass slang top pipe3c define CUT=1 define CONTRACT=1 define BUG=1
`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
endmodule// formal: bmc 4 expect fail slang top pipe3c define CUT=0 define CONTRACT=0 define BUG=1
`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 fourth run passes: the box hides the fault, and the contract that should have caught it is only assumed. The fifth removes the box and proves the same contract on the faulty real stage: it fails at step 3 (depth 3 passes), before the end-to-end property would at step 4. That run is the discharge, and the table of contracts needs it for every box.
Each boxed block has a contract, the proof of that contract on the real block, and a planted fault that fails the proof.
A pass obtained with a box is accepted as valid for the real design; a failure is replayed on the real block before anyone tightens an assumption.
No assumption on a box's output is written to make a proof go through: it states a property of the real block that has its own proof.
Plant a fault in the real block and rerun the box proof: it must still pass (the box hides it) and the contract proof on the real block must fail. If the contract proof also passes, the contract is too weak to matter.
The box is sound; the contract is not. A pass with free outputs is valid for the real design. The false pass came from assuming the contract without proving it.