The symptom: a proof that a decade counter never reads 15 passes its bounded check to any depth, and fails its induction step at every window you try. The property is true and unprovable as stated, because the induction step starts in states that reset can never produce. One extra assertion repairs it, but only if it is itself proved. This lesson makes you find it, measure the window it needs, replay the idea on the FIFO, and then judge a proof that passes with a fault planted.
The counter below, which counts 0 to 9 and wraps, with properties: never 15, the terminal pulse, the step rule, the hold rule, and three covers. It has a BUG switch (W1) and no helper.
The FIFO of stage 1 with its helper assertion switched off by HELPER=0.
A small counter module with a bound check and a fault planted, with the variant lines read last.
// formal: prove 10 expect unproven slang top mod10_counter
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified).
module mod10_counter #(parameter BUG = 0) (
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);
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
endmodule// formal: bmc 20 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified).
module mod10_counter #(parameter BUG = 0) (
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);
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
endmoduleThe first block's expected outcome is unproven: the bounded check passes and the induction step fails. The second is a bounded pass to depth 20, which proves nothing unbounded.
// formal: prove 12 expect unproven slang top sync_fifo define HELPER=0
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO with a combinational read of the oldest word.
// Synchronous active-high reset. count is an output so that properties can see it.
// BUG selects a variant (0 is the design as specified); HELPER=0 removes the helper assertion.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: the first cycle is a reset, the state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (they read history, so skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
// ---- data integrity by tracked-slot abstraction: one free slot, one shadow value ----
// The free constant is an anyconst wire that is also assumed equal to its one-cycle-old copy;
// this form works in both front ends, while a clocked assume of stability lags one step.
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv; // the tracked slot holds a word we are watching
reg [7:0] td; // the value that should be there
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
// ---- covers: the triggers of the properties can happen ----
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
c_tracked_read: cover (tv && !empty && rptr == tslot);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule// formal: bmc 6 expect pass slang top bound_check define BUG=1
`define FORMAL
// lesson-local counter with a small bound, first form
module bound_check #(parameter BUG = 0) (
input wire clk,
input wire rst,
output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (BUG == 1 && c == 2'd2) c <= 2'd3;
else c <= (c == 2'd2) ? 2'd0 : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
assume (c <= 2'd2);
a_never3: assert (c != 2'd3);
end
`endif
endmoduleThe last block passes with the fault planted: that is what you are asked to explain.
def step(c, en):
return c if not en else (0 if c == 9 else (c + 1) & 15)
def reachable():
seen, todo = {0}, [0]
while todo:
c = todo.pop()
for en in (0, 1):
n = step(c, en)
if n not in seen:
seen.add(n)
todo.append(n)
return seen
REACH = reachable()
assert REACH == set(range(10))
P = lambda c: c != 15
def cti(k, helper=lambda c: True, ens=(0, 1)):
"""Is there a path of k states, all satisfying P and the helper, whose next state violates P?"""
cur = {c for c in range(16) if P(c) and helper(c)}
for _ in range(k - 1):
cur = {step(c, e) for c in cur for e in ens if P(step(c, e)) and helper(step(c, e))}
return any(not P(step(c, e)) for c in cur for e in ens)
def inductive(h):
return all(h(step(c, e)) for c in range(16) if h(c) for e in (0, 1))
assert all(cti(k) for k in range(1, 21)), "with a free enable no window closes the step"
assert [k for k in range(1, 12) if not cti(k, ens=(1,))] == [6, 7, 8, 9, 10, 11], "with the enable forced high the step closes at window 6"
assert 14 not in REACH
ok = lambda c: c <= 9
assert inductive(ok) and not any(cti(k, ok) for k in range(1, 21))
forged = lambda c: c <= 10
assert not inductive(forged), "a helper that is not itself inductive is a wish, not a proof"
print("PASS: the model reproduces the stalled step, the window with a forced enable, and the repair")Produce | How |
|---|---|
The reason the counter's step stalls | Name a start state of a failing step, say whether reset can reach it, and say why no window helps when the enable can stay low. |
A helper assertion that closes it | State it, show it is inductive on its own, and report the smallest window of the proof with it, for the whole property set and for the two-property subset. |
The same analysis for the FIFO | Which property fails its step without the helper, what the helper says, and the smallest window with it. |
An explanation of the last block | Why the planted fault does not show, and a rewrite of the module in which it does. |
Rows |
|
Variant | Edit the header of the block above to | Expected category |
|---|---|---|
W1 |
| counterexample |
The model's asserts hold, and your helper survives the same inductive test it applies to the forged one.
Your rewrite of the small counter module fails at a depth you report.
The inconclusive rows cite runs whose induction step failed, and the package check passes.
# ---- formal lab results ledger, engine v2: every row cites a typed run (kind, depth, outcome[, design]) ----
STATUS = ("proven", "bounded", "cex", "cover-reached", "inconclusive")
FROM_RUN = {"proven": {("prove", "proved")},
"bounded": {("bmc", "bounded")},
"cex": {("bmc", "counterexample"), ("prove", "counterexample")},
"cover-reached": {("cover", "reached")},
"inconclusive": {("prove", "unproven"), ("cover", "not-reached")}}
NEED = {"sync_fifo": 9, "rr_arbiter": 5, "hs_bridge": 4, "csr_block": 3,
"pipe3": 5, "pipe3_eq": 5, "mod10_counter": 15, "toggle_demo": 4}
KEYS = ("property", "design", "status", "bound", "why", "run", "assumes", "cover", "kills", "rev")
REV = 3
ALWAYS = "reset-at-step-0"
TRACKED = "tracked-constant-stable"
def row_problems(e, runs, tracked):
n = e.get("property", "?")
miss = [k for k in KEYS if k not in e]
if miss:
return ["missing-field:%s:%s" % (n, ",".join(miss))]
if e["status"] not in STATUS:
return ["bad-status:" + n]
p = []
if e["rev"] != REV:
p.append("stale:" + n)
if e["run"] not in runs:
return p + ["no-such-run:" + n]
kind, depth, outcome = runs[e["run"]][:3]
if len(runs[e["run"]]) > 3 and runs[e["run"]][3] != e["design"]:
p.append("run-of-another-design:" + n) # a run typed with its design may be cited only by that design's rows
if (kind, outcome) not in FROM_RUN[e["status"]]:
p.append("status-not-from-run:" + n)
if e["bound"] != depth:
p.append("bound-not-run-depth:" + n)
has_cover = bool(str(e["cover"]).strip())
if e["status"] in ("proven", "bounded") and not (has_cover and e["kills"]):
p.append("no-evidence:" + n)
if e["status"] == "cover-reached" and not has_cover:
p.append("no-evidence:" + n)
if e["status"] == "cex" and not e["kills"]:
p.append("no-evidence:" + n)
if e["status"] == "bounded":
if e["design"] not in NEED:
p.append("unknown-design:" + n)
elif depth < NEED[e["design"]]:
p.append("short-bound:" + n)
if len(str(e["why"]).strip()) < 12:
p.append("unjustified:" + n)
if ALWAYS not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, ALWAYS))
if n in tracked and TRACKED not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, TRACKED))
return p
def ledger_ok(ledger, runs, required, mutants, register, tracked, final=True):
names = [e.get("property") for e in ledger]
bad = ["duplicate:" + n for n in sorted({n for n in names if names.count(n) > 1})]
bad += ["missing-row:" + r for r in sorted(set(required) - set(names))]
bad += [q for e in ledger for q in row_problems(e, runs, tracked)]
good = [e for e in ledger if not row_problems(e, runs, tracked)] # only a row without complaints counts as evidence
solid = {e["property"] for e in good if e["status"] in ("proven", "cover-reached")}
for a, rows in sorted(register.items()):
if rows is None:
if final:
bad.append("deferred-assume:" + a) # a stage may defer a discharge; a final package may not
elif not (rows and all(r in solid for r in rows)):
bad.append("open-assume:" + a)
bad += ["unregistered-assume:%s:%s" % (e.get("property"), a) for e in ledger
for a in e.get("assumes", []) if a not in register]
killed = {m for e in good if e["status"] == "cex" for m in e["kills"]}
bad += ["survivor:" + m for m in sorted(set(mutants) - killed)]
bad += ["unsupported-kill:%s:%s" % (e.get("property"), m) for e in ledger
if e.get("status") in ("proven", "bounded") for m in e.get("kills", []) if m not in killed]
return bad
def mutation_score(ledger, mutants):
assert mutants, "no mutants registered"
killed = {m for e in ledger if e.get("status") == "cex" for m in e.get("kills", [])}
return len(killed & set(mutants)) / len(mutants)
RUNS = {
"ctr-plain-prove": ("prove", 10, "unproven"),
"ctr-plain-bmc": ("bmc", 20, "bounded"),
"fifo-nohelp-prove": ("prove", 12, "unproven"),
"bound-claim-a": ("bmc", 6, "bounded"),
}
REQUIRED = ["counter-full-set", "counter-needs-helper", "fifo-induction-needs-helper"]
MUTANTS = ["ctr-W1"]
REGISTER = {"reset-at-step-0": None} # discharged by the pair rows of stage 2
YOUR_ROWS = [] # fill from your own runs
bad = ledger_ok(YOUR_ROWS, RUNS, REQUIRED, MUTANTS, REGISTER, set(), final=False)
if YOUR_ROWS:
assert bad == [], bad
verdict = "stage 4 induction package consistent"
else:
expected = ["missing-row:" + r for r in REQUIRED] + ["survivor:" + m for m in MUTANTS]
assert sorted(bad) == sorted(expected), bad
verdict = "the empty package is rejected with %d complaints" % len(bad)
# a bounded pass cannot stand in for the proof the helper would give
stand_in = dict(property="counter-full-set", design="mod10_counter", status="proven", bound=20, why="", run="ctr-plain-bmc",
assumes=["reset-at-step-0"], cover="c_wrap step 14", kills=["ctr-W1"], rev=3)
assert "status-not-from-run:counter-full-set" in ledger_ok([stand_in], RUNS, [], [], REGISTER, set(), final=False)
print("PASS: %s; a bounded run is refused as the evidence of a proven row" % verdict)Hint 1: the bounded check passes at every depth, so the design is fine and the argument is not: read the start state of the failing step.
Hint 2: ask whether that start state can be reached from reset, and which values like it satisfy the property.
Hint 3: strengthen with a statement that excludes the whole region of such states and is itself preserved by the transition.
Hint 4: for the last block, read every statement of the module and ask which behaviour of the planted fault each one removes.
When a step fails, print the start state first: whether it is reachable decides everything. When you add a helper, prove it alone before conjoining it, because a false helper poisons the set. Whenever a proof passes with a fault planted, list every statement the model contains and ask which behaviour of the fault each one removes.
A held enable repeats a state forever, so a chain of good states of any length can precede the violation. Bigger windows do not remove bad starts; only a helper does.
Plant a fault the property should catch and rerun: a pass that survives it is not evidence. The causes are in the Solutions topic.