The most confusing trace in formal work starts in a state the design can never reach and ends in a property violation. Newcomers file it as a bug; veterans recognise a counterexample to induction. Telling the two apart decides whether the fix belongs in the RTL or in the proof, and the wrong call wastes a week in either direction.
The induction step starts from arbitrary states, so its failing trace may begin anywhere, including the unreachable region. Such a trace is spurious as a bug report and decisive as a proof diagnostic: it names the unreachable states the property cannot exclude. On the counter, the property count never 15 is satisfied by the unreachable states 10 to 14 and broken by 15, so the window 10 to 14 followed by 15 is a failing step. While enable can hold any state forever, arbitrarily long satisfying windows sit before the violation: no k closes the step. Hold enable high and the longest violating window is exactly the five-state chain 10 to 14, so k equal to 6 should be the minimum there. The runs below measure both cases.
The measuring models keep only the state properties, so a step failure is about never-15 alone. The free-enable model is the real design; the enable-high model adds the assumption that enable is always high, a different model used only to measure the chain length, not a fix.
// formal: prove 20 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
`endif
endmoduleFree enable, helper removed, depth 20: base passes, step fails on never-15. The property holds on all reachable states, so this is a proof gap, not a design bug.
// formal: prove 5 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) u_en: assume (en); // a different model: the environment never stalls the counter
`endif
endmodule// formal: prove 6 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) u_en: assume (en); // a different model: the environment never stalls the counter
`endif
endmoduleWith enable held high the step fails at k equal to 5 and passes at k equal to 6, as the chain length predicts: five unreachable states satisfy never-15 in a row before 15.
// formal: prove 1 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
`endif
endmoduleHelper present: the range bound count within 9 excludes the whole unreachable region, the step has nowhere spurious to start, and never-15 closes at k equal to 1. The helper is doing the work the step alone cannot.
k | Free enable: base | Free enable: step | Enable held high: base | Enable held high: step |
|---|---|---|---|---|
1 to 5 | Pass | Fail | Pass | Fail |
6 | Pass | Fail | Pass | Pass |
7 | Pass | Fail | Pass | Pass |
10 | Pass | Fail | Not run | Not run |
20 | Pass | Fail | Not run | Not run |
Each cell is one prove run of the model in the column head, with only the depth in the header changed; the blocks above carry the story. Free enable did not close at any k tested up to 20, which is a measurement and not a proof that no k closes; enable high closes at 6.
The script enumerates violating windows directly: the longest run of satisfying states that ends in a violation, and whether arbitrarily long such runs exist. With enable free, the self loops make violating runs arbitrarily long, so no finite k exists. With enable held high, the longest violating run is the five-state chain 10 to 14, giving minimum k equal to 6, the value the runs measured. A wrap constant of 8 is an illustrative variant that was not run: it lengthens the chain and moves the minimum to 7, and a claim that k equal to 5 suffices is caught by exhibiting the violating window.
def succ(s, en_free, last):
outs = {s} if en_free else set()
outs.add(0 if s == last else (s + 1) % 16)
return outs
def on_cycle(P, en_free, last):
succs = {s: succ(s, en_free, last) for s in range(16)}
cyc = set()
for s in P:
seen, stack = set(), [s]
while stack:
u = stack.pop()
for t in succs[u]:
if t == s:
cyc.add(s)
elif t in P and t not in seen:
seen.add(t)
stack.append(t)
return cyc
def min_k(P, en_free, last):
succs = {s: succ(s, en_free, last) for s in range(16)}
bad = [(u, v) for u in P for v in succs[u] if v not in P]
if not bad:
return 1
reach = set(on_cycle(P, en_free, last))
frontier = list(reach)
while frontier:
u = frontier.pop()
for t in succs[u]:
if t in P and t not in reach:
reach.add(t)
frontier.append(t)
if any(u in reach for u, v in bad):
return None # arbitrarily long violating runs exist
best = [0]
def dfs(s, n, seen):
for t in succs[s]:
if t not in P:
best[0] = max(best[0], n)
elif t not in seen:
dfs(t, n + 1, seen | {t})
for s in P:
dfs(s, 1, {s})
return best[0] + 1
P = {s for s in range(16) if s != 15}
assert min_k(P, True, 9) is None # free enable: the runs fail at every k tested
assert min_k(P, False, 9) == 6 # enable held high: the runs fail at 5 and pass at 6
assert min_k(P, False, 8) == 7 # illustrative variant (wrap at 8, not run): the minimum moves
# failing variant: claiming k = 5 suffices with wrap at 8
def window_violates(k, en_free, last):
succs = {s: succ(s, en_free, last) for s in range(16)}
found = []
def dfs(s, n, seen):
for t in succs[s]:
if t not in P:
if n == k:
found.append(True)
elif t not in seen and n < k:
dfs(t, n + 1, seen | {t})
for s in P:
dfs(s, 1, {s})
return bool(found)
caught = False
try:
assert not window_violates(5, False, 8) # must fail: 10..14 then 15
except AssertionError:
caught = True
assert caught, "window check missed the length-5 violating run"
print("PASS: no finite k with free enable; k = 6 with enable high, moved to 7 by the wrap change")Step | Count | Satisfies never-15 | Note |
|---|---|---|---|
0 to 4 | 10 to 14 | Yes, all five | Unreachable chain, enable high |
5 | 15 | No | The CTI ends here; the design never starts here |
This table is the trace the failing step encodes: a window of five states that satisfy the property and are followed by the violation. The failing step of the enable-high run at k equal to 5 returns this window: it starts at 10 and ends at 15. The waveform replays it in simulation, with the counter started in state 10.
How to read it: one slot is one step, so slot 1 is step 0. rst is low and en is high in every slot: reset is never applied, because this start state cannot come from reset. count is shown in hexadecimal and reads a, b, c, d, e, f, which are 10, 11, 12, 13, 14 and 15, one per step. range_ok, the range bound that the count is at most 9, is low in every slot: the start state and every state after it lie outside the reachable range. not15_ok, the property that the count is not 15, is high in steps 0 to 4, the five states of the window, and drops in step 5, where the count is 15.
Every step failure is classified spurious or real before any RTL or proof change.
Spurious verdicts name the unreachable start states and the helper that would exclude them.
The claimed minimum k is measured by runs and reproduced by an argument like the enumeration above, not guessed.
Decide spurious or real by checking the CTI start against what is known about the reachable set. A start is spurious when something excludes it: a proven helper invariant that it violates, or an exact reachable set, as the ten states of the counter by enumeration. A bounded run from reset that does not reach the start proves nothing about it: not reached within N is inconclusive, so it cannot make a CTI spurious on its own. If the start is reachable, the trace is a real bug with a short trace, and the fix belongs in the design. Never strengthen blindly against a real trace.
Spurious: 12 is outside the exact reachable set 0 to 9, and enable low holds it there. The window 12, 12, then a high enable stepping toward 15 is a proof artefact. Exclude 10 to 15 with the range helper instead of touching the design.