Sign-off is a statement that the coherence protocol in this exact RTL is correct, makes progress, meets its performance targets, and that every known issue has a verified answer. Each claim needs evidence that someone other than its author has checked. Block-level verification closure is defined in Closure Evidence; tape-out sign-off adds the program view: design reviews, performance, known issues and the match between evidence and the final RTL.
Item | Evidence | Done when (thresholds illustrative) | Signs |
|---|---|---|---|
Value checking | Scoreboard and reference model on random and stress regressions | Zero value failures over the team's seed count (for example 20,000 seeds across all stress profiles) | Verification lead |
Coverage closure | State x event table, race crosses in both orders, assertion antecedents | Every legal cell and race bin hit, or a reviewed waiver with owner and different approver | Verification lead |
Formal safety | SWMR and the data-value invariant on a stated small model | Proven, configuration and any extension argument written down | Formal lead |
Progress | Watchdog-clean regressions, stuck-state search on the small model | Zero hangs; no reachable stuck state in the model | Formal lead and verification lead |
Litmus suites | Forbidden outcomes of the target memory model (SB and MP and beyond) in simulation or emulation | No forbidden outcome observed; allowed outcomes seen where the harness can produce them | Architecture lead |
Design reviews | Protocol and controller reviews (checklist) | Every action item closed or deferred with owner and reason | Coherence architect |
Performance | Miss latency, bandwidth under contention, directory occupancy on named workloads | Targets met in RTL simulation or emulation, with the workload and configuration stated | Performance lead |
Known issues | List of open bugs, each with workaround | Each chicken bit regressed with the bit set, its cost measured, its erratum text drafted | Design lead |
Change control | RTL tag of each piece of evidence | All evidence on the frozen tag, or a written argument that no dependency changed | Program lead, last |
Each signer owns a claim they can defend in a review, and the program lead signs last, only when every other line is signed. A signature is not a vote: one unsigned line blocks tape-out, however good the rest looks.
Take the course model with the three-hop route of Three-Hop Versus Four-Hop and the Put-handler fix of Late Bug Decisions. Specific lines on the checklist for this feature:
Item | Evidence for direct transfer |
|---|---|
Coverage | Cross (MI^A, Fwd-GetM) x route x PutM before or after the forwarded Data, all four cells hit |
Value checking | Regression in both chicken-bit settings, zero value failures; the race's directed test included |
Formal | Small model includes both routes and a delayed PutM; SWMR and the data-value invariant proven |
Assertion | 'A Put from a non-holder never changes the directory or memory', non-zero antecedent count |
Performance | Dirty-miss latency measured: three legs with the bit clear, four with it set |
Known issues | Bit defaults to four-hop for first silicon; firmware procedure to clear it documented |
The Put-handler fix landed in the last RTL tag. A proof run on the tag before it says nothing about the handler as shipped. The strict rule is to rerun everything on the frozen tag. A program that carries evidence forward must show that no file the evidence depends on changed since it was produced. The gate below makes that argument mechanical; the naive gate only reads the results.
TAGS = ["r40", "r41", "r42"] # r42 is the frozen tag
CHANGED = {"r41": {"noc/router"}, "r42": {"home/put_handler"}} # files changed in each tag
EVIDENCE = { # name: (tag it ran on, result, files it depends on)
"value regression": ("r42", "clean", {"home/put_handler", "home/dir", "cache/ctrl"}),
"coverage closure": ("r42", "closed", {"home/put_handler", "home/dir", "cache/ctrl"}),
"formal SWMR": ("r41", "proven", {"home/put_handler", "home/dir"}),
"litmus suite": ("r42", "clean", {"cache/ctrl", "home/dir"}),
"dirty-miss latency": ("r41", "met", {"noc/router", "home/dir"}),
}
GOOD = {"clean", "closed", "proven", "met"}
def changed_after(tag, frozen):
later = TAGS[TAGS.index(tag) + 1: TAGS.index(frozen) + 1]
return set().union(*(CHANGED.get(t, set()) for t in later))
def blockers(evidence, frozen="r42"):
out = []
for name, (tag, result, deps) in evidence.items():
if result not in GOOD:
out.append(f"{name}: result {result}")
elif changed_after(tag, frozen) & deps:
out.append(f"{name}: run on {tag}, stale after {sorted(changed_after(tag, frozen) & deps)}")
return out
def naive_blockers(evidence, frozen="r42"): # broken: ignores which tag the evidence ran on
return [n for n, (_, result, _) in evidence.items() if result not in GOOD]
b = blockers(EVIDENCE)
assert b == ["formal SWMR: run on r41, stale after ['home/put_handler']"], b
assert naive_blockers(EVIDENCE) == [] # the naive gate would sign off on a stale proof
# carrying forward is allowed when no dependency changed: the latency run on r41 is not blocked
assert not any(x.startswith("dirty-miss latency") for x in b)
# general claim: for every tag t and every dependency set, the gate flags clean evidence exactly
# when some file changed in a tag after t, up to and including the frozen tag, is a dependency
import itertools
FILES = sorted(set().union(*CHANGED.values()) | {"home/dir", "cache/ctrl"})
for t in TAGS:
window = {f for u, fs in CHANGED.items() if TAGS.index(t) < TAGS.index(u) <= TAGS.index("r42") for f in fs}
for n in range(len(FILES) + 1):
for deps in map(set, itertools.combinations(FILES, n)):
assert bool(blockers({"e": (t, "clean", deps)})) == bool(window & deps), (t, deps)
# rerunning the proof on r42 clears the last blocker
fixed = dict(EVIDENCE, **{"formal SWMR": ("r42", "proven", {"home/put_handler", "home/dir"})})
assert blockers(fixed) == []
assert blockers(dict(fixed, **{"litmus suite": ("r42", "1 forbidden", {"cache/ctrl"})})) == ["litmus suite: result 1 forbidden"]
print("PASS: the gate blocks a proof made stale by the fix and accepts evidence whose dependencies did not change")The dependency sets are the weak point: a missed dependency lets stale evidence through. Teams that cannot keep them accurate should use the strict rule, and teams that use them should have them reviewed like a waiver.
Only those whose evidence does not depend on the snoop filter, and only with a written dependency argument. Value regression, coverage, formal results that model the filter, litmus runs and any performance numbers that involve snoops must be rerun on the new tag. The program lead's signature is void until the affected lines are signed again.