An engineer doubled the time limit on a stalled run and waited twice as long for the same inconclusive answer. The run did not need more time; it needed a different engine, a deeper bound, or a split property set. Depth, engine, time and splitting are four different controls, and turning the wrong one wastes the run. This lesson shows what each does on one design.
Job of this lesson: define task, engine, depth and time limit in any formal tool, and show what changing each one does.
Control | What it is | What changing it does |
|---|---|---|
Task | The question: prove unboundedly, check boundedly to N, or search for a witness | Changes what a result means: a bounded pass is not a proof. |
Engine | The method that answers it: unrolling for bounded checks, the induction step for proofs | A different engine answers a different question. |
Depth | How far the unrolling reaches | Looks further; costs clauses linearly. |
Time limit | How long the solver may work | Helps only a run that was making progress. |
Splitting | One property per run | Narrows each cone. |
The running design is a three-stage arithmetic pipeline beside its retimed twin, compared output by output in a miter (a circuit that feeds both the same inputs and raises a flag when the outputs differ) with 48 design state bits. The bug variant of the twin ignores bit 3 of one operand, and the outputs diverge at step 4, when the first input vector reaches the output. Depth 4 passes and depth 5 fails on the same design; the good twin proves.
// 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 (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed 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 invariant
);
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 (works in every front 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; // 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);
// after 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 invariant
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 invariant across the moved cut: the reference's stage-2 register p equals the
// twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
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 (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed 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 invariant
);
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 (works in every front 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; // 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);
// after 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 invariant
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 invariant across the moved cut: the reference's stage-2 register p equals the
// twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
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 5 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 (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed 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 invariant
);
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 (works in every front 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; // 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);
// after 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 invariant
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 invariant across the moved cut: the reference's stage-2 register p equals the
// twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
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
endmoduleDepth | Sees step 4? | Verdict on the bug variant | Reading |
|---|---|---|---|
4 | No | Pass | Bounded to 4: the divergent outputs are one step outside. |
5 | Yes | Counterexample at step 4 | The first input vector reaches the output. |
The script prices the two depths for illustrative sizes (2,000 gates and the miter's 48 flops, labelled illustrative): unrolled size is gates times three times depth plus one equality per flop per step. Depth 5 costs a quarter more than depth 4, and ten times the depth costs ten times the clauses. The check runs on the formula and on three mutants, all caught.
def unrolled(gates, flops, depth):
return gates * 3 * depth + flops * depth
def check(fn):
assert fn(2000, 48, 4) == 24000 + 192
assert fn(2000, 48, 5) == 30000 + 240
assert fn(2000, 48, 40) == 10 * fn(2000, 48, 4)
assert fn(2000, 0, 5) == 30000
assert fn(0, 48, 5) == 240
check(unrolled)
mutants = [
lambda g, f, d: g * 3 * d,
lambda g, f, d: g * d + f * d,
lambda g, f, d: g * 3 + f * d,
]
for mutant in mutants:
caught = False
try:
check(mutant)
except AssertionError:
caught = True
assert caught
print("PASS: depth 4 costs 24,192 clauses and depth 5 costs 30,240 in the illustrative miter; all three mutants are caught")Each run names its task, engine, depth and time limit beside the verdict; a bounded pass states its depth.
Depth changes are justified by trigger length plus latency, not by round numbers; slow runs are split by property before the time limit is raised.
Read the status table per property at two depths before touching any control: if the deeper bound flips the verdict, the question was depth, not effort. Raise the time limit only when the solver reports progress; otherwise reduce, split or strengthen. Never tighten assumptions to buy speed without a written justification.
Depth: the trigger needs step 4, so depth 4 cannot see it. Raising the time limit at depth 4 would change nothing.
When the solver reports steady progress and the cone and depth are already right: the run needs budget, not a new question.