A report that says the base case passed is routinely filed as a proof, and it is not one. The base case checks the first k states from reset; the induction step checks every k-window anywhere, including states reset can never produce. Either half alone proves nothing unbounded. This lesson states both obligations as mathematics, passes both on the counter, and shows the misread: a run whose base passes while its step fails.
K-induction proves that P holds in every reachable state. The base obligation says: starting from the initial state and following the transition relation for k minus 1 steps, P holds in each of the k states reached. The step obligation says: take any k consecutive states, with no initial-state condition, that follow the transition relation and each satisfy P; then P holds in the state after them. Together they cover everything: the base anchors the start, and the step extends the guarantee forward one state at a time, forever. The step's anywhere is load-bearing: it is what generalises beyond the bound, and it is what admits spurious failures from unreachable states.
The base quantifies over the reachable prefix, because Init and Trans pin the states; the step quantifies over all states, because nothing but Trans and P constrains them. A verdict needs both, to the same k: a step at k equal to 6 with a base at k equal to 3 leaves states 3 to 5 covered by neither half.
The full counter property set, helper included, closes at k equal to 2: at k equal to 1 the two transition properties, which read the previous cycle through $past, cannot be inductive because a single state carries no past, and at k equal to 2 both halves pass. Remove the helper and the same set reports unproven at depth 10: the base still passes, because every reachable state satisfies never-15, but the step fails on a trace through the unreachable states 10 to 14. The last block is the misread made concrete: the base half alone, which is the bounded line of the report, passes at depth 10 and looks exactly like a proof.
// formal: prove 1 expect unproven slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
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);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
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
// sticky flag: the counter has wrapped at least once
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
endmoduleAt k equal to 1 the base passes and the step fails: the transition properties need two states. This is a statement about the properties, not a defect in the counter.
// formal: prove 2 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
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);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
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
// sticky flag: the counter has wrapped at least once
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
endmoduleAt k equal to 2 base and step both pass. With the helper count within 9 present, the never-15 property is inductive, and the full set is proven for this model under its assumptions.
// formal: prove 10 expect unproven slang top mod10_counter define HELPER=0
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
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);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
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
// sticky flag: the counter has wrapped at least once
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
endmoduleHelper removed, at depth 10: the base case passes while the induction step fails on never-15. The verdict is inconclusive, not failed: the property is true on every reachable state, but the step cannot establish it from arbitrary states.
// formal: bmc 10 expect pass slang top mod10_counter define HELPER=0
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
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);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
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
// sticky flag: the counter has wrapped at least once
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
endmoduleThe same model with only the bounded half: no violation within 10 steps. Filed as a proof it would be the mismatch of lengths this lesson warns about; filed as bounded to 10 it is true and narrow.
Run | Base | Step | Verdict |
|---|---|---|---|
Full set, helper on, k = 1 | Pass | Fail on the transition properties | Inconclusive: they need two states |
Full set, helper on, k = 2 | Pass | Pass | Proven for this model and assumptions |
Helper removed, k = 10 | Pass | Fail on never-15 | Inconclusive: step undecided |
Helper removed, bounded line only | Pass to depth 10 | Not run | Bounded to 10, not a proof |
The report quotes base and step statuses separately, at the same depth, before claiming proven.
Every unproven verdict names the failing step obligation and the property it fails on.
Transition properties that read history run at k of at least 2, since one state carries no past.
Recheck any unproven run by asking which half failed: a failing base is a reachable bug or a bad reset model, fixed like any counterexample, while a failing step with a passing base is a candidate CTI, handled in the next lesson. Never lengthen only one half: base and step depths move together.
Not necessarily a bug, and not necessarily safe either: the step failure may start from an unreachable state, which makes it a counterexample to induction, or it may start from a reachable state that a longer bounded run would reach. The next lesson reads exactly this trace and shows how to decide.