When every kind of evidence the protocol needs is present, and every gap has an owner and a reason someone else has checked. A coverage percentage on its own is not closure: 98% of cells hit says nothing about whether the missing 2% are the races. For a coherence controller the evidence comes in five kinds, and each covers something the others cannot.
Evidence | What it shows | What it cannot show |
|---|---|---|
Functional coverage of the protocol table and the race crosses, both orders | The stimulus reached every legal cell and every named race | That the results were right |
Value checking (scoreboard and reference model) with zero failures over long random and stress regressions | Every load and every Data returned the newest value on the runs that happened | Anything about runs that did not happen |
Assertion coverage: each impossible-cell assertion and each protocol assertion has a non-zero antecedent count | The assertions were exercised, not vacuously true | Behaviour outside the assertions |
Formal proofs of SWMR and the data-value invariant on a small model | No reachable state of that configuration violates them, including races no test reached | Larger configurations, unless an argument extends the result |
Reviewed waivers for every remaining hole | Each gap is proven unreachable or consciously accepted, with an owner | Nothing, if the waiver is wrong: hence the review |
The default answer to 'reachable?' is yes. Shifting a cell to 'unreachable' needs the same evidence as any impossible cell: a property that formal proves, which then runs as an assertion in simulation so a later RTL change that makes the cell reachable fails at once instead of quietly reopening the hole.
The protocol table says a replacement of a line in IS^D stalls, following the Primer's convention. Suppose the course controller's victim selection never picks a way with an outstanding miss (an MSHR), so the event never reaches the controller and the cell stays at zero in every regression. That is a claim of unreachability, so it needs a proof, not a comment.
Waiver field | Entry for (IS^D, Evict) |
|---|---|
Cell or bin | (IS^D, Evict), also (IM^D, Evict) and (SM^D, Evict) for the same reason |
Kind | Unreachable in this design |
Argument | Victim selection masks every way with a valid MSHR, so a line in a transient miss state is never chosen |
Evidence | Formal property 'victim way never has a valid MSHR', proven; the same property runs as an assertion in every simulation |
Effect on the model | Cells reclassified from stall to impossible in this configuration; the stall action remains in the specification |
Owner and approver | Controller design lead owns it; verification lead, a different person, approves |
Revisit when | Victim selection or MSHR allocation changes |
Now a waiver that must be rejected: "(SI^A, Inv) never hit; low risk, rare in practice". The cell is reachable on the course model: a PutS crossing an Inv, as Clean Eviction: Silent or Notified describes. Rarity is the reason it needs a test, not a reason to waive it. The right ending is the stress recipe from Directed Race Stress: eviction pressure on shared lines while another core upgrades.
Item | Done when |
|---|---|
Protocol table | Every state x event cell classified as action, stall or impossible, reviewed against the specification, machine-readable |
State x event coverage | Every legal cell hit, or covered by a reviewed waiver |
Race crosses | Every named race cross hit in each arrival order, on runs the value checker passed |
Impossible cells | Each has an assertion that never fired, with a non-zero antecedent count |
Assertion coverage | No vacuous assertion: every antecedent exercised in simulation or covered in formal |
Formal | SWMR and the data-value invariant proven on the stated small model; the configuration and any extension argument written down |
Random and stress regression | Long seeded regressions across all stress profiles with zero value-checker failures; failing seeds reproducible |
Waivers | Each has kind, argument or proof, owner, a different approver and a revisit trigger; none waives a reachable race in a shipped configuration on the grounds that it is rare. Out-of-scope waivers name the disabled feature or configuration |
Change control | Any protocol-table change regenerates coverage and assertions and reopens the affected items |
The block below is that checklist as a gate: it returns every blocking reason, and each single defect (a hole with no waiver, a self-approved waiver, an unproven unreachability claim, a justified waiver with no reason, a race cross hit in only one order, a vacuous assertion, one value failure, an unproven SWMR) must block sign-off with a reason that names it.
def blockers(r):
"""Return every reason the coherence block cannot be signed off (empty list = closed)."""
out, waived = [], {w["cell"]: w for w in r["waivers"]}
for cell in r["legal"]:
if r["hits"].get(cell, 0) == 0:
w = waived.get(cell)
if w is None: out.append("hole %s/%s with no waiver" % cell)
elif not w.get("owner") or w.get("approver") in (None, w.get("owner")):
out.append("waiver %s/%s needs an owner and a different approver" % cell)
elif w["kind"] == "unreachable" and r["formal"].get(w.get("proof")) != "proven":
out.append("waiver %s/%s claims unreachable without a proof" % cell)
elif w["kind"] == "justified" and not (w.get("reason") and w.get("disabled")):
out.append("waiver %s/%s has no justification naming the disabled feature" % cell)
for race, orders in r["races"].items():
for order in ("put first", "request first"):
if orders.get(order, 0) == 0: out.append("race %s not hit in order '%s'" % (race, order))
for name, a in r["assertions"].items():
if a["fails"]: out.append("assertion %s failed" % name)
if a["antecedent"] == 0: out.append("assertion %s is vacuous" % name)
for prop in ("swmr", "data_value"):
if r["formal"].get(prop) != "proven": out.append("formal %s not proven" % prop)
if r["regression"]["value_fails"] or r["regression"]["seeds"] < 1000:
out.append("random regression not clean over enough seeds")
return out
good = {
"legal": [("SM^D", "Inv"), ("MI^A", "Fwd-GetM"), ("IS^D", "Evict")],
"hits": {("SM^D", "Inv"): 412, ("MI^A", "Fwd-GetM"): 37},
"waivers": [{"cell": ("IS^D", "Evict"), "kind": "unreachable", "proof": "victim_skips_mshr",
"owner": "controller lead", "approver": "verification lead"}],
"races": {"PutM crossing Fwd-GetS": {"put first": 21, "request first": 9}},
"assertions": {"inv_only_to_sharer_states": {"antecedent": 9120, "fails": 0},
"fwd_only_to_exclusive_states": {"antecedent": 3310, "fails": 0}},
"formal": {"swmr": "proven", "data_value": "proven", "victim_skips_mshr": "proven"},
"regression": {"seeds": 5000, "value_fails": 0},
}
assert blockers(good) == []
# failing cases: each defect alone must block sign-off, with a reason naming it
def broken(**change):
r = {k: (dict(v) if isinstance(v, dict) else list(v)) for k, v in good.items()}
r.update(change); return blockers(r)
assert broken(waivers=[]) == ["hole IS^D/Evict with no waiver"]
assert broken(waivers=[dict(good["waivers"][0], approver="controller lead")])[0].startswith("waiver IS^D/Evict needs")
assert broken(formal=dict(good["formal"], victim_skips_mshr="bounded 20"))[0].endswith("without a proof")
vac = dict(good["assertions"], fwd_only_to_exclusive_states={"antecedent": 0, "fails": 0})
assert broken(assertions=vac) == ["assertion fwd_only_to_exclusive_states is vacuous"]
assert broken(regression={"seeds": 5000, "value_fails": 1}) == ["random regression not clean over enough seeds"]
assert broken(formal=dict(good["formal"], swmr="bounded 20")) == ["formal swmr not proven"]
just = {"cell": ("IS^D", "Evict"), "kind": "justified", "owner": "controller lead", "approver": "verification lead",
"disabled": "prefetch-on-miss build option, off in every shipped configuration"}
assert broken(waivers=[just]) == ["waiver IS^D/Evict has no justification naming the disabled feature"]
assert broken(waivers=[dict(just, reason="needs prefetch-on-miss")]) == [] # the complete waiver passes
one_order = {"PutM crossing Fwd-GetS": {"put first": 21, "request first": 0}}
assert broken(races=one_order) == ["race PutM crossing Fwd-GetS not hit in order 'request first'"]
print("PASS: the closure gate accepts complete evidence and names each missing item")The numbers in the report are illustrative, and the seed threshold of 1,000 is a placeholder for a team's own rule. The gate treats a bounded formal result as not proven. A team may accept a bounded proof when the bound is shown to cover every reachable state of the small model; that argument then belongs in the formal sign-off, as the Bounded Proofs lesson of First Principles of Verification Strategy discusses for bounds and the reachability diameter. One value failure blocks closure however rare: a coherence violation is a correctness failure, not a rate.
It is strong evidence for that configuration, including races no simulation reached, but not by itself a proof for eight caches. The sign-off must state the configuration and the argument for extending it (for example that caches are symmetric and the protocol treats addresses independently, or a separate parameterised proof), and the simulation evidence on the full configuration still has to be clean. If no extension argument exists, record the gap explicitly.