A cache controller is specified by a table: one row per state (stable and transient), one column per event, and in each cell either an action, a stall, or nothing because the event cannot happen there. That table is the coverage model. Writing coverage from anything else (the RTL's case statement, a list of tests someone thought of) misses exactly the cells nobody thought of.
Rule: cover the full cross of states x events, and classify every cell before running anything. A legal cell (action or stall) must be hit. An impossible cell must never be hit, and that is checked by an assertion, not by noting that coverage stayed at zero. A cell left unclassified is a specification gap.
States are the course's MSI states with transients (acks collected at H, so IS^D, IM^D, SM^D; eviction states MI^A, SI^A, II^A from the eviction topic). Events are the three core events (load, store, evict, meaning the replacement logic picks X as a victim) and the five incoming messages. The model is the course model with notified evictions and the grant-delivery rule. "act" means a defined action, "stall" means the event waits, "-" means impossible.
State | Load | Store | Evict | Inv | Fwd-GetS | Fwd-GetM | Data | Put-Ack |
|---|---|---|---|---|---|---|---|---|
I | act: GetS, IS^D | act: GetM, IM^D | - | - | - | - | - | - |
S | act: hit | act: GetM, SM^D | act: PutS, SI^A | act: Inv-Ack, I | - | - | - | - |
M | act: hit | act: hit | act: PutM, MI^A | - | act: Data to H, S | act: Data to H, I | - | - |
IS^D | stall | stall | stall | - | - | - | act: load, S | - |
IM^D | stall | stall | stall | - | - | - | act: store, M | - |
SM^D | act: hit | stall | stall | act: Inv-Ack, IM^D | - | - | act: store, M | - |
MI^A | stall | stall | stall | - | act: Data from WB, SI^A | act: Data from WB, II^A | - | act: I |
SI^A | stall | stall | stall | act: Inv-Ack, II^A | - | - | - | act: I |
II^A | stall | stall | stall | - | - | - | - | act: I |
Nine states by eight events give 72 cells: 39 legal (22 actions, 17 stalls) and 33 impossible. Each impossible cell has a reason that can be written as a property: H sends Inv only to recorded sharers (S, SM^D, SI^A); H forwards only to its recorded exclusive holder (M, or MI^A while the PutM is in flight); Data arrives only for an outstanding miss; Put-Ack only for an outstanding Put; an invalid line is never a victim.
The grant-delivery rule is why five cells are impossible here: (IS^D, Inv), (IM^D, Fwd-GetM), (SM^D, Fwd-GetM), (IM^D, Fwd-GetS) and (SM^D, Fwd-GetS). Drop it, as Racing Requests at the Home does, and all five become reachable: H can send an Inv to a reader whose S grant is still in flight, and it can forward the next GetM or the next GetS to a writer whose M grant is still in flight. The controller then needs IS^D_I and a stalled Fwd (either kind) in IM^D and SM^D, and the matrix gains a row. The coverage model must be regenerated whenever the protocol table changes, and the assertion set changes with it. This is the strongest argument for generating both from one machine-readable table.
Take the trace in Simultaneous Upgrades: C0 and C1 both hold S / 0, H records S{C0,C1}, memory = 0. Both store and enter SM^D. H picks C0's GetM A and sends Inv to C1 at step 3. That delivery samples the cell (SM^D, Inv) at C1, whose action is Inv-Ack and a move to IM^D. Step 5 (Data at C0 in SM^D) samples (SM^D, Data). No other single trace in the course hits (SM^D, Inv), because it needs two sharers storing at nearly the same time.
The block below encodes the table, runs a seeded random model of C0, C1 and H that follows it (non-FIFO delivery, value checks on every load and Data), and reports unhit legal cells. Two broken variants must fail: a run with no evictions leaves holes, and an H that drops the grant-delivery rule enters an impossible cell.
Where the model simplifies the course protocol. Deviation, as in Small Models and Parameters: the M grant always carries memory's value, including the permission-only grant of an upgrade (memory is current while the line has sharers in MSI). H also records the new holder or sharer when it sends the grant rather than at delivery; it starts nothing else for X until the grant is delivered, so the cells reached are the same.
import random
EV = ["Load", "Store", "Evict", "Inv", "Fwd-GetS", "Fwd-GetM", "Data", "Put-Ack"]
# Protocol table of the C0/C1 controller: a = action, s = stall, - = impossible
TABLE = {"I": "aa------", "S": "aaaa----", "M": "aaa-aa--",
"IS^D": "sss---a-", "IM^D": "sss---a-", "SM^D": "assa--a-",
"MI^A": "sss-aa-a", "SI^A": "sssa---a", "II^A": "sss----a"}
LEGAL = {(s, e) for s, row in TABLE.items() for e, c in zip(EV, row) if c != "-"}
assert len(LEGAL) == 39 and len(TABLE) * len(EV) - len(LEGAL) == 33
def run(seed, steps, evict=True, wait_grant=True):
rng, st, val, net, hits, q = random.Random(seed), {0: "I", 1: "I"}, {0: None, 1: None}, [], set(), []
g = {"mem": 0, "latest": 0, "busy": None, "acks": 0, "X": None, "S": set()}
def hit(c, e): # record the cell; True means the controller stalls
cell = (st[c], e); hits.add(cell)
assert cell in LEGAL, "impossible cell hit: %s %s" % cell
return TABLE[st[c]][EV.index(e)] == "s"
def grant(c, perm, v):
net.append((c, "Data", "H", (perm, v)))
g["S"], g["X"] = (g["S"] | {c}, None) if perm == "S" else (set(), c)
g["busy"] = ("deliv", c) if wait_grant else None
def start():
while g["busy"] is None and q:
kind, c, p = q.pop(0)
if kind in ("PutS", "PutM"):
if kind == "PutM" and g["X"] == c: g["mem"], g["X"] = p, None
g["S"].discard(c); net.append((c, "Put-Ack", "H", None))
elif g["X"] is not None:
g["busy"] = ("fwd", kind, c)
net.append((g["X"], "Fwd-GetS" if kind == "GetS" else "Fwd-GetM", "H", None))
elif kind == "GetS": grant(c, "S", g["mem"])
elif g["S"] - {c}:
g["busy"], g["acks"] = ("ack", c), len(g["S"] - {c})
for o in g["S"] - {c}: net.append((o, "Inv", "H", None))
else: grant(c, "M", g["mem"])
def home(kind, src, p):
b = g["busy"]
if kind == "Inv-Ack":
g["S"].discard(src); g["acks"] -= 1
if g["acks"] == 0: grant(b[1], "M", g["mem"])
elif kind == "Data": # answer to a forward
v, still_holder = p
if b[1] == "GetS": # MSI: H writes memory, the old holder stays only if it kept S
g["mem"], g["X"], g["S"] = v, None, ({src} if still_holder else set())
grant(b[2], "S", v)
else: grant(b[2], "M", v)
else: q.append((kind, src, p))
start()
def cache_msg(c, kind, p):
s = st[c]
if hit(c, kind): return False
if kind == "Data":
st[c], val[c] = ("S" if p[0] == "S" else "M"), p[1]
assert val[c] == g["latest"], "stale Data"
if st[c] == "M": g["latest"] += 1; val[c] = g["latest"] # the stalled store
if g["busy"] == ("deliv", c): g["busy"] = None; start()
elif kind == "Inv":
st[c] = {"S": "I", "SM^D": "IM^D", "SI^A": "II^A"}[s]; net.append(("H", "Inv-Ack", c, None))
elif kind in ("Fwd-GetS", "Fwd-GetM"):
keep = kind == "Fwd-GetS" and s == "M"
net.append(("H", "Data", c, (val[c], keep)))
st[c] = {("M", "Fwd-GetS"): "S", ("M", "Fwd-GetM"): "I",
("MI^A", "Fwd-GetS"): "SI^A", ("MI^A", "Fwd-GetM"): "II^A"}[(s, kind)]
else: st[c] = "I" # Put-Ack
return True
def core(c, op):
s = st[c]
if (s == "I" and op == "Evict") or hit(c, op): return
if op == "Load" and s == "I": st[c] = "IS^D"; net.append(("H", "GetS", c, None))
elif op == "Load": assert val[c] == g["latest"], "stale load"
elif op == "Store" and s == "M": g["latest"] += 1; val[c] = g["latest"]
elif op == "Store": st[c] = "IM^D" if s == "I" else "SM^D"; net.append(("H", "GetM", c, None))
else:
st[c] = "SI^A" if s == "S" else "MI^A"
net.append(("H", "PutS" if s == "S" else "PutM", c, val[c]))
for _ in range(steps):
if net and rng.random() < 0.6:
i = rng.randrange(len(net)); dst, kind, src, p = net[i]
if dst == "H": net.pop(i); home(kind, src, p)
elif cache_msg(dst, kind, p): net.pop(i)
else: core(rng.randrange(2), rng.choice(["Load", "Store", "Evict"][:3 if evict else 2]))
return LEGAL - hits # the coverage report: unhit legal cells
assert run(seed=7, steps=5000) == set() # every legal cell hit, no impossible one
holes = run(seed=7, steps=5000, evict=False) # failing case 1: no evictions
assert len(holes) == 20 and ("MI^A", "Fwd-GetM") in holes and ("SI^A", "Inv") in holes
raised = "" # failing case 2: H drops the grant-delivery wait
try: run(seed=7, steps=5000, wait_grant=False)
except AssertionError as err: raised = str(err)
assert raised == "impossible cell hit: SM^D Fwd-GetM", raised
print("PASS: 39 legal cells hit, holes reported without evictions, impossible cell flagged")With evictions switched off, the report lists 20 holes: every MI^A, SI^A and II^A cell plus the Evict column. That is the useful shape of a coverage report: it names cells, not a percentage. With the grant-delivery wait removed, seed 7 first fails on (SM^D, Fwd-GetM): H granted M to a cache and forwarded the next writer's request to it before its Data had arrived. The model is two caches and one line; it shows the method, not the size of a real regression.
In a testbench the matrix becomes a cross with the impossible cells as illegal bins, and each impossible group also becomes an assertion. Illegal bins report only while coverage is sampled; the assertion fires in every run and is what formal proves.
// snippet
covergroup cg_ctrl @(posedge clk iff ev_valid);
cp_st: coverpoint st { bins s[] = {I, S, M, IS_D, IM_D, SM_D, MI_A, SI_A, II_A}; }
cp_ev: coverpoint ev { bins e[] = {LOAD, STORE, EVICT, INV, FWD_GETS, FWD_GETM, DATA, PUT_ACK}; }
x_st_ev: cross cp_st, cp_ev {
illegal_bins inv_to_non_sharer = binsof(cp_st) intersect {I, M, IS_D, IM_D, MI_A, II_A} && binsof(cp_ev) intersect {INV};
illegal_bins fwd_to_non_holder = binsof(cp_st) intersect {I, S, IS_D, IM_D, SM_D, SI_A, II_A} && binsof(cp_ev) intersect {FWD_GETS, FWD_GETM};
illegal_bins data_unrequested = binsof(cp_st) intersect {I, S, M, MI_A, SI_A, II_A} && binsof(cp_ev) intersect {DATA};
illegal_bins ack_unrequested = binsof(cp_st) intersect {I, S, M, IS_D, IM_D, SM_D} && binsof(cp_ev) intersect {PUT_ACK};
illegal_bins evict_invalid = binsof(cp_st) intersect {I} && binsof(cp_ev) intersect {EVICT};
}
endgroup
a_inv_to_sharer: assert property (@(posedge clk) disable iff (!rst_n)
ev_valid && ev == INV |-> st inside {S, SM_D, SI_A});The five illegal groups hold 6 + 14 + 6 + 6 + 1 = 33 cells, matching the table.
H forwards only to the cache it records as the exclusive holder. In MI^A, C0 was the M holder and its PutM may still be in flight, so H can still record exclusive(C0) and forward to it. A cache reaches SI^A either from S (never an exclusive holder) or from MI^A by answering a Fwd-GetS, after which H records only the reader as a sharer. In neither case does H record C0 as exclusive, so no Fwd can be sent to it.