A formal proof says: on every trace the environment assumptions allow, the assertions hold. Both halves matter. Assumptions describe what the rest of the system may do: the caches, the network, the cores. Too few, and the tool reports impossible inputs as bugs. Too many, and the proof covers a smaller world than the real one. A proof under a wrong assumption is a proof about a different system.
Assumption on the environment | Why it is legal | What it must not become |
|---|---|---|
A cache sends at most one request for X at a time (one MSHR per line) | The real cache controller guarantees it | 'No two caches request X at the same time' |
GetM comes only from I or S, PutM only from M | Legal message sequences of the protocol | 'GetM never arrives while a sharer exists' |
An Inv-Ack follows only an Inv to that cache | Responses answer requests | 'The Inv-Ack arrives within 2 cycles' |
Finite outstanding requests: at most k in the network | Real buffers are finite, and it keeps the model finite | A bound smaller than any real race needs |
Messages are eventually delivered (A1) | Needed for liveness only | 'Delivered within N cycles' in a safety proof, which removes long-delay interleavings |
The right-hand column is the danger: each entry is a plausible simplification that removes exactly the interleavings in which coherence bugs live. Assumptions on the environment should ideally be proved as assertions on the real neighbouring block (assume-guarantee): the cache's 'one request per line' assumed at H is asserted at the cache.
Use the early-grant bug that Small Models and Parameters finds: H sends M permission at the same time as the Inv, instead of after the Inv-Ack. A formal engineer, tired of counterexamples that start with a shared line, adds an assumption:
// bad-example
// Over-constrained: "a GetM never arrives while another cache holds S".
asm_no_shared_getm: assume property (@(posedge clk) disable iff (!rst_n)
getm_valid |-> (sharers & ~(1 << getm_src)) == '0);Under it, SWMR proves. But the bug needs exactly that situation: C0 = S / 0, C1 sends GetM. The assumption deleted every trace in which an Inv is ever sent, so the Inv path, the ack counter and the early grant are never exercised. Any assertion about them is now vacuous: its antecedent (an Inv is in flight, an ack is pending) is never true, so 'antecedent implies consequent' holds trivially.
A cover property asks the tool for a trace in which a condition happens. If the cover is unreachable, every assertion whose antecedent depends on it is vacuous. Write covers for the scenarios the proof is meant to include, before trusting the proof:
// snippet
c_getm_with_sharer: cover property (@(posedge clk) disable iff (!rst_n)
getm_valid && (sharers & ~(1 << getm_src)) != '0);
c_inv_sent: cover property (@(posedge clk) disable iff (!rst_n) inv_valid);
c_ack_counts: cover property (@(posedge clk) disable iff (!rst_n)
ack_pending ##1 !ack_pending);Many tools also report vacuity per assertion and produce a witness trace: a trace in which the antecedent fires and the consequent is checked. Read at least one witness for each important assertion; it is the evidence that the property was exercised. The program below repeats the worked case on an atomic sketch of the course model: with the assumption, SWMR holds and the 'an Inv is sent' cover is unreachable; without it the bug appears; the correct design passes with the cover reached.
# Atomic sketch of the course model: C0, C1 in I, S or M, Inv messages in flight,
# and H's grant rule. Fwd-GetS and Fwd-GetM are collapsed into one step.
def moves(s, early_grant, over_constrained):
st, inv, want = s
for i in (0, 1):
j = 1 - i
if st[i] == "I" and want is None and not inv: # load miss
new = list(st); new[i] = "S"
new[j] = "S" if st[j] == "M" else st[j]
yield (tuple(new), inv, None)
if st[i] != "M" and want is None and not inv: # store needing M
if over_constrained and st[j] == "S": # ASSUMPTION
continue
new = list(st)
sharers = frozenset({j}) if st[j] == "S" else frozenset()
new[j] = "I" if st[j] == "M" else st[j]
if early_grant or not sharers:
new[i] = "M" # grant now
yield (tuple(new), sharers, None)
else:
yield (tuple(new), sharers, i) # wait for Inv-Ack
for j in inv: # Inv delivered
new = list(st); new[j] = "I"
rest = inv - {j}
if want is not None and not rest:
new[want] = "M" # all acks: grant
yield (tuple(new), rest, None if not rest else want)
def explore(early_grant, over_constrained):
init = (("I", "I"), frozenset(), None)
seen, todo = {init}, [init]
while todo:
for t in moves(todo.pop(), early_grant, over_constrained):
if t not in seen:
seen.add(t); todo.append(t)
swmr = all("M" not in st or sorted(st) == ["I", "M"] for st, _, _ in seen)
cover_inv = any(inv for _, inv, _ in seen) # witness: an Inv is ever sent
return swmr, cover_inv
assert explore(early_grant=True, over_constrained=True) == (True, False) # "proof" passes, cover unreachable
assert explore(early_grant=True, over_constrained=False) == (False, True) # bug found once assumption removed
assert explore(early_grant=False, over_constrained=False) == (True, True) # correct design, non-vacuous
print("PASS: over-constrained assumption hides the early-grant bug, the Inv cover exposes it")The proof never saw an upgrade with a sharer, so it says nothing about the Inv and ack path where early-grant bugs live. Look for the assumption (or a reset or tie-off) that blocks it, remove or weaken it, rerun the cover until it is reached, then rerun the proof.