These questions test whether you can prove a coherence design works and find out why it does not. A strong answer always names the reference (the store history, not memory), says where each check observes, and shows the checker has been seen to fail. For silicon, it captures before it guesses and finds the first illegal step, not the symptom.
Field | Answer |
|---|---|
Interviewer is testing | A concrete bug that keeps every state legal, and the golden-memory check. |
Weak answer | We check SWMR and that the directory matches the tags. |
Strong answer (a 4) | Assumption: the MSI dirty read, C0 M / 1, C1 sends GetS. Mechanism: inject a data-select bug: H's speculative memory read (0) is sent to C1 instead of C0's Data(1). Every state and directory entry is legal (S{C0,C1}, two S copies), so a state checker passes, while C1 loads 0. The specification is per-location write serialization: stores build each location's write order (the golden value), and every load is compared with the newest write it is serialized after. Trade-off: the checker must observe below the store buffer, where the golden value is exact; at the core port the named memory model decides what is allowed. Evidence: unique store values (a counter, or writer id plus sequence number), so every returned value names exactly one write; with repeated values this bug can be invisible. |
Follow-ups | At step 4, which fails: one M at most, directory matches tags, every usable copy equals golden? (Only the third.) Why not compare loads with memory? (Memory is legally stale.) |
Common trap | Taking the load's perform time from issue or retirement instead of when it read a copy. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | Structure, independence from the RTL and the checks that run after every event. |
Weak answer | A C model of the cache that we compare outputs with. |
Strong answer (a 4) | Assumption: course protocol, MSI, three caches (so a GetM can wait for more than one Inv-Ack), one line. Mechanism: a protocol half (cache and home rules, one busy entry per line at H, Inv-Acks collected at H, late Puts acknowledged with no change) and a checker half (golden value, SWMR, every usable copy and every load equal golden, every message legal in the receiver's state, a drain check at the end). The network is an unordered list driven by a seeded generator. Only new requests wait behind the busy entry; responses must always sink. Trade-off: a simple model runs thousands of events per second but omits E and O, multiple outstanding requests and real queues, and uses a grant-delivery oracle. Evidence: write it from the specification, not the RTL, and show it fails on a planted bug (a home that acks PutM without writing memory is caught at the next memory-sourced read). |
Follow-ups | What if H cleared busy when it sent Data rather than on delivery? (An Inv or Fwd overtakes the Data and the model reports a protocol error.) Why unique store values? (Stale reads become visible.) |
Common trap | Sharing code between the model and the RTL, so one misreading agrees with itself. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | Bug injection, window sensitivity and directed stress. |
Weak answer | It has been running for months with no failures. |
Strong answer (a 4) | Assumption: the course reference model with single-change bugs: (a) early grant with an ack outstanding, (b) no downgrade on Fwd-GetS, (c) memory answers a GetS while a cache holds M. Mechanism: inject each and confirm it fails. Bug a needs a sharer, Data arriving before the Inv, and for a value check a load inside that window. Trade-off: in 30-event runs over 100 seeds, bug a was caught 52 times with random delivery, 99 with a delay knob on Inv, and 9 with only the value and protocol checks; per-event SWMR catches it at the grant. Evidence: keep every failing seed as a regression, include bugs whose first symptom is a value, a hang (a lost Inv-Ack) and an illegal message, and after a fix rerun the directed race plus fresh seeds. |
Follow-ups | Why is 'the failing seed passes now' not proof? (A changed design shifts every interleaving.) What does a delay knob buy? (A sometimes-seen window becomes an always-seen one.) |
Common trap | Injecting only bugs the checker was written for. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | Mapping states, including transients, to permissions, and a ghost for values. |
Weak answer | assert property ($onehot0(state == M)). |
Strong answer (a 4) | Assumption: one checker per address that sees every cache's state at once. Mechanism: map states first. Readable: S, SM^D, E, O, M. Not readable: I, IS^D, IM^D, EI^A, SI^A, II^A, and MI^A (dirty, data in the WB entry). Writable: E or M. Then assert $onehot0(writable) and 'if any cache is writable, readable equals writable'. Add a single-dirty-holder assertion over M, O and MI^A (needed in every protocol, since SWMR does not see MI^A beside an M). For values, a ghost variable updated from performed stores (X = 0 at reset) must equal every readable copy. Trade-off: concurrent clocked assertions can be proved by formal; an immediate form in always_comb checks only in simulation. Evidence: on the broken upgrade, SWMR fires at the grant while bits still agree; the value assertion only after the store. |
Follow-ups | What does forgetting that SM^D is readable miss? (A grant of M to C0 while C1 still serves loads in SM^D.) Why not use memory as the reference? (False failures on legal M / 1 with memory = 0, missed lost writes.) |
Common trap | Feeding the ghost from the bus or directory, the same path the bug corrupts. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | Safety versus liveness, fairness and bounded substitutes. |
Weak answer | Yes, the key invariant is proved. |
Strong answer (a 4) | Assumption: course home with an arbiter for X. Mechanism: no. A controller that never grants anything satisfies SWMR forever. Safety (nothing bad happens: SWMR, data value, single dirty holder) has finite counterexamples; liveness (every accepted GetM is granted, every Put gets Put-Ack) has infinite lasso counterexamples and needs fairness assumptions on delivery, arbitration, credits and acceptance. In SVA the unbounded form is s_eventually (IEEE 1800-2017); a bounded req |-> ##[1:N] done is really a safety property. Trade-off: bounded checks give a product number and are easy to run, but N must be argued and they assume bounded environment delays. Evidence: with fixed priority C0 can win forever (a lasso while SWMR holds); round robin grants C1 within 2 arbitration steps. Pair the bounded check with an end-of-test drain check. |
Follow-ups | Is 'granted within 200 cycles' safety or liveness? (Safety.) Why does a weak bounded consequent pass a test that ends early? (The trace ends inside the window.) |
Common trap | Calling the protocol verified on safety alone. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | Assumptions, vacuity, covers and witnesses. |
Weak answer | The tool says proven, so it is proven. |
Strong answer (a 4) | Assumption: list every environment assumption with its reason: one request per line per cache, legal message sequences, responses only to requests, finite outstanding work, eventual delivery for liveness only. Mechanism: an assumption such as 'no GetM while a sharer exists' deletes every trace in which an Inv is sent, so the early-grant bug disappears and every assertion about the ack path is vacuously true. Write covers for the intended scenarios (GetM with a sharer, Inv sent, late Inv-Ack), read a witness trace per important assertion and check vacuity reports. Trade-off: each extra assumption shrinks the proof's world; ideally prove each one as an assertion on the neighbouring block (assume-guarantee). Evidence: covers reached, a witness that exercises the consequent, and a seeded bug that the proof catches. |
Follow-ups | c_inv_sent is unreachable: what next? (Find the blocking assumption or tie-off, weaken it, rerun.) Can bring-up assumptions stay in sign-off? (No.) |
Common trap | Adding an assumption to silence a counterexample before deciding whether it is legal. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | A coverage model from the protocol table, race crosses and engineered stimulus. |
Weak answer | Cover every state and every message type. |
Strong answer (a 4) | Assumption: the course MSI controller with transients. Mechanism: cover the full state-by-event cross: 9 states by 8 events give 72 cells, 39 legal (22 actions, 17 stalls) and 33 impossible; impossible cells become illegal bins and assertions, never ignore_bins. Then race crosses: the transient state, the arriving message, its cause and, where it matters, the order at H, with both orders as bins, counted only on runs the value checker passed: (SM^D, Inv), (MI^A, Fwd-GetS), (MI^A, Fwd-GetM), (SI^A, Inv), a late PutM from a non-holder. Trade-off: uniform random traffic rarely hits them (illustrative: 0.024% per window for 2 cores over 4,096 lines against 82.8% for 8 cores on 4 lines), so knobs are needed: hot lines, tiny caches, per-class delays, backpressure. Evidence: on the course model, hits of (MI^A, Fwd-GetS) went from 4 (baseline) to 1,405 with hot spot, tiny cache and slow writebacks together. |
Follow-ups | (MI^A, Put-Ack) and (M, Fwd-GetS) are covered: is the eviction race covered? (No.) Why can a hot-spot profile miss (SI^A, Inv)? (Nothing is ever evicted.) |
Common trap | Waiving a reachable race cell because it is rare. |
Taught in | State and Transition Coverage, Race and Cross Coverage and Directed Race Stress |
Field | Answer |
|---|---|
Interviewer is testing | Trace-first method and mapping the supplier of the value to a bug class. |
Weak answer | Rerun with more logging and look at the cache that returned it. |
Strong answer (a 4) | Assumption: a trace buffer at H filtered on the line, records with line address, type and direction, source and destination, transaction id and timestamp (state and payload optional; value bugs need the payload). Mechanism: five steps: which word and values; is the older value forbidden by the named model; reconstruct write epochs in H's accept order; find who supplied the stale value (the reader's own copy, memory or another cache); find the rule that supply broke. Classes: missed Inv, grant before Inv-Ack, memory answered while a dirty copy existed, lost writeback (Put-Ack with no memory write), late PutM from a non-holder accepted as a writeback, late Data installed after an Inv. Trade-off: the first illegal step is usually several records before the symptom. Evidence: replay the capture against the protocol rules, not only the values, which would report the load but never the cause. |
Follow-ups | The Inv-Ack arrived before the grant but the reader still read stale data: where next? (The reader's Inv handling in S and in IS^D.) What if a forward record is missing? (Check the overflow flag and filters first.) |
Common trap | Patching the load path where the wrong value appeared. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | Wait-for chains from a consistent snapshot and classification. |
Weak answer | It is a deadlock: add a timeout and retry. |
Strong answer (a 4) | Assumption: course controllers with MSHRs, pending entries and credited queues. Mechanism: freeze (or read twice and compare), dump every MSHR and H's pending entry for the line and the occupancy and credits of every queue on the path, draw one edge per wait (waiter, target, item) and follow it. A chain that ends at an agent with no record of the item is a lost message; a chain that closes on itself, with identical dumps, is a deadlock; counters rising with no completions is livelock; one entry ageing while others complete is starvation. Trade-off: a lost Inv shows up as a hang only because H's ack counting refuses to grant early, which is the safe failure. Evidence: worked case, H pend GetM C0, acks 0/1, C1 still S / 0 with nothing queued: the Inv was lost. If C1 is I with nothing queued, check for a PutS first, then the Inv-Ack path. A P/Q credit cycle needs a reserved response path, not retransmission. |
Follow-ups | Why not read MSHRs while running? (The dump can show a cycle that never existed.) One line or many? (Many points to a resource or credit cycle.) |
Common trap | Calling every timeout a deadlock. |
Taught in |
Field | Answer |
|---|---|
Interviewer is testing | The asymmetry of evidence and how a harness creates rare timing. |
Weak answer | If we never see a bad outcome, the ordering logic is correct. |
Strong answer (a 4) | Assumption: name the architecture, revision, fences and memory type; X and Y in different lines. Mechanism: an outcome the model forbids, seen once, is a bug; an allowed outcome never seen proves nothing (the part may be stronger, or the harness never made the timing). MP (1,0) with plain accesses on Armv8-A is legal; with DMB ISH on both sides it is a bug. CoRR going backwards is forbidden on every model. Trade-off: knobs that make windows reachable cost run time: iterations (10^6 to 10^9), random delays, thread placement, cache preconditioning (flush X so its store misses), background pressure, memory layout. Evidence: compare the histogram with the model's allowed set, for example with herdtools7 (diy7 generates tests, litmus7 runs them, herd7 computes the allowed set), and check that every allowed outcome appeared to judge the stress. A store buffer that lets a hitting store drain past a missing one shows MP (1,0) only when X is flushed first. |
Follow-ups | What if a forbidden outcome appears once? (Reproduce and triage: never rerun until it passes.) Which test needs four agents? (IRIW.) |
Common trap | Comparing the histogram with a guess about the pipeline instead of the model. |
Taught in |
No. The newest value never left C0, so the PutM path for that line was never exercised. Add the end-of-test sequence: stop stimulus, drain until no message is in flight and every MSHR, pending entry and credit is free, then flush every dirty line (PutM, H writes memory, Put-Ack) and compare memory with the newest write of each address, and the directory with the tags.