A single claim about a decade counter, that its count is never 15, is true and gives the solver one problem with no midpoint. A variant with a bug may not even trip it. Split into layers, each failure points at one behaviour, and the range invariant that emerges doubles as the helper the induction needs.
Job of this lesson: split a monolith into layers, and climb a parameter ladder where every rung has a run behind it.
Layering means one behaviour per property: range, outputs from state, transitions. Each layer is proven alone, and the target claim may rely on the proven shallower layers. Parameter work means proving at a small width, where counterexamples are short, then proving the real parameter directly. The closing argument is about the proof, not the width: each layer's step is the same two-case argument at every width and wrap value (below the wrap value the count adds one; at it, it returns to 0). A small run is evidence of that argument, not a replacement, so the real parameter has its own run. The ladder, every row from the runs below:
Rung | Counter | The one-line claim alone | The layered set |
|---|---|---|---|
1 | 2 bits, counts 0 to 1 | Unproven: base passes, step fails (block 3) | Proven, |
2 | 3 bits, counts 0 to 4 | Not run | Proven, |
3 | 4 bits, counts 0 to 9: the real decade counter | Unproven: step fails at k = 20 (block 1) | Proven, |
Block 1 is the real decade counter without its range helper. The claim is true, since only 0 to 9 are reachable, but the unreachable states 10 to 14 satisfy it and lead to 15, and with the enable low a state can repeat, so a longer window never helps. The base case passes and the step fails at k = 20, hence at every k up to 20: unproven, undetermined, never proven:
// formal: prove 20 expect unproven slang top mod10_counter define HELPER=0
`define FORMAL
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_not15: assert (count != 4'd15);
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmoduleBlock 2 adds the layer that emerges: the count is within 0 to 9. It is inductive on its own and makes the target claim inductive. With it the set is proven at depth 4:
// formal: prove 4 expect pass slang top mod10_counter
`define FORMAL
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_not15: assert (count != 4'd15);
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmoduleNow a lesson-local counter whose width and wrap value are parameters, so the rungs can be run. LAYERS=0 leaves only the one-line claim. At 2 bits counting 0 to 1, states 2 and 3 are unreachable and 2 leads to 3, so the claim leaks at once and the counterexample to induction is readable: count 2, held, then 3 (block 3):
// formal: prove 8 expect unproven slang top dec_counter define W=2 define LAST=1 define LAYERS=0
`define FORMAL
// Lesson-local: a counter from 0 to LAST that wraps to 0, W bits wide (LAST below 2^W - 1).
// a_top is the one-line claim "never all ones". LAYERS=1 adds three layered properties. BUG=1 wraps one count late.
module dec_counter #(parameter W = 4, parameter LAST = 9, parameter LAYERS = 1, parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
output reg [W-1:0] count,
output wire tc
);
wire [W-1:0] top = LAST + ((BUG == 1) ? 1 : 0);
assign tc = en && (count == top);
always @(posedge clk) begin
if (rst) count <= 0;
else if (en) count <= (count == top) ? 0 : count + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_top: assert (count != {W{1'b1}});
generate if (LAYERS) begin : g_layers
always @(*) if (!init) begin
l1_range: assert (count <= LAST);
l2_tc: assert (tc == (en && count == LAST));
end
always @(posedge clk) if (!init && !$past(rst))
l3_step: assert (!$past(en) || count == (($past(count) == LAST) ? 0 : $past(count) + 1'b1));
end endgenerate
`endif
endmoduleWith three layers on, l1_range, l2_tc (the terminal pulse follows the state) and l3_step (the transitions), the small counter is proven (block 4), and so is a 3-bit counter counting 0 to 4 (block 5):
// formal: prove 4 expect pass slang top dec_counter define W=2 define LAST=1
`define FORMAL
// Lesson-local: a counter from 0 to LAST that wraps to 0, W bits wide (LAST below 2^W - 1).
// a_top is the one-line claim "never all ones". LAYERS=1 adds three layered properties. BUG=1 wraps one count late.
module dec_counter #(parameter W = 4, parameter LAST = 9, parameter LAYERS = 1, parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
output reg [W-1:0] count,
output wire tc
);
wire [W-1:0] top = LAST + ((BUG == 1) ? 1 : 0);
assign tc = en && (count == top);
always @(posedge clk) begin
if (rst) count <= 0;
else if (en) count <= (count == top) ? 0 : count + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_top: assert (count != {W{1'b1}});
generate if (LAYERS) begin : g_layers
always @(*) if (!init) begin
l1_range: assert (count <= LAST);
l2_tc: assert (tc == (en && count == LAST));
end
always @(posedge clk) if (!init && !$past(rst))
l3_step: assert (!$past(en) || count == (($past(count) == LAST) ? 0 : $past(count) + 1'b1));
end endgenerate
`endif
endmodule// formal: prove 4 expect pass slang top dec_counter define W=3 define LAST=4
`define FORMAL
// Lesson-local: a counter from 0 to LAST that wraps to 0, W bits wide (LAST below 2^W - 1).
// a_top is the one-line claim "never all ones". LAYERS=1 adds three layered properties. BUG=1 wraps one count late.
module dec_counter #(parameter W = 4, parameter LAST = 9, parameter LAYERS = 1, parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
output reg [W-1:0] count,
output wire tc
);
wire [W-1:0] top = LAST + ((BUG == 1) ? 1 : 0);
assign tc = en && (count == top);
always @(posedge clk) begin
if (rst) count <= 0;
else if (en) count <= (count == top) ? 0 : count + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_top: assert (count != {W{1'b1}});
generate if (LAYERS) begin : g_layers
always @(*) if (!init) begin
l1_range: assert (count <= LAST);
l2_tc: assert (tc == (en && count == LAST));
end
always @(posedge clk) if (!init && !$past(rst))
l3_step: assert (!$past(en) || count == (($past(count) == LAST) ? 0 : $past(count) + 1'b1));
end endgenerate
`endif
endmoduleThe failing partner wraps one count late. The first layer to fail is the terminal pulse l2_tc, at step 5 (depth 5 passes, depth 6 fails): the state is still legal but the pulse is wrong, which points at one behaviour. Run alone, the range layer fails at step 6 and the transition layer at step 7 (block 6). Block 7 shows why layers earn their place: with only the one-line claim the same bug passes to depth 12:
// formal: bmc 8 expect fail slang top dec_counter define W=3 define LAST=4 define BUG=1
`define FORMAL
// Lesson-local: a counter from 0 to LAST that wraps to 0, W bits wide (LAST below 2^W - 1).
// a_top is the one-line claim "never all ones". LAYERS=1 adds three layered properties. BUG=1 wraps one count late.
module dec_counter #(parameter W = 4, parameter LAST = 9, parameter LAYERS = 1, parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
output reg [W-1:0] count,
output wire tc
);
wire [W-1:0] top = LAST + ((BUG == 1) ? 1 : 0);
assign tc = en && (count == top);
always @(posedge clk) begin
if (rst) count <= 0;
else if (en) count <= (count == top) ? 0 : count + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_top: assert (count != {W{1'b1}});
generate if (LAYERS) begin : g_layers
always @(*) if (!init) begin
l1_range: assert (count <= LAST);
l2_tc: assert (tc == (en && count == LAST));
end
always @(posedge clk) if (!init && !$past(rst))
l3_step: assert (!$past(en) || count == (($past(count) == LAST) ? 0 : $past(count) + 1'b1));
end endgenerate
`endif
endmodule// formal: bmc 12 expect pass slang top dec_counter define W=3 define LAST=4 define BUG=1 define LAYERS=0
`define FORMAL
// Lesson-local: a counter from 0 to LAST that wraps to 0, W bits wide (LAST below 2^W - 1).
// a_top is the one-line claim "never all ones". LAYERS=1 adds three layered properties. BUG=1 wraps one count late.
module dec_counter #(parameter W = 4, parameter LAST = 9, parameter LAYERS = 1, parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
output reg [W-1:0] count,
output wire tc
);
wire [W-1:0] top = LAST + ((BUG == 1) ? 1 : 0);
assign tc = en && (count == top);
always @(posedge clk) begin
if (rst) count <= 0;
else if (en) count <= (count == top) ? 0 : count + 1'b1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_top: assert (count != {W{1'b1}});
generate if (LAYERS) begin : g_layers
always @(*) if (!init) begin
l1_range: assert (count <= LAST);
l2_tc: assert (tc == (en && count == LAST));
end
always @(posedge clk) if (!init && !$past(rst))
l3_step: assert (!$past(en) || count == (($past(count) == LAST) ? 0 : $past(count) + 1'b1));
end endgenerate
`endif
endmoduleThe script checks the closing argument: for every width up to 6 and every wrap value, the range layer is inductive, the one-line claim is not (unless exactly one state is unreachable and nothing leads into it), and a late wrap breaks the range layer. It also builds the chain of unreachable states the monolith leaks through:
def make(width, last, late=0):
n, top = 2 ** width, last + late
def step(s, en):
if not en:
return s
return 0 if s == top else (s + 1) % n
return step, n
def inductive(inv, step, n):
return all(inv(step(s, e)) for s in range(n) if inv(s) for e in (0, 1))
def chain(width, last):
step, n = make(width, last)
out, s = [], last + 1
while s != n - 1:
out.append(s)
s = step(s, 1)
return out
checked = 0
for width in range(2, 7):
for last in range(1, 2 ** width - 1):
step, n = make(width, last)
assert inductive(lambda s: s <= last, step, n) # layer 1 is inductive at every size
one_line = lambda s: s != n - 1
leaks = last <= n - 3 # at least one unreachable state leads in
assert inductive(one_line, step, n) == (not leaks)
late_step, _ = make(width, last, late=1)
if last + 1 < n:
assert not inductive(lambda s: s <= last, late_step, n) # a late wrap breaks layer 1
checked += 1
assert chain(2, 1) == [2]
assert chain(3, 4) == [5, 6]
assert chain(4, 9) == [10, 11, 12, 13, 14] # the counterexample chain on the real counter
print("PASS: layer 1 inductive at all", checked, "sizes; the one-line claim leaks; chains match the runs")Properties are layered by behaviour, and the layers catch a bug the one-line claim misses.
Helpers are asserted and proven, never only assumed; every rung has a run, and the real parameter its own proof.
When the layered set passes but the monolith failed, keep both on record: the failure was the symptom, the layers the diagnosis. When a helper is added, rerun the base case too; an invariant that fails there is false, and a proof built on it is conditional on a lie.
Not yet: a failing step from unreachable states is spurious until strengthened. Add the invariant, prove it, and only then read a surviving failure as a bug.