Every bounded pass carries an invisible remainder: everything past the bound. A bug that needs more steps than the bound is not unlikely or corner-case, it is simply unexamined. This lesson makes the remainder visible with a bug that sits exactly one step past a passing bound, so that bounded to N is read as a measured statement rather than a certificate.
A bounded run to depth D checks steps 0 to D minus 1. A violation at step D or later might as well not exist as far as the verdict is concerned. The pointer controller below tracks a 4-entry FIFO with 3-bit pointers; its faulty variant reloads the write pointer with 4 instead of 0 when it wraps from 7. Nothing is wrong on the first lap: the fault needs 8 pushes, twice the number of entries, with enough pops in between to keep the FIFO from filling. Depth 9 passes and depth 10 fails. The design did not change between the two runs; the search simply looked one step further. A bounded pass is therefore always reported with its N, and N is signoff-grade only with a justification: a diameter argument, a recurrence argument, or an inductive proof that removes the bound.
The fault shows on the eighth push, at step 8, and the count it corrupts is read at step 9. Depth 9 examines steps 0 to 8 and never sees the bad count; depth 10 does. The cover of the wrap event tells the same story from the other side: it is not reached within 9 (inconclusive: the trigger never fired inside the bound) and is reached within 10. The good controller is proven outright at depth 4, because its occupancy property is inductive however many laps the pointers take.
// formal: bmc 9 expect pass slang top fifo_ptr_ctl define BUG=1
`define FORMAL
// fifo_ptr_ctl: pointer controller of a 4-entry FIFO (lesson-local module, no data path).
// 3-bit pointers: bits 1:0 pick a slot, bit 2 is the lap bit. count = wp - rp.
// BUG = 1: when the write pointer wraps from 7 it reloads 4 instead of 0, so the fault
// only shows on the second lap of the write pointer (8 pushes).
module fifo_ptr_ctl #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire push,
input wire pop,
output wire [2:0] count,
output wire full,
output wire empty
);
reg [2:0] wp, rp;
assign count = wp - rp;
assign full = (count == 3'd4);
assign empty = (count == 3'd0);
wire do_push = push && !full;
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) begin
wp <= 3'd0;
rp <= 3'd0;
end else begin
if (do_push) wp <= (BUG == 1 && wp == 3'd7) ? 3'd4 : wp + 3'd1;
if (do_pop) rp <= rp + 3'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= 3'd4);
// sticky flag: the write pointer has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (do_push && wp == 3'd7) wrapped <= 1'b1;
end
always @(*) if (!init) c_wrapped: cover (wrapped);
`endif
endmoduleBounded to 9: the run examines every input sequence of up to 9 steps and the corrupted count first exists at step 9, outside the window. The pass is honest and narrow.
// formal: bmc 10 expect fail slang top fifo_ptr_ctl define BUG=1
`define FORMAL
// fifo_ptr_ctl: pointer controller of a 4-entry FIFO (lesson-local module, no data path).
// 3-bit pointers: bits 1:0 pick a slot, bit 2 is the lap bit. count = wp - rp.
// BUG = 1: when the write pointer wraps from 7 it reloads 4 instead of 0, so the fault
// only shows on the second lap of the write pointer (8 pushes).
module fifo_ptr_ctl #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire push,
input wire pop,
output wire [2:0] count,
output wire full,
output wire empty
);
reg [2:0] wp, rp;
assign count = wp - rp;
assign full = (count == 3'd4);
assign empty = (count == 3'd0);
wire do_push = push && !full;
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) begin
wp <= 3'd0;
rp <= 3'd0;
end else begin
if (do_push) wp <= (BUG == 1 && wp == 3'd7) ? 3'd4 : wp + 3'd1;
if (do_pop) rp <= rp + 3'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= 3'd4);
// sticky flag: the write pointer has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (do_push && wp == 3'd7) wrapped <= 1'b1;
end
always @(*) if (!init) c_wrapped: cover (wrapped);
`endif
endmodule// formal: cover 9 expect fail slang top fifo_ptr_ctl
`define FORMAL
// fifo_ptr_ctl: pointer controller of a 4-entry FIFO (lesson-local module, no data path).
// 3-bit pointers: bits 1:0 pick a slot, bit 2 is the lap bit. count = wp - rp.
// BUG = 1: when the write pointer wraps from 7 it reloads 4 instead of 0, so the fault
// only shows on the second lap of the write pointer (8 pushes).
module fifo_ptr_ctl #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire push,
input wire pop,
output wire [2:0] count,
output wire full,
output wire empty
);
reg [2:0] wp, rp;
assign count = wp - rp;
assign full = (count == 3'd4);
assign empty = (count == 3'd0);
wire do_push = push && !full;
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) begin
wp <= 3'd0;
rp <= 3'd0;
end else begin
if (do_push) wp <= (BUG == 1 && wp == 3'd7) ? 3'd4 : wp + 3'd1;
if (do_pop) rp <= rp + 3'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= 3'd4);
// sticky flag: the write pointer has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (do_push && wp == 3'd7) wrapped <= 1'b1;
end
always @(*) if (!init) c_wrapped: cover (wrapped);
`endif
endmodule// formal: cover 10 expect reached slang top fifo_ptr_ctl
`define FORMAL
// fifo_ptr_ctl: pointer controller of a 4-entry FIFO (lesson-local module, no data path).
// 3-bit pointers: bits 1:0 pick a slot, bit 2 is the lap bit. count = wp - rp.
// BUG = 1: when the write pointer wraps from 7 it reloads 4 instead of 0, so the fault
// only shows on the second lap of the write pointer (8 pushes).
module fifo_ptr_ctl #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire push,
input wire pop,
output wire [2:0] count,
output wire full,
output wire empty
);
reg [2:0] wp, rp;
assign count = wp - rp;
assign full = (count == 3'd4);
assign empty = (count == 3'd0);
wire do_push = push && !full;
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) begin
wp <= 3'd0;
rp <= 3'd0;
end else begin
if (do_push) wp <= (BUG == 1 && wp == 3'd7) ? 3'd4 : wp + 3'd1;
if (do_pop) rp <= rp + 3'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= 3'd4);
// sticky flag: the write pointer has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (do_push && wp == 3'd7) wrapped <= 1'b1;
end
always @(*) if (!init) c_wrapped: cover (wrapped);
`endif
endmodule// formal: prove 4 expect pass slang top fifo_ptr_ctl
`define FORMAL
// fifo_ptr_ctl: pointer controller of a 4-entry FIFO (lesson-local module, no data path).
// 3-bit pointers: bits 1:0 pick a slot, bit 2 is the lap bit. count = wp - rp.
// BUG = 1: when the write pointer wraps from 7 it reloads 4 instead of 0, so the fault
// only shows on the second lap of the write pointer (8 pushes).
module fifo_ptr_ctl #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire push,
input wire pop,
output wire [2:0] count,
output wire full,
output wire empty
);
reg [2:0] wp, rp;
assign count = wp - rp;
assign full = (count == 3'd4);
assign empty = (count == 3'd0);
wire do_push = push && !full;
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) begin
wp <= 3'd0;
rp <= 3'd0;
end else begin
if (do_push) wp <= (BUG == 1 && wp == 3'd7) ? 3'd4 : wp + 3'd1;
if (do_pop) rp <= rp + 3'd1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= 3'd4);
// sticky flag: the write pointer has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (do_push && wp == 3'd7) wrapped <= 1'b1;
end
always @(*) if (!init) c_wrapped: cover (wrapped);
`endif
endmoduleThe table is one shortest input sequence for the failing run: a push, then a push together with a pop every cycle so the FIFO never fills. The solver may choose other inputs; none is shorter, because depth 9 passes. The script replays the sequence on an explicit model of the controller and also searches all input sequences for the earliest violation: step 9 for the faulty design, none for the good one.
Step | Inputs at this step | wp | rp | count, faulty | count, correct |
|---|---|---|---|---|---|
1 | push | 0 | 0 | 0 | 0 |
2 to 7 | push and pop | 1 to 6 | 0 to 5 | 1 | 1 |
8 | push and pop, with wp = 7 | 7 | 6 | 1 | 1 |
9 | (effect of step 8) | 4 (correct: 0) | 7 | 5, above 4 | 1 |
from itertools import product
def step(state, push, pop, reload):
"""One clock edge of the pointer controller; reload is the value the write pointer takes after 7."""
wp, rp = state
count = (wp - rp) % 8
do_push = push and count != 4
do_pop = pop and count != 0
if do_push:
wp = reload if wp == 7 else wp + 1
if do_pop:
rp = (rp + 1) % 8
return (wp, rp)
def count_of(state):
return (state[0] - state[1]) % 8
def first_violation(reload, limit=40):
"""Earliest step (reset state = step 1) at which count > 4, over ALL input sequences."""
seen, layer = {(0, 0)}, {(0, 0)}
for s in range(1, limit + 1):
if any(count_of(st) > 4 for st in layer):
return s
nxt = set()
for st in layer:
for push, pop in product((0, 1), repeat=2):
nxt.add(step(st, push, pop, reload))
layer = nxt - seen
seen |= nxt
if not layer:
return None # fixed point reached: no violation on any lap
return None
# replay of the table: one push, then push and pop together
seq = [(1, 0)] + [(1, 1)] * 7
def replay(reload):
st, counts = (0, 0), []
for push, pop in seq:
st = step(st, push, pop, reload)
counts.append(count_of(st))
return counts
def check_count_in_range(reload):
for c in replay(reload):
assert c <= 4, "count above 4"
check_count_in_range(0) # correct reload: the replay stays in range
assert replay(4)[:-1] == [1] * 7 and replay(4)[-1] == 5 # faulty reload: step 9 reads 5
caught = False
try:
check_count_in_range(4) # injected fault: the same check must fail
except AssertionError:
caught = True
assert caught, "the range check accepted the faulty wrap"
assert first_violation(4) == 9 # the run: depth 9 passes, depth 10 fails
assert first_violation(0) is None # the good controller never violates, on any lap
print("PASS: the faulty wrap first shows at step 9 (depth 10); the good controller never violates")How to read it: one slot is one step, counted from the first step after reset, so slot 1 is step 1; the inputs are those of the table above. push is high in steps 1 to 8 and pop in steps 2 to 8, so step 1 is a push alone and steps 2 to 8 are a push together with a pop; both are low in step 9. wp_bug and wp_good count 0 to 7 in steps 1 to 8, the first lap, and rp is 0 in steps 1 and 2, then 1 to 7, one behind. count_bug and count_good read 0 in step 1 and 1 in steps 2 to 8, the same on both. In step 9, the effect of step 8, wp_bug reads 4, the reload, where wp_good reads 0, and count_bug reads 5 where count_good still reads 1. ok_bug, the check that the count is at most 4, is high through step 8 and drops in step 9; ok_good stays high. A bounded run of depth 9 examines steps 0 to 8 and sees only the high part of that lane.
The report says bounded to N with N printed next to the verdict, never a bare pass.
The lesson names the step the bug needs and shows the passing bound sitting below it.
Deep-trigger mutations exist for every bounded property, proving the bound is load-bearing.
Test every bounded property with a mutant whose trigger sits past the bound: move a wrap constant, delay a pulse, deepen a FIFO. If the property still passes, the bound is below the trigger and the pass says nothing about that bug class. Then either lengthen the bound past the trigger or replace the bounded check with induction, as the last block does for the good controller. Write the report line as: occupancy property, bounded to 9 steps, wrap trigger needs 10, inconclusive.
Unknown: the trigger completes at step 41 or later, outside the window. Extend past reset plus trigger plus latency plus 1, or prove inductively.