Plans fail at signoff, not at writing: a row without an owner is never run, a row without a trigger cover passes vacuously, a row without recorded evidence is rerun from scratch by the reviewer. This lesson writes the whole plan for two blocks small enough to hold in one view, so the pattern transfers to larger ones.
Job of this lesson: produce a complete, checkable plan and run the completeness check on it.
A complete row has seven fields: requirement, method, property, trigger cover, owner, evidence and exit criterion. Evidence is one of proven (with the run that proved it), bounded to a stated depth with a justification, or counterexample with a linked fix. A bounded run is never filed as proven. The table below is the full plan for the two blocks, seven rows each with its own exit criterion; every run named in it is a prove run from the previous lessons, so each row is proven for the model and the reset assumption stated there:
Row | Requirement | Properties | Trigger cover | Evidence | Exit criterion |
|---|---|---|---|---|---|
CSR-1 | ID reads 0xA5 |
|
| Proven, | Proof passes; |
CSR-2 | Write-1-to-clear clears unless hardware sets |
|
| Proven, | Proof passes; |
CSR-3 | Reset values |
|
| Proven, | Proof passes; |
CSR-4 | No cross-register disturbance |
|
| Proven, | Proof passes; |
HS-1 | Nothing lost or duplicated |
|
| Proven, | Proof passes; |
HS-2 | Stall holds valid and data |
|
| Proven, | Proof passes; |
HS-3 | Ready has no combinational path |
|
| Proven, | Proof passes; |
The script encodes those seven rows as data and checks them against the properties and covers of each block. Every property and cover must exist in its block, every row needs an owner and its own exit criterion, and the evidence must be honest: a proven row must cite a prove run, and a bounded row must justify its depth by reset plus trigger plus latency plus one (the numbers in the bounded test are illustrative). The second half plants four broken rows, one for each rule, and shows each one rejected:
ASSERTS = {
"csr_block": {"a_id_const", "a_status_hi", "a_rst_ctrl", "a_rst_status", "a_rst_data", "a_ctrl_rw",
"a_data_rw", "a_w1c_done", "a_w1c_err", "a_w1c_zero", "a_hw_set",
"a_isolate_ctrl", "a_isolate_data"},
"hs_bridge": {"a_skid_needs_out", "a_conserve", "a_valid_hold", "a_data_hold", "a_no_ready_comb", "a_data"},
}
COVERS = {
"csr_block": {"c_w1c_clear", "c_both_bits", "c_id_write", "c_reset_released", "c_ctrl_write"},
"hs_bridge": {"c_stall", "c_skid_used", "c_backpress_full", "c_flow", "c_reset_released"},
}
P4 = {"kind": "proven", "run": "prove 4"}
def row(rid, block, props, cover, exit_):
return {"id": rid, "block": block, "props": props, "cover": cover, "owner": "block owner",
"evidence": P4, "exit": exit_}
plan = [
row("CSR-1", "csr_block", ["a_id_const"], "c_id_write", "proof passes; c_id_write reached at step 1"),
row("CSR-2", "csr_block", ["a_w1c_done", "a_w1c_err", "a_w1c_zero", "a_hw_set"], "c_w1c_clear", "proof passes; c_w1c_clear reached at step 2"),
row("CSR-3", "csr_block", ["a_rst_ctrl", "a_rst_status", "a_rst_data"], "c_reset_released", "proof passes; c_reset_released reached at step 1"),
row("CSR-4", "csr_block", ["a_isolate_ctrl", "a_isolate_data"], "c_ctrl_write", "proof passes; c_ctrl_write reached at step 1"),
row("HS-1", "hs_bridge", ["a_conserve", "a_skid_needs_out"], "c_skid_used", "proof passes; c_skid_used reached at step 3"),
row("HS-2", "hs_bridge", ["a_valid_hold", "a_data_hold"], "c_stall", "proof passes; c_stall reached at step 2"),
row("HS-3", "hs_bridge", ["a_no_ready_comb"], "c_backpress_full", "proof passes; c_backpress_full reached at step 3"),
]
def evidence_problem(ev):
if ev["kind"] == "proven":
return None if ev["run"].startswith("prove ") else "filed as proven but the run is not a proof"
if ev["kind"] == "bounded":
needed = ev["reset"] + ev["trigger"] + ev["latency"] + 1
depth = int(ev["run"].split()[1])
return None if depth >= needed else "bounded depth below reset + trigger + latency + 1"
return "evidence not recorded"
def check(rows):
problems = []
for r in rows:
for p in r["props"]:
if p not in ASSERTS[r["block"]]:
problems.append(r["id"] + ": property " + p + " not in the block")
if not r["cover"]:
problems.append(r["id"] + ": no trigger cover")
elif r["cover"] not in COVERS[r["block"]]:
problems.append(r["id"] + ": cover not in the block")
if not r["owner"]:
problems.append(r["id"] + ": no owner")
e = evidence_problem(r["evidence"])
if e:
problems.append(r["id"] + ": " + e)
exits = [r["exit"] for r in rows]
if len(set(exits)) != len(exits) or not all(exits):
problems.append("exit criteria are missing or repeated")
return problems
assert len(plan) == 7
assert check(plan) == []
def broken(index, **changes):
rows = [dict(r) for r in plan]
rows[index].update(changes)
return check(rows)
assert any("no trigger cover" in p for p in broken(0, cover=""))
assert any("not in the block" in p for p in broken(1, props=["a_w1c_gone"]))
assert any("cover not in the block" in p for p in broken(2, cover="c_reset_done"))
assert any("exit criteria" in p for p in broken(3, exit=plan[2]["exit"]))
assert any("exit criteria" in p for p in broken(3, exit=""))
assert any("not a proof" in p for p in broken(4, evidence={"kind": "proven", "run": "bmc 4"}))
short = {"kind": "bounded", "run": "bmc 4", "reset": 1, "trigger": 1, "latency": 3}
assert any("below reset" in p for p in broken(5, evidence=short))
assert broken(5, evidence=dict(short, run="bmc 8")) == []
print("PASS: the seven-row plan is accepted; each broken row is rejected for its own reason")Every requirement maps to exactly one row, and every row maps to one owner.
Formal rows carry a trigger cover each; simulation rows carry their traffic instead.
Bounded results name their depth and their justification; none is filed as proven.
Rerun the checker after every plan edit: rows rot as properties are renamed. Cross-check the evidence column against the actual run ledger before signoff; a row whose proof was rerun on newer RTL without updating the ledger is stale, and the regression topic says how to keep it fresh.
Reject: file it as inconclusive until a justification exists, such as depth beyond reset plus trigger plus worst-case latency plus one, a diameter argument, or an inductive proof.