In the Python model every check reads the whole system at once. A testbench cannot: it sees the design through monitors on interfaces, each event arrives with some delay, and the internal state of a cache is visible only through a probe. The architecture below keeps the same checks and assigns each to the place that can observe what it needs. The general structure of a scoreboard is taught in Scoreboards; this lesson is the coherence version.
Check | Observes | Rule | Catches (from the Python bugs) |
|---|---|---|---|
Protocol checker, one per interface | Every message on a cache to H link and the receiver's state | Message legal in that state, ids match a pending request, no duplicate or missing response | An Inv at a cache in I, a late Inv-Ack counted twice |
Permission tracker | Grants delivered, Inv and Fwd processed, or state probes | At most one M per line, and no S beside it | Bugs a and b at the moment the grant lands |
Write-order tracker | Stores from the L1 port monitors, with the writer and a unique value, ordered by a white-box store perform hook or by H's M grant order | Per address, one list of writes in serialization order | The reference every value check needs |
Value checker | Every load completion at an L1 load/store port, below the store buffer, with its issue time | The returned value is allowed by the write order and by what this core has already seen | Bug c, the stale data-select, a lost writeback |
End-of-test checks | Everything, after stimulus stops and the system drains | No messages in flight, no MSHR or pending entry left, no credit missing, then every dirty line flushed and memory equal to the newest write for every address touched | Hangs, leaked entries, data lost on eviction |
Two observations decide the hard parts. Store perform order: the tracker needs the order in which stores joined each location's write order. A white-box hook at the cache (the store wrote a line in M) gives it exactly. Without one, the order in which H granted M for that line, plus the holder's local stores between grants, gives the same order. Load perform time: the port monitor sits at the L1 load/store port, below the store buffer, so every load it sees is served by the cache or its miss, never forwarded from the store buffer. It sees issue and completion, not the instant the load read the cache. Any write that performed in between could legally be the one it saw.
A black-box value checker therefore accepts the value of any write between the newest one performed before the load issued and the newest one performed before it completed, and it never lets a core go backwards in a location's write order. The illustrative times below show the rule.
# Black-box value check with windows: the monitor at the L1 load/store port (below the store
# buffer, so no store-buffer forwarding) sees when a load was issued and when its response
# returned, not the instant it read the cache. Writes to X are recorded in
# their serialization order with the time each one performed (illustrative times).
writes = [(0, 0), (5, 1), (20, 2)] # (perform time, unique value): X's write order
def index_at(t):
return max(i for i, (when, _) in enumerate(writes) if when <= t)
def make_checker():
last_seen = {} # per core: newest write index already observed
def check(core, issue, done, value):
order = [v for _, v in writes]
if value not in order: return False # a value nobody wrote
k = order.index(value)
lo = max(index_at(issue), last_seen.get(core, 0))
if not lo <= k <= index_at(done): return False
last_seen[core] = k # this core may never go back before write k
return True
return check
check = make_checker()
assert check("C1", 10, 30, 1) # read before the store at 20 performed: legal
check = make_checker()
assert check("C1", 10, 30, 2) # read after it: also legal, same window
assert not check("C1", 12, 32, 1) # a later load of C1 went backwards: illegal
check = make_checker()
assert not check("C1", 10, 30, 0) # 0 was overwritten at 5, before issue: stale
strict = lambda done, value: value == writes[index_at(done)][1]
assert not strict(30, 1) # golden-at-completion would reject a legal 1
wide = lambda value: value in [v for _, v in writes]
assert wide(0) # any value ever written: accepts the stale 0
print("PASS: the window accepts both legal values, rejects stale and backwards reads, strict and wide rules fail")The strict rule, compare with the golden value at completion, would reject the legal 1. A window that is too wide (any value ever written) would accept the stale 0. The per-core bound is the per-location rule that a core cannot see X go backwards; a monitor placed above the store buffer, at the core port, must also allow this core's newest program-order-earlier store to X that has not yet performed, and under a relaxed model use the rules of the named model, as Coherence Is Not Consistency explains.
Stop stimulus, let every message drain, then check in this order: no message in flight, every MSHR and home pending entry free (a leaked entry is a future hang), every credit returned. Then flush: make each cache write back its dirty lines (or read them through a backdoor) and compare memory with the newest write of every address the test touched. A test that ends with a dirty line still in a cache has not proven that the data would survive its eviction. The directory entry for each line must also match the cache tags after the flush.
The load is legal. It could have read the line after the store performed at 20, so both 1 (the value before) and 2 are allowed. The checker must use the window from issue to completion, not one instant inside it.
No. The newest value has never left C0. Flush it at the end of the test (PutM, then H writes memory) and compare memory with 7. Only then has the writeback path for that line been checked.