A watchdog counter with a flaw shows it in a bounded run at 4 bits wide. The same flaw at 24 bits passes the same run, because the depth it needs is millions of cycles and the run stopped at 20. The runs look identical until someone asks what depth the flaw needs. The team that measures first reduces the width and moves on; the team that tunes flags first loses the week.
Job of this lesson: turn a slow or suspiciously quick proof into three measurements and one action, in that order.
Non-convergence has four causes, checked in order: the cone is too wide, the depth needed is beyond reach, the engine has stalled, or the induction step fails. The response is fixed: diagnose from the numbers, then reduce the model, split the work, or strengthen the invariant. Raising the time limit is not a response; a timeout is inconclusive. Tightening assumptions is the last resort and needs a written justification, because it can hide bugs.
Measurement | Healthy sign | Sick sign | First action |
|---|---|---|---|
Cone size per property | Matches the expected logic | Whole datapath in a control property | Reduce: cut points, narrower counters |
Depth reached against depth needed | Steady progress to the target | Stalled, or far below it | Reduce the parameter, or split the bound |
Engine report | Base and step both move | Step fails from unreachable states | Strengthen: helper invariants |
Assumption list | Short, reviewed, discharged | Growing with every rerun | Stop: review, justify in writing, or revert |
The lesson-local watchdog counts while a request holds and clears otherwise; the property says it never reaches all ones. It is false by construction, which makes it a good probe: a held request walks the counter there. W is the counter width. At W = 4 a bounded run to depth 20 finds the counterexample: depth 16 passes and depth 17 fails, because the counter reads 0 at step 1 and all ones at step 16:
// formal: bmc 20 expect fail slang top timeout_wait define W=4
`define FORMAL
// Lesson-local: a request-persistence watchdog. The counter runs while req holds and clears otherwise.
// The property says it never reaches the all-ones value. W is the counter width.
module timeout_wait #(parameter W = 4) (
input wire clk,
input wire rst,
input wire req
);
reg [W-1:0] c;
always @(posedge clk) begin
if (rst) c <= 0;
else if (req) c <= c + 1'b1;
else c <= 0;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_bound: assert (c != {W{1'b1}});
`endif
endmoduleThe same module at W = 24 passes the bounded check to depth 20: bounded to 20, silent about depth 21 and beyond. The induction step fails at k = 20, so the run ends unproven: neither a proof nor a counterexample. Nothing in the result or the timing reveals that the claim is false; the counterexample sits at depth 16,777,217 (formula checked below against the measured depth 17 at W = 4):
// formal: prove 20 expect unproven slang top timeout_wait define W=24
`define FORMAL
// Lesson-local: a request-persistence watchdog. The counter runs while req holds and clears otherwise.
// The property says it never reaches the all-ones value. W is the counter width.
module timeout_wait #(parameter W = 4) (
input wire clk,
input wire rst,
input wire req
);
reg [W-1:0] c;
always @(posedge clk) begin
if (rst) c <= 0;
else if (req) c <= c + 1'b1;
else c <= 0;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_bound: assert (c != {W{1'b1}});
`endif
endmoduleThe step fails because it may start one below all ones, a state that satisfies the claim and leads out of it, and no 20-step run from reset reaches it. The cure is not a longer run: reduce the parameter until the flaw is visible (the 4-bit run), then argue the logic is the same at 24 bits, or bound the counter by an invariant. The script checks the depth formula against the measured pair, scales it to 24 bits, and maps measurements to an action; its stall detector is tried on a stalled and a moving reading.
def needed_depth(width):
# a held request: the counter reads 0 at step 1 and all ones at step 2**width,
# so a counterexample needs a bound of 2**width + 1 steps
return 2 ** width + 1
assert needed_depth(4) == 17 # measured: depth 16 passes, depth 17 fails
assert needed_depth(24) == 16777217
bound = 20
assert bound >= needed_depth(4) # the narrow run sees the flaw
assert bound < needed_depth(24) # the wide run passes the bounded check and still hides it
assert 2 ** 24 // 2 ** 4 == 1048576 # 24-bit counter: a million times the state space
def stalled(readings, window=3):
# readings: (minute, depth reached); stalled when the depth has not grown over the last readings
last = [d for _, d in readings[-window:]]
return len(last) == window and last[-1] == last[0]
def recommend(cone_ok, depth_moving, step_from_reachable):
if not cone_ok:
return "reduce"
if not depth_moving:
return "split"
if not step_from_reachable:
return "strengthen"
return "rerun-in-budget"
moving = [(1, 10), (2, 25), (3, 40)]
stuck = [(1, 10), (2, 40), (3, 40), (4, 40)]
assert not stalled(moving) and stalled(stuck)
assert recommend(True, not stalled(moving), True) == "rerun-in-budget"
assert recommend(True, not stalled(stuck), True) == "split"
assert recommend(False, True, True) == "reduce"
assert recommend(True, True, False) == "strengthen"
print("PASS: depth formula matches the measured pair; stalled readings are recommended for a split")A slow proof has recorded numbers: cone size, state bits, depth against time.
Every bounded pass states its bound and the depth the property needs.
The action matches the measurement; the time limit was not raised as a fix.
Reproduce on the small parameter first: if the 4-bit version fails or converges and the 24-bit version does neither, the cause is size, not logic. Compare the cone against the schematic before abstracting; abstracting logic the property needs produces a spurious failure.
Strengthen: add helper invariants that tie the state elements together, and prove each helper rather than assuming it.
A proof that needs more time: the engine is stuck, not slow. Split the bound or the property, or reduce the model, instead of raising the limit.