The symptom: a package lands on the reviewer's desk with forty proven rows, three bounded rows and two waivers, and nobody can say why that depth was enough for the counter, or who owns the old waiver. The rows are fine; the package is not, because a package is an argument and this one has no citations. This lesson turns each depth into a cited bound, each assumption into a discharged entry, and each waiver into an owned, dated record.
The cover steps of the six designs, measured in the earlier stages and tabulated below.
The ledger rows you have filed in stages 1 to 3.
The assumption register: the only assumptions the lab's proofs make are the reset at step 0 and the free tracked constants. Every input is free.
A waiver record: id, owner, date raised, expiry, evidence revision. The day numbers in this lesson are illustrative.
Design | Deepest step the claim needs | Smallest depth that sees it | Used for |
|---|---|---|---|
FIFO | 8 (a state: the first reach of the farthest control state; the covers are reached at steps 2 to 5) | 9 | bounded and cover rows |
Bridge | 3 (a cover) | 4 | bounded and cover rows |
Registers | 2 (a cover) | 3 | bounded and cover rows |
Arbiter | 4 (a cover: contention) | 5 | bounded and cover rows |
Pipeline and miter | 4 (a cover: first result) | 5 | bounded and cover rows |
Counter | 14 (a cover: wrap) | 15 | cover rows |
// formal: cover 15 expect reached 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); HELPER=0 removes the helper assertion.
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);
always @(*) if (!init) a_not15: assert (count != 4'd15);
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
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
endmoduleExpected outcome: reached. The counter's covers are first reached at steps 10, 10 and 14, so a run shorter than depth 15 cannot show all of them.
A bound justification for every bounded or cover row: the depth, the cover step it rests on, and the reason in one sentence.
For every proven row: the proof depth and the induction window at which it passed, not a bounded-depth argument.
The assumption register with two entries, each naming the rows that discharge it.
Two waivers, each with owner, dates and revision, checked by the freshness function below.
The staleness drill: bump the revision and list the rows that go stale.
Every bound cites a cover step from the table.
The freshness function accepts your waivers and rejects each of the three defects: expired, ownerless, stale.
A revision bump makes every row stale until it is rerun.
# ---- 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)
# illustrative day numbers: the limit and the dates are made up for this exercise
TODAY, LIMIT, REV_NOW = 200, 90, 3
def fresh(w):
return (TODAY - w["raised"] <= LIMIT and TODAY <= w["expires"] and w["rev"] == REV_NOW and bool(w["owner"]))
WAIVERS = [dict(id="W-demo-1", owner="block-owner", raised=180, expires=260, rev=3),
dict(id="W-demo-2", owner="block-owner", raised=170, expires=260, rev=3)]
assert all(fresh(w) for w in WAIVERS)
assert not fresh(dict(WAIVERS[0], raised=50)), "a waiver raised 150 days ago has aged out"
assert not fresh(dict(WAIVERS[0], expires=190)), "a waiver past its expiry fails"
assert not fresh(dict(WAIVERS[1], owner="")), "a waiver without an owner fails"
assert not fresh(dict(WAIVERS[0], rev=2)), "a waiver on an older revision fails"
RUNS = {"demo-prove": ("prove", 4, "proved")}
ROW = dict(property="demo-row", design="toggle_demo", status="proven", bound=4, why="", run="demo-prove",
assumes=["reset-at-step-0"], cover="c_demo step 2", kills=["demo-W1"], rev=3)
CEX = dict(property="demo-W1@a", design="toggle_demo", status="cex", bound=3, why="", run="demo-cex",
assumes=["reset-at-step-0"], cover="", kills=["demo-W1"], rev=3)
RUNS["demo-cex"] = ("bmc", 3, "counterexample")
world = dict(runs=RUNS, required=["demo-row"], mutants=["demo-W1"], register={"reset-at-step-0": ["demo-row"]}, tracked=set())
assert ledger_ok([ROW, CEX], **world) == []
stale = [dict(r, rev=2) for r in (ROW, CEX)]
stale_bad = ledger_ok(stale, **world)
assert "stale:demo-row" in stale_bad and "stale:demo-W1@a" in stale_bad, "a revision bump marks every row stale"
print("PASS: waivers need an owner, a date inside the limit and the current revision; a bump stales every row")# ---- 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-cover": ("cover", 15, "reached"),
}
REQUIRED = ["counter-covers"]
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, [], REGISTER, set(), final=False)
if YOUR_ROWS:
assert bad == [], bad
print("PASS: stage 4 counter cover package consistent")
else:
assert bad == ["missing-row:counter-covers"], bad
print("PASS: the empty package is rejected: the counter covers are missing")Hint 1: for each bounded or cover row, find the cover that reaches the deepest behaviour the row claims.
Hint 2: a proven row needs no cover-step argument for its depth, only the window at which the induction passed.
Hint 3: for each assumption, search your rows for the ones that show it does not remove the behaviour the proofs need: a proven reset claim, or a cover that reaches the trigger.
Hint 4: a waiver without an owner is refused; assign one before anything else.
Read the package backwards from the waivers: every waiver should point at a behaviour the covers also show, so the waived risk is bounded on both sides. Check each discharge by opening the named row, not by trusting the name. After any change to the source, bump the revision first and watch the package go stale: that failure is the freshness check working.
No: they answer different questions. The induction closes the property at its window; witnessing the wrap behaviour needs depth 15. Both are filed with their own reasons.
Fail: an ownerless waiver is refused. Someone must be accountable for re-checking it at expiry.