A timeout counter counts to 1,000,000. A bounded run needs a million cycles to see done, so it never looks. The team shrinks the limit to 5, the proof passes, and a fault in the compare logic ships because it only appears for larger limits. Job of this lesson: shrink a counter, say what the small size can hide, and prove the real size by induction.
Shrinking a threshold is sound only if the logic is the same for every threshold. It is not enough that it passes at one size. Two checks make it sound: run at two or three small sizes that differ in the way the fault could (here, 5 against 12), and close the real value with an inductive proof, not with a deeper bounded run. The proof needs a helper that ties the counter to a reference count; without it the induction step starts from a state where the two disagree.
Fact | Value | Source |
|---|---|---|
Depth at which | LIMIT + 2 (reset step, then LIMIT start cycles) | Runs below: limit 5 at depth 7, limit 12 at depth 14 |
Depth a bounded run needs for 1,000,000 | 1,000,002 | The formula |
State bits, counter and reference | 2 x W | W = 4: 8 bits; W = 20: 40 bits |
Two cover runs check the first row: done is reached at depth 7 for limit 5 and at depth 14 for limit 12, and is not reached one step sooner.
// formal: cover 7 expect reached slang top tmo define W=3 define LIMIT=5
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmodule// formal: cover 14 expect reached slang top tmo define W=4 define LIMIT=12
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmoduleThe counter counts consecutive start cycles up to LIMIT, and done is high at LIMIT. A reference counter in the harness holds the specification, and a_not_early says done implies the reference has reached LIMIT. The fault compares only the low three bits of the count with the low three bits of LIMIT. At limit 5 the counter never exceeds 5, so the fault is invisible; at limit 12 the low three bits equal 4 at count 4 and done rises eight counts early.
// formal: prove 6 expect pass slang top tmo define W=3 define LIMIT=5
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmodule// formal: prove 6 expect pass slang top tmo define W=3 define LIMIT=5 define BUG=1
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmodule// formal: bmc 6 expect fail slang top tmo define W=4 define LIMIT=12 define BUG=1
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmoduleThe second run is the lesson: the faulty design proves at limit 5 because, at that size, it is the same circuit. The third run, at limit 12, fails at step 5 (depth 5 passes). Now the real size. With the helper h_same (counter equals reference) the proof is complete in a few steps, whatever the limit; without it the induction step fails:
// formal: prove 4 expect pass slang top tmo define W=20 define LIMIT=1000000
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmodule// formal: prove 8 expect unproven slang top tmo define W=20 define LIMIT=1000000 define HELPER=0
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmoduleAt the real size the same fault fails at step 1, because 1,000,000 has zero low bits and done rises at count 0. The abstraction question is therefore about which sizes show a fault, not about how large the size is. Finally the bound that proves nothing: asserting cnt <= 4'b1111 on a four-bit counter is true for every value, so the faulty design passes to depth 12 and the property is useless:
// formal: bmc 12 expect pass slang top tmo define W=4 define LIMIT=12 define BUG=1 define PROP=2
`define FORMAL
// tmo: timeout counter. cnt counts consecutive start cycles and stops at LIMIT; done is high while cnt == LIMIT.
// W is the counter width. BUG=1 compares only the low three bits of cnt with the low three bits of LIMIT.
// PROP=2 swaps the reference check for a bound that every W-bit value satisfies.
module tmo #(parameter W = 4, parameter LIMIT = 5, parameter BUG = 0, parameter PROP = 1, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire start,
output wire done
);
reg [W-1:0] cnt;
assign done = (BUG == 1) ? (cnt[2:0] == LIMIT[2:0]) : (cnt == LIMIT);
always @(posedge clk) begin
if (rst || !start) cnt <= {W{1'b0}};
else if (cnt != LIMIT) cnt <= cnt + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// reference: consecutive start cycles seen, held at LIMIT (the specification of "LIMIT cycles")
reg [W-1:0] run;
always @(posedge clk) begin
if (rst || !start) run <= {W{1'b0}};
else if (run != LIMIT) run <= run + 1'b1;
end
generate if (PROP == 1) begin : g_early
always @(*) if (!init) a_not_early: assert (!done || run == LIMIT);
end else begin : g_taut
always @(*) if (!init) a_bound: assert (cnt <= {W{1'b1}});
end endgenerate
always @(*) if (!init) c_done: cover (done);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same: assert (cnt == run);
end endgenerate
`endif
endmodule# Depth at which done first fires, from the measured covers: limit 5 -> depth 7, limit 12 -> depth 14
measured = {5: 7, 12: 14}
def depth_to_done(limit):
return limit + 2 # one reset step, then LIMIT start cycles, one step to see done
assert all(depth_to_done(l) == d for l, d in measured.items())
real = 1_000_000
assert depth_to_done(real) == 1_000_002
width = real.bit_length()
assert width == 20 and 2 ** width > real # 20 bits are needed; the counter and its reference are 40 flip-flops
bits = 2 * width
assert bits == 40
wrong = lambda l: l + 1 # a formula that forgets the reset step
assert any(wrong(l) != d for l, d in measured.items())
print("PASS: done needs depth LIMIT + 2, so 1000002 for the real limit; counter plus reference are 40 bits")The soundness claim names the logic that must not depend on the threshold, and a second small size that would expose a dependence.
The real value is proved by induction, with the helper written and proved; a deeper bounded run is not offered as proof.
No bound is a tautology: a limit on a W-bit signal below its maximum value, never at it.
Run two small sizes before the real one and compare them: limit 5 hides the compare fault, limit 12 fails at step 5. When the real-size proof does not close, read the induction failure: with the helper off at limit 1,000,000 the step fails because the counter and the reference may start apart, and h_same ties them. Check each bound against its signal's maximum before trusting a pass: a bound at the maximum value removes nothing, as the last run shows.
It must run to depth 1,000,002 to see done fire. A shorter bounded run never reaches the state where the property can fail, so it is bounded to its depth only.