Cache Coherency Over CXL

Chapter 11.2 made remote capacity addressable. The host owned the ranges, the host managed the coherency flows, and the memory chiplet was a target — one value per address, one owner, and a reference model that held exactly that.

This chapter removes that simplification. The accelerator on the other die now holds copies of host memory in its own cache, and the moment it does, three things stop being true: correctness is no longer a property of either die, the device owes responses to events it did not initiate, and the value at an address is no longer a single fact anyone can look up.

That is a categorical change, not an incremental one. It is also where the hardest bugs in chiplet integration live, because a coherence failure produces wrong answers with a completely clean link — and every diagnostic an engineer reaches for first reports health.

1. The One-Sentence Model

Coherence is distributed ownership tracking, and the state that makes it work is mostly the state that exists while ownership is changing.

The first half is the idea. The second half is why this chapter is long. A design that implements four stable line states and no transient ones will pass every single-threaded test and fail in silicon, for reasons §11 makes normative rather than merely plausible.

2. Sourcing, and Where the Line Is

3. What Coherence Actually Has to Decide

Strip away the protocol and coherence is a set of questions that must have answers before an access can be served. For every cache line the system must be able to determine:

• who may hold a copy?
• who holds the newest data — which may not be memory;
• may this agent read locally, right now, without asking anyone?
• must another agent be invalidated before this write proceeds?
• is a transaction currently in the middle of changing the answer to any of the above?

The first four are what people picture. The fifth is the chapter. It is also the one with no representation at all in a design that models only stable states, and the specification requires that it be tracked — §19 is the exact sentence.

4. Two Agents, Six Channels, and Who Owns What

The structure the specification defines, at the level this chapter needs.

The Home Agent sits on the host. The specification defines it as the agent responsible for resolving system-wide coherency for a given address. It is the serialisation point: it decides who gets ownership next, and it is the only party with a system-wide view.

The DCOH sits on the device. The specification defines it as the agent responsible for resolving coherency with respect to device caches. In the CXL.mem context the specification adds that where the subordinate is an accelerator, the DCOH is assumed responsible for coherency functions such as snooping device caches based on CXL.mem commands.

Between them, CXL.cache provides three channels in each direction — Request, Response, and Data — with the directions named D2H and H2D. Six channels, and their differences are not cosmetic: §32 shows that the forward-progress class of each channel is what prevents the protocol from deadlocking, and that a design which merges them destroys that property.

Read the table for its asymmetry. The device's Response channel exists to answer host requests, and the host's Response channel exists to answer device requests. Both directions are simultaneously requester and responder, which is precisely what makes coherence a distributed problem and a deadlock risk.

5. Which Revision's Coherence Model

A section that cannot be skipped, because the answer changed.

In CXL 1.0 the coherency model for device-attached memory is Bias Based coherency, with memory in host bias when it is expected to be accessed mainly by the host and device bias when mainly by the device, and the DCOH described as managing those bias states.

The CXL 3.0 white paper states that a major enhancement in CXL 3.0 is the ability to back-invalidate the host's caches, that this model of maintaining coherency for host-managed device-attached memory is called enhanced coherency, and that it replaces Bias Based coherency introduced in previous generations. The Consortium's tutorial adds the motivation directly: the existing bias-flip mechanism required HDM to be tracked fully because the device could not back-snoop the host, and back-invalidation enables a snoop filter implementation, so that a much larger amount of memory can be mapped as HDM. The Consortium's feature summary places enhanced coherency on the 256-byte flit format.

What that means for a design. The direction in which a snoop can travel is a revision-dependent capability. Under bias-based coherency the host snoops the device; under enhanced coherency the device can also invalidate the host. A device coherence agent designed for one is not a device coherence agent for the other, and a verification environment that models one will not exercise the other's flows at all.

What this chapter therefore teaches. The mechanisms that are true in both: transient state, same-line serialisation, probe-versus-local races, dirty-data ownership, and the transport-boundary rules. The specific message set, and which direction may initiate what, comes from your revision. This is not hedging — it is the only defensible way to teach a protocol whose coherence model was replaced between revisions.

6. One Ownership Change, End to End

Three things the figure is drawn to show.

The device's line is in a transient state for the whole middle of the exchange. It is not the old state, because a request is outstanding. It is not the new state, because permission has not arrived. §11 is about representing that interval.

The host serialises. The other agent is invalidated before the grant is sent, not after. That ordering is the Home Agent's job and it is the reason ownership is unambiguous.

The UCIe transport appears twice and understands nothing. It delivers a request and a grant. It has no idea that one is a permission, and §27 is about keeping it that way.

7. Cache-Line Metadata

// ILLUSTRATIVE device-side coherence metadata — a teaching model of what a
// DCOH must hold per line. NOT a CXL state encoding, NOT a CXL register, and
// NOT a claim about how any CXL agent represents line state.
typedef struct packed {
  coh_state_t state;          // §11 — stable AND transient
  logic       dirty;          // this copy differs from memory
  logic       probe_pending;  // §19 — a probe hit this line and is unresolved
  logic       txn_pending;    // §14 — a local transaction owns this line
} line_meta_t;
 
line_meta_t meta_q [NUM_LINES];

Architecture. Four fields, and the last two are the ones a first implementation omits. state and dirty describe what the device has; probe_pending and txn_pending describe what the device is in the middle of, and every race in this chapter is invisible without them.

State. NUM_LINES entries with per-cache-line lifetime — indexed by address, persisting across requests, across link epochs, and across everything else. Chapter 11.1 §25 called this out as a lifetime unlike anything in Modules 9 or 10, and §30 is where the consequence bites.

Cycle behaviour. Read on every local access to decide whether a hit is legitimate. Written on fills, evictions, local writes, and on protocol events arriving from the host — that last class arriving independently of local activity, which makes this a genuinely multi-writer structure and §13 the bug it produces.

Contract. The local datapath relies on it for permission, not merely for presence. The coherence engine relies on it to compute what the device owes when a probe arrives. Both must see a consistent view, which is a real design problem when both can update it in the same cycle.

Failure. Metadata and data going out of step, which is the coherence-layer form of the misalignment bug this curriculum keeps meeting (Chapter 10.2 §7, Chapter 10.4 §11, Chapter 11.2 §15). Metadata saying valid over data never filled produces a hit returning uninitialised contents.

DV. The cheap pairing invariants first, because they cost nothing and catch update-ordering bugs:

// Illustrative pairing invariants — the cheapest coherence assertions there are.
property p_dirty_implies_valid;
  @(posedge clk) disable iff (!rst_n)
    meta_q[i].dirty |-> (meta_q[i].state != C_INVALID);
endproperty
 
property p_invalid_implies_clean;
  @(posedge clk) disable iff (!rst_n)
    (meta_q[i].state == C_INVALID) |-> !meta_q[i].dirty;
endproperty
 
// A line cannot be in a transient state with no transaction to explain it.
property p_transient_implies_pending;
  @(posedge clk) disable iff (!rst_n)
    is_transient(meta_q[i].state) |-> (meta_q[i].txn_pending || meta_q[i].probe_pending);
endproperty

8. A Tag Hit Is Not Permission

The single most consequential line of RTL in the chapter, and it is one expression long.

// WRONG — presence mistaken for permission. This is a correct private cache
// and a catastrophic coherent one.
assign read_hit  = tag_match[req_idx];
assign read_data = line_data_q[req_idx];

Architecture. A tag match says the data for this address is in this array. It says nothing about whether the copy is still legitimate, whether a transaction is changing its status, or whether another agent has since taken ownership. In a private cache — Chapter 11.1 §13's case — those questions do not exist. In a coherent cache they are the entire point.

Cycle behaviour. Fast, short, and correct for every single-agent test.

Failure. The line is present and C_INVALID, or present and mid-transition, and the device returns stale or not-yet-permitted data. And note that this failure is worse than Chapter 11.1 §13's, because there the design had no invalidation mechanism at all and the bug was architectural. Here the mechanism exists, the metadata is correct, and the datapath simply does not consult it — so the design looks coherent, reviews as coherent, and is not.

The right shape is a permission function, not a comparison:

// Illustrative permission predicates. Naming them as functions rather than
// inlining the comparisons is not style — it means the same rule is used by
// the datapath, by the probe handler, and by the assertions, so they cannot
// drift apart.
function automatic logic is_transient(coh_state_t s);
  return (s == C_S_TO_X) || (s == C_I_TO_S) || (s == C_I_TO_X) || (s == C_X_TO_I);
endfunction
 
function automatic logic read_allowed(coh_state_t s);
  // A read may be served from any state that holds a legitimate copy.
  // Transient states are excluded DELIBERATELY: during an ownership change
  // the device does not know what it is allowed to do with the line.
  return (s == C_SHARED) || (s == C_EXCLUSIVE) || (s == C_MODIFIED);
endfunction
 
function automatic logic write_allowed(coh_state_t s);
  // A write requires exclusive rights. Shared is not enough: another agent
  // may hold a readable copy that would become stale.
  return (s == C_EXCLUSIVE) || (s == C_MODIFIED);
endfunction
 
assign read_hit  = tag_match[req_idx] && read_allowed(meta_q[req_idx].state)
                                      && !meta_q[req_idx].probe_pending;
assign write_hit = tag_match[req_idx] && write_allowed(meta_q[req_idx].state)
                                      && !meta_q[req_idx].probe_pending;

Why probe_pending gates the access too. A probe has arrived and the device has not yet answered it. The line's stable state still says the copy is legitimate, and by the time the probe is answered it will not be. Serving an access in that window is serving data whose legitimacy is already being revoked, and §19 is the specification requirement that makes tracking this mandatory rather than prudent.

// Illustrative — local access only from a permitted state. The executable form
// of "a tag hit is not permission".
property p_read_only_when_permitted;
  @(posedge clk) disable iff (!rst_n)
    local_read_hit |-> read_allowed(meta_q[req_idx].state);
endproperty
a_read_only_when_permitted: assert property (p_read_only_when_permitted);
 
property p_write_only_with_ownership;
  @(posedge clk) disable iff (!rst_n)
    local_write_commit |-> write_allowed(meta_q[req_idx].state);
endproperty
a_write_only_with_ownership: assert property (p_write_only_with_ownership);
 
// No access is served out of a transient state, in either direction.
property p_no_access_in_transient;
  @(posedge clk) disable iff (!rst_n)
    (local_read_hit || local_write_commit) |-> !is_transient(meta_q[req_idx].state);
endproperty
a_no_access_in_transient: assert property (p_no_access_in_transient);

On what these assertions are. They are implementation policy for this model, not CXL requirements. What CXL requires of a device's caches is the specification's to state. What these encode is that this design's datapath and this design's metadata agree — which is the property that fails when someone optimises the hit path.

9. Wrong RTL — the Bug in Its Most Realistic Form

The §8 version is obvious once stated. Here is the version that actually ships.

// WRONG, and much harder to see. The permission check exists, but it reads a
// REGISTERED COPY of the state captured a cycle earlier for timing.
always_ff @(posedge clk) state_shadow_q <= meta_q[req_idx].state;
 
assign read_hit = tag_match_q && read_allowed(state_shadow_q);

Architecture. Someone found that the tag lookup, the metadata read, and the permission function did not meet timing in one cycle, and pipelined the permission check. The logic is now one cycle stale.

Cycle behaviour. In the overwhelming majority of cycles, identical. In the cycle where a probe invalidates the line, meta_q updates and state_shadow_q does not — for exactly one cycle.

Failure. A read that arrives in that one cycle is served from a line the device has already given up. The data is stale by one coherence event, and there is no evidence: the metadata is correct, the probe was handled correctly, the response to the host was correct. Only the access that slipped through is wrong, and only if something was actually written to that line elsewhere.

Why it is a genuinely hard bug. It requires a probe and a local access in adjacent cycles to the same line, plus a remote write, plus something that consumes the value. Random testing hits that conjunction rarely. It reproduces intermittently. And the natural first hypothesis — that the coherence state machine is wrong — is false, which sends the investigation to the wrong module.

The fix is structural. Either the permission check reads the same cycle's metadata, or the pipeline stage is accompanied by an explicit invalidation-forwarding path and an assertion that the shadow copy matches:

// Illustrative — if the state must be pipelined, prove the copy is coherent
// with the source at the point of use.
property p_shadow_matches_meta;
  @(posedge clk) disable iff (!rst_n)
    read_hit |-> (state_shadow_q == meta_q[req_idx].state);
endproperty

DV. This is what the directed test in §32's coverage list — probe and local access to the same line in the same or adjacent cycles — exists for. It will not arrive by chance.

10. Why Stable States Are Not Enough

Now the central argument, and it is stronger than "transient states are good practice". The protocol makes them necessary.

So the state space has three regions, not one. Stable states, in which the device knows what it may do. Transient states, in which a transaction it initiated is changing that. And probe-shadowed states, in which a transaction the host initiated is changing it. A design that models only the first cannot even express the situations the protocol guarantees will occur.

11. Transient States

// ILLUSTRATIVE coherence states — a teaching model, NOT a CXL state encoding
// and NOT a claim about any CXL agent's state set. The stable names are the
// classical architecture vocabulary; the transient names are this model's own.
typedef enum logic [2:0] {
  // Stable — the device knows what it may do with the line.
  C_INVALID   = 3'd0,   // no usable copy
  C_SHARED    = 3'd1,   // readable; others may hold it too
  C_EXCLUSIVE = 3'd2,   // readable and writable; no other copy expected
  C_MODIFIED  = 3'd3,   // written locally; this is the only current value
 
  // Transient — a transaction is changing what the device may do. Each is a
  // DISTINCT state because each owes a different answer to an arriving probe.
  C_I_TO_S    = 3'd4,   // asked for a readable copy, waiting
  C_I_TO_X    = 3'd5,   // asked for write ownership from nothing, waiting
  C_S_TO_X    = 3'd6,   // hold a readable copy, upgrading to writable
  C_X_TO_I    = 3'd7    // giving the line up; data may still owe a transfer
} coh_state_t;

Architecture. Four transient states rather than one "busy" flag, and the reason is §19: what the device must do when a probe arrives depends on which transition is in flight. A line in C_S_TO_X still holds readable data and can supply it. A line in C_X_TO_I may be the only holder of modified data that has not yet been transferred. A line in C_I_TO_S holds nothing yet. Collapsing these into one bit forces the probe handler to guess.

State. Three bits per line, per-cache-line lifetime, though the transient values themselves have per-coherence-transaction lifetime — they exist only while a transaction does. Two lifetimes in one field is worth noticing, because it is why §30's recovery question is hard.

Cycle behaviour. Entered when a transaction is issued, left when it resolves. Crucially, the transitions are driven from two independent sources — local transaction completion and incoming host events — and §13 is the bug that follows from not acknowledging that.

Contract. The datapath uses the state for permission (§8). The probe handler uses it to compute a response. The transaction table (§14) must agree with it.

Failure. Without C_S_TO_X as a distinct state, a device that has requested an upgrade while holding a shared copy either refuses to serve reads it is entitled to serve — a performance bug — or serves a write it has not yet been granted, which is a correctness bug that produces two writers.

DV. Cover every state. Then cover every state crossed with every incoming event class. That cross is the real state space, and the transient rows are the ones that a stable-state-only testbench cannot even reach.

12. The Next-State Function, With Explicit Event Priority

// ILLUSTRATIVE next-state logic for one cache line's coherence state.
// ONE always_comb, ONE priority order, ONE assignment per output. The
// structure is the lesson: coherence state has several concurrent event
// sources, and the order in which they are resolved must be a stated policy
// rather than an accident of how the if-statements were typed.
//
// The PRIORITY ORDER BELOW IS THIS MODEL'S POLICY. It is NOT a CXL-mandated
// priority, and no such claim is made.
always_comb begin
  // Defaults: hold. Assigning every output first means no latch and no
  // dependence on which branch happened to be written last.
  next_state        = meta_q[idx].state;
  next_dirty        = meta_q[idx].dirty;
  next_probe_pend   = meta_q[idx].probe_pending;
  next_txn_pend     = meta_q[idx].txn_pending;
  probe_rsp_send    = 1'b0;
  probe_rsp_fwd_data = 1'b0;
 
  unique case (1'b1)
    // ---- 1. Error and reset conditions win. Nothing below can be trusted
    //         if the line's state is being torn down deliberately (§30).
    coh_teardown[idx]: begin
      next_state      = C_INVALID;
      next_dirty      = 1'b0;
      next_probe_pend = 1'b0;
      next_txn_pend   = 1'b0;
    end
 
    // ---- 2. An arriving probe is RECORDED before anything else acts on the
    //         line. Recording is not the same as answering: the response may
    //         have to wait for a pending local transaction to reach a point
    //         where the answer is well defined (§19).
    probe_arrive[idx]: begin
      next_probe_pend = 1'b1;
      // The response depends on the CURRENT state, including transient ones.
      // A line being given up may owe data; a line not yet filled owes none.
      probe_rsp_send     = !is_transient(meta_q[idx].state) || (meta_q[idx].state == C_X_TO_I);
      probe_rsp_fwd_data = meta_q[idx].dirty &&
                           (meta_q[idx].state == C_MODIFIED || meta_q[idx].state == C_X_TO_I);
    end
 
    // ---- 3. A probe already recorded and now resolvable is answered and
    //         the line moves to whatever the probe requires.
    probe_resolve[idx]: begin
      next_probe_pend = 1'b0;
      next_state      = probe_requires_invalid[idx] ? C_INVALID : C_SHARED;
      next_dirty      = probe_requires_invalid[idx] ? 1'b0
                                                    : (meta_q[idx].dirty && !probe_took_data[idx]);
    end
 
    // ---- 4. A local transaction completing. Ranked BELOW probe handling so
    //         that a grant cannot overwrite an unanswered probe's effect —
    //         which is §13's bug.
    txn_complete[idx]: begin
      next_txn_pend = 1'b0;
      next_state    = txn_granted_state[idx];
      next_dirty    = (txn_granted_state[idx] == C_MODIFIED) ? 1'b1 : meta_q[idx].dirty;
    end
 
    // ---- 5. A new local request may only start on a QUIET line (§15).
    txn_start[idx] && !meta_q[idx].txn_pending && !meta_q[idx].probe_pending: begin
      next_txn_pend = 1'b1;
      next_state    = txn_transient_state[idx];
    end
 
    default: ;   // hold
  endcase
end
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    for (int l = 0; l < NUM_LINES; l++) begin
      meta_q[l].state         <= C_INVALID;
      meta_q[l].dirty         <= 1'b0;
      meta_q[l].probe_pending <= 1'b0;
      meta_q[l].txn_pending   <= 1'b0;
    end
  end else begin
    meta_q[idx].state         <= next_state;
    meta_q[idx].dirty         <= next_dirty;
    meta_q[idx].probe_pending <= next_probe_pend;
    meta_q[idx].txn_pending   <= next_txn_pend;
  end
end

Classification: synthesizable, illustrative microarchitecture. The priority order is this model's policy, stated as such. The obligations it encodes — that a probe hitting a pending eviction must be tracked, that a dirty line must return data — are from §18 and §19's verified requirements.

Architecture. One combinational block, one priority order, one assignment per output. The unique case (1'b1) idiom makes the priority explicit and makes an unintended overlap a simulation error rather than a silent precedence.

State. The metadata of §7, written from exactly one place.

Cycle behaviour. Every event source is evaluated in the same cycle against the same current state, and exactly one branch fires. Recording a probe and answering it are separate branches, because the answer may not be computable yet.

Contract. The transaction table (§14) must be updated consistently with this — the same cycle, the same conditions. Two structures describing one line's status is itself a coherence problem, one level down.

Failure. §13, immediately.

Deliberately simplified: one line's logic shown, with idx selecting it; a real design handles concurrent events on different lines and must arbitrate the metadata array's ports. The probe response is a single pulse rather than a channel with backpressure. And the transient-state set is minimal — a real agent typically has more.

13. Wrong RTL — Two Independent State Assignments

// WRONG — two always_ff blocks (or two if-statements in one) writing the same
// state from two event sources. Each is individually correct and reviewable.
always_ff @(posedge clk) begin
  if (probe_arrive[idx] && probe_requires_invalid[idx])
    meta_q[idx].state <= C_INVALID;         // the probe's effect
end
 
always_ff @(posedge clk) begin
  if (txn_complete[idx])
    meta_q[idx].state <= txn_granted_state[idx];   // the grant's effect
end

Architecture. Two writers, no arbitration, and no statement anywhere of what happens when both fire.

Cycle behaviour. In simulation, the last assignment executed wins, which depends on the order the blocks appear in the file. In synthesis, the tool builds whatever multiplexer it infers and may warn, or may not.

Failure, and it is the most dangerous single bug in the chapter. An invalidating probe and a completing ownership grant land in the same cycle. The grant wins. The line becomes C_MODIFIED for a device the host believes has just invalidated it.

Now trace the consequences:

• The device believes it has exclusive write rights. It writes.
• The host believes the device has no copy, so it grants ownership to another agent. Two writers.
• The device's dirty data will eventually be written back, overwriting whatever the other agent wrote — or the other way round, depending on timing.
• Meanwhile the probe was answered as though the invalidation had happened, so the host's tracking is consistent with a device state that does not exist.

No error is reported anywhere. The link is clean. Every message was well formed and every response was legal. The distributed state is simply inconsistent, and the observable symptom is a wrong value in memory, arbitrarily far from the cause.

Why review misses it. Each block is short, has a single obvious purpose, and is correct in isolation. The bug is in the absence of a statement about their interaction, and absences do not appear in diffs.

Why simulation misses it. The conjunction requires a probe and a grant for the same line in the same cycle. Unless the testbench deliberately creates that alignment — §32's coverage cross — it may never occur.

The fix is §12's structure, and the assertion that makes a regression of it visible:

// Illustrative — the state has exactly one writer, and the priority is honoured.
// If a probe requiring invalidation is recorded, a grant in the same cycle
// must NOT leave the line in a writable state.
property p_probe_beats_grant;
  @(posedge clk) disable iff (!rst_n)
    (probe_arrive[idx] && probe_requires_invalid[idx] && txn_complete[idx])
      |=> !write_allowed(meta_q[idx].state);
endproperty
a_probe_beats_grant: assert property (p_probe_beats_grant);

14. The Coherence Transaction Table

A line with a transaction in flight needs more context than three bits of state.

// ILLUSTRATIVE per-transaction context for an in-flight coherence operation.
// Deliberately NOT called an MSHR: that name implies a specific miss-handling
// architecture this model does not commit to. NOT a CXL structure.
typedef struct packed {
  logic                 valid;
  logic [LINE_ADDR_W-1:0] line_addr;    // cache-line granular — see below
  logic [REQ_ID_W-1:0]  local_req_id;   // who asked, on the device side
  coh_state_t           target_state;   // what we are trying to reach
  logic                 probe_seen;     // §19 — a probe hit while we were open
  logic                 data_received;  // §10 — data may precede permission
  logic                 perm_received;  // ... and permission may precede data
} coh_txn_t;
 
coh_txn_t coh_txn_q [MAX_COH_TXN];

Architecture. data_received and perm_received are separate bits, and that is §10's normative rule made structural: the specification states that data for a read may arrive before its Global Observation and that the device may consume it, with the GO arriving later to say what state to cache it in. A design with one "response arrived" bit cannot represent the legal intermediate state.

Note the address granularity. The specification's CXL.cache request and snoop addresses identify a cache line — the address field starts above the line offset — and the same-address restrictions of §15 are stated per cache line. So the conflict-detection granularity is not a design choice; it is set by the protocol, and a design that detects conflicts at a coarser granularity serialises unnecessarily while one that detects at a finer granularity misses conflicts entirely.

State. MAX_COH_TXN entries with per-coherence-transaction lifetime, allocated when a transaction is issued and freed exactly once when it resolves.

Cycle behaviour. Allocation gates issue. probe_seen is set by the probe handler, not by the requester, which makes this a structure written from both sides — with the same discipline §13 demands.

Contract. The state machine of §12 and this table describe the same line and must agree. An entry with valid set implies the line's state is transient, and the reverse.

// Illustrative — the two structures cannot disagree about whether a line is busy.
property p_txn_implies_transient;
  @(posedge clk) disable iff (!rst_n)
    (coh_txn_q[t].valid && line_of(coh_txn_q[t].line_addr) == idx)
      |-> is_transient(meta_q[idx].state);
endproperty

Failure. A table that can hold two entries for one line is §16.

15. Same-Line Conflict — What the Specification Actually Requires

This is where a coherence design is won or lost, and the rules are published rather than a matter of taste.

So the design consequence is precise, and it is not "serialise everything":

At most one ownership-changing transaction per cache line at a time; concurrent non-ownership requests permitted, with the device responsible for whatever ordering it needs.

// Illustrative same-line conflict detection. The GRANULARITY (cache line) and
// the RESTRICTION (one ownership-changing transaction per line) follow the
// verified rules above; the associative-match implementation is illustrative.
logic [MAX_COH_TXN-1:0] same_line_vec;
logic                    same_line_busy;
 
always_comb begin
  for (int t = 0; t < MAX_COH_TXN; t++)
    same_line_vec[t] = coh_txn_q[t].valid &&
                       (coh_txn_q[t].line_addr == new_req_line_addr);
  same_line_busy = (same_line_vec != '0);
end
 
// A new OWNERSHIP-CHANGING request may only be issued on a quiet line. A
// non-ownership request need not be blocked by this, but the device must then
// own its ordering — which is a deliberate design decision, not a default.
assign coh_txn_issue_ok =
    coh_txn_free_entry
 && !(new_req_changes_ownership && same_line_busy)
 && !(new_req_changes_ownership && meta_q[new_req_idx].probe_pending);

Architecture. An associative match over the transaction table, at cache-line granularity, qualified by whether the new request changes ownership.

Why probe_pending is also a blocker. A probe is an ownership change initiated by the host. Starting a device-side ownership change on a line with an unanswered probe creates exactly the two-transaction situation the rules forbid — from both directions at once, which is worse than either alone.

Failure. §16.

DV. The conflict cases must be constructed. Cover: a second ownership request to a busy line; a non-ownership request to a busy line; a probe to a line with a transaction open; a transaction attempt on a line with a probe open. Random stimulus over a large address space almost never produces same-line pairs, which is why same-line traffic must be a deliberate stimulus mode with a deliberately small address footprint.

16. Wrong RTL — Two Ownership Transactions for One Line

// WRONG — allocation checks only for a free entry, not for a line conflict.
assign coh_txn_issue_ok = coh_txn_free_entry;

Architecture. The table is treated as a pool of slots rather than as a set of claims on lines. Nothing prevents two entries naming the same line.

Cycle behaviour. Both transactions are issued. Both are legal-looking messages. Both will receive responses.

Failure. Two ownership transitions for one line, resolving in an order neither the device nor the host controls:

• Both may believe they succeeded. The line's state is written twice, and the second write reflects a grant that was computed against a state that no longer applies.
• The responses may be matched to the wrong transaction. If the identities differ but the line is the same, the state update from transaction A may be applied while transaction B's is in flight, leaving the line in a state neither requested.
• The device may end up believing it has write ownership it was never granted, which is §13's two-writer outcome by a different route.

And it directly violates a published restriction. The specification says multiple Evicts to the same line are not allowed and states exactly when a second may be issued. A design that issues two is not making an aggressive performance choice; it is non-conformant, and the far side is entitled to behave in ways the design has no model for.

Why it survives testing. With a large address space and random stimulus, two concurrent transactions to the same line is a rare event. The bug is a function of address-space locality in the stimulus, not of the design, so it is invisible until the workload has locality — which every real workload does.

// Illustrative — at most one transaction per line. Written as a pairwise
// property over the table because that is what "at most one" means here.
property p_one_txn_per_line;
  @(posedge clk) disable iff (!rst_n)
    (coh_txn_q[a].valid && coh_txn_q[b].valid && (a != b))
      |-> (coh_txn_q[a].line_addr != coh_txn_q[b].line_addr);
endproperty
a_one_txn_per_line: assert property (p_one_txn_per_line);
 
// And the same-line match vector, at issue, must be at most one-hot-zero —
// the same argument as Chapter 11.2 §9, applied to lines instead of windows.
property p_same_line_at_issue;
  @(posedge clk) disable iff (!rst_n)
    coh_txn_alloc_fire |-> $onehot0(same_line_vec);
endproperty

On generating the pairwise assertion. In practice this is elaborated with a generate loop over a and b, which produces MAX_COH_TXN × (MAX_COH_TXN−1) / 2 properties. For a small table that is fine. For a large one, the affordable equivalent is to assert $onehot0(same_line_vec) at every allocation, which catches the same bug at the moment it is introduced rather than continuously — and costs one property.

17. Probes, and What They Oblige

A probe is a request from the host about a line the device may hold. What the device owes in response is where coherence stops being bookkeeping.

The design consequence. The probe handler's answer is a function of two things: which probe it is, and what state the line is in including transient states. That is a two-dimensional table, and it is the state space §11's DV note asked you to cover.

The C_MODIFIED row is the essence of coherence. Memory does not have the current value. If the device does not supply it, the requester reads memory and gets a stale value, and nothing anywhere reports an error.

18. Wrong RTL — a Probe That Only Reads Stable State

// WRONG — the probe response is computed from a stable-state assumption.
always_comb begin
  probe_rsp_has_data = (meta_q[idx].state == C_MODIFIED);
  probe_rsp_next     = C_INVALID;
end

Architecture. The handler asks "am I modified?" rather than "do I hold the only current value?" Those differ precisely in the transient states.

Failure. A line in C_X_TO_I — the device is voluntarily giving it up — still holds modified data until the transfer completes. A probe arriving in that window is answered with no data, because the state is not literally C_MODIFIED. The host then reads memory. Memory is stale. The requester receives the old value.

The value is well formed. The link is clean. The probe was answered promptly and with a legal response. And the answer was a lie about the state of the world.

The second failure in the same code. probe_rsp_next = C_INVALID unconditionally means a SnpCur-shaped probe — which the specification says need not change the line's state — destroys a perfectly good copy. That one is only a performance bug, but it is a large one: a workload with a read-mostly shared structure will lose its copies continuously and refetch them, and the symptom is that coherence "works" and is inexplicably slow.

The right shape is §12's branch, which computes both the data obligation and the next state from the full state including transients.

DV. Probe every state. The transient rows are the ones a stable-state testbench cannot generate, which is why §32's stimulus must be able to inject a probe while a transaction is open.

19. The Race the Specification Has a Field For

The highest-value section in this chapter, because it is a race the specification anticipated, named, and required the device to track — which means it is a race that will occur, and a design that has not planned for it is wrong rather than merely lucky.

// Illustrative device-side handling of the snoop-versus-eviction race. The
// REQUIREMENT to track the hit and to mark subsequently-sent evict data as
// stale is verified specification behaviour (above); the signal names, the
// table structure, and the pulse shapes are illustrative.
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    for (int t = 0; t < MAX_COH_TXN; t++) coh_txn_q[t].probe_seen <= 1'b0;
  end else begin
    // Record the hit at the moment it happens. NOT when the pull arrives —
    // by then the information no longer exists anywhere.
    if (probe_hits_open_evict) coh_txn_q[evict_txn_idx].probe_seen <= 1'b1;
 
    if (evict_txn_retire) coh_txn_q[evict_txn_idx].probe_seen <= 1'b0;
  end
end
 
// When the eviction's data is finally sent, it must be marked stale if a probe
// took the line's data first. One bit, computed from state recorded earlier.
assign evict_data_is_stale = coh_txn_q[evict_txn_idx].probe_seen;

Architecture. One bit per open transaction, set by a different event source than the one that reads it — which is exactly why §12's single-writer discipline matters here too.

State. Per-coherence-transaction. It must be recorded at the moment of the probe, because the probe handler runs, completes, and leaves no trace otherwise.

Cycle behaviour. Set on the probe hit. Read when the eviction's data is sent, which may be many cycles later. Cleared with the transaction.

Contract. The far side relies on stale eviction data being marked so it can be discarded. If it is not marked, the host cannot distinguish the two copies and may keep the wrong one.

Failure — and this is a data-corruption failure with a clean link. The eviction's stale data is accepted as current, overwriting the fresher data the snoop already delivered. A write is silently lost. Every message was well formed; one of them was unmarked.

DV. This is a directed test. Issue an eviction of a modified line, then inject a probe to the same line before the data pull, then complete the eviction, and verify the stale marking. Random stimulus produces this alignment approximately never.

20. Metadata Correctness Is Not Data Correctness

A short section that reframes everything before it.

Suppose the state machine is perfect. Every transition legal, every probe answered correctly, every transient state represented. The system can still return stale data, because state says who may act, and data says what is true.

The worked example, and it is the whole of coherence in six lines:

1. Memory at address X holds 0.
2. The device obtains write ownership of X.
3. The device writes 1 locally. Its copy is C_MODIFIED and dirty.
4. Memory still holds 0. Nothing has been written back, and nothing should have been.
5. The host requests X.
6. If the request is served from memory, it returns 0. The value is stale, the state machines are all correct, and no error is reported anywhere.

The specification is explicit about the obligation that prevents step 6 — a device receiving SnpData must return dirty data to the host — and about the corresponding rule for grants: a response granting the device the sole copy of modified data means the device must cache this data and write it back when it is done.

Coherence state determines permission. Data ownership determines truth. A design can get the first entirely right and still be wrong.

This is why §36's reference model must track a value per line and not merely a state per line, and it is why Chapter 11.1 §23's claim — that assertions prove internal consistency and only a system model proves agreement — is not a hedge.

21. Worked Trace — a Host Write Invalidates the Device's Copy

Illustrative timing; generic action names. What matters is which state exists in each row.

Initial condition: the host and the device both hold X readable. The device's line is C_SHARED, clean.

Four things to read off it.

Step 3 is where the device stops being allowed to read, and it is before the state changes. probe_pending is what makes that expressible. A design without it serves reads through steps 3 and 4 from a copy whose invalidation is already committed — §9's bug, arriving via a different route.

Step 5's response is what makes step 7 safe. The host does not write until it knows the device's copy is gone. The specification's rule that no grant is sent to a device for an address until the snoop response and all implicit writeback data have been received is what enforces this.

Step 8 is a transient state on a line that holds nothing. The device has no data and no permission, and a probe arriving here needs an answer that says exactly that — §17's table.

Step 9 completes with a different value than step 1 had. That is coherence working. The device did not detect a change; it lost its copy and refetched, and the protocol arranged for the loss.

22. Worked Trace — the Device Holds Dirty Data and the Host Wants It

The reverse direction, and the one where the device's obligation is load-bearing.

Initial condition: the device holds X in C_MODIFIED, dirty, value 1. Memory holds 0.

Step 1 is the row worth staring at. A read of memory at this instant returns the wrong value, and this is a correct state of the system. Memory being stale is not a bug; it is the normal condition whenever any agent holds modified data. Coherence exists to make sure nobody reads memory in that situation without asking first.

Step 3 is the obligation. The specification's requirement is direct — if the device holds dirty data it must return it. This is the single obligation whose omission produces the classic stale read, and it produces it silently.

Step 4 is where a design can lose data in two different ways. Responding without the data loses the write. Responding with the data but also keeping the line dirty risks writing it back later over something newer — which is what §19's race is about in its eviction form.

23. Two Completion Points, Not One

A subtlety with direct consequences for both the RTL and the scoreboard, and it is stated in the specification.

For a CXL.cache write the specification says the transaction is considered complete by the device once the device has received the Global Observation response and has sent the required data messages — at which point the device's entry can be de-allocated. And that the host considers the write done once it has received all 64 bytes of data and has sent the GO response.

Those are different moments. They must be, because each party's condition includes something it can only observe locally.

Three consequences.

The RTL must not free a transaction entry on one condition. Both the response and the data transfer must have happened. A design that de-allocates on the grant alone frees an entry whose data has not been sent — and the entry may then be reused while the old transaction's data is still in flight.

The scoreboard must pick a point and be explicit about it. Chapter 11.2 §30 made this argument for memory writes; here the two candidate points are further apart and there are two parties, so an implicit choice produces failures whose only cause is the model's own ambiguity.

The two parties' views of "outstanding" legitimately differ for an interval. Any check that compares the device's open-transaction count against the host's must account for that skew, or it will report a mismatch that is not one.

The specification also states the ordering constraint that pairs with this: for a write, the grant must never arrive at the device before the data pull, though the two may arrive together in a combined message. An implementation that can present them in the other order is not making a scheduling choice; it is producing a sequence the far side is entitled to treat as impossible.

24. Ordering Is the Device's Problem

A rule that is easy to get backwards, and the specification states it plainly.

The Host will NOT preserve ordering of the CXL.cache requests as delivered by the device. The device must maintain the ordering of requests for the case(s) where ordering matters.

And the same-address restrictions repeat it for reads and for writes: multiple requests to one line are allowed, the host can freely reorder them, and the device is responsible for ordering when required.

What this means for a design. Issuing two requests in order buys nothing. If the device needs A to be observed before B, the device must not issue B until A has reached whatever point makes that true. The ordering must be enforced by issue control, not by transmission order.

The specification also describes how the chosen order is conveyed back, which is the detail that makes the mechanism usable: for reads, the Global Observation response conveys next ownership of the line while the data message conveys ordering with respect to other transactions; for writes, the GO conveys both.

And the transport layer beneath cannot help. UCIe delivers what it is given. If the device relies on transmission order for correctness, and the mapping layer or the host reorders — both permitted — the failure is in the device.

Why this catches people. Every bus this curriculum has covered so far had some ordering guarantee to lean on. This one explicitly does not, and the burden is placed on the agent that is easiest to write incorrectly.

25. Transport Retry Must Not Duplicate a Coherence Action

Chapter 10.2 §9 established the rule for PCIe transactions. Here the same rule has worse consequences, and it is worth being specific about why.

// WRONG — semantic coherence action driven by transport arrival.
assign probe_process = flit_received && flit_crc_ok && (flit_class == CLASS_PROBE);

A UCIe retry occurs when a flit is corrupted — and also when a confirmation is lost, in which case the original arrived perfectly and the receiver sees the same transport object twice (Chapter 9.4 §12). With processing keyed on arrival, the device processes the same probe twice.

Why a duplicated coherence action is worse than a duplicated data transaction.

A duplicated memory write corrupts one location. A duplicated coherence action corrupts distributed state, and the corruption then affects every future access to that line:

• A probe processed twice may generate two responses. The host receives an answer to a snoop it is not tracking, which — given the specification's rule that only one snoop per line per device may be outstanding — is a response the host has no context for.
• The second processing sees a different state than the first. The line was invalidated by the first pass, so the second answers "no copy found" — which is true but is being reported for a transaction that already completed differently.
• A duplicated ownership grant may be applied twice, and if the second application lands after a subsequent local transaction has begun, it overwrites that transaction's transient state — §13's failure with a transport cause.
• A duplicated eviction may double-count the transaction table, leaking an entry or freeing one twice.

None of this produces a link error. The transport did exactly what it was designed to do.

// Illustrative — semantic processing gated on transport RESOLUTION plus
// duplicate suppression, never on arrival. Requires an identity the receiver
// can use to recognise a repeat (Ch 9.4 §12).
assign probe_process = probe_obj_complete        // fully reconstructed
                    && !probe_obj_is_duplicate   // this transport object is new
                    && probe_order_ok;           // §24 — dependencies satisfied

And the layering rule that follows. The suppression belongs below the coherence engine and above the transport, in the mapping layer — which is Chapter 11.4's subject. A coherence engine that has to defend itself against duplicates has been handed a problem that is not its own, and it will get it wrong, because it has no visibility into transport identity.

// Illustrative — one semantic coherence action per accepted request. Uses a
// VERIFICATION-ONLY monitor tag allocated by the testbench, not a protocol field.
property p_one_semantic_action_per_request;
  @(posedge clk) disable iff (!rst_n)
    coh_action_fire |-> !action_done_mon[coh_mon_tag];
endproperty
a_one_semantic_action_per_request: assert property (p_one_semantic_action_per_request);

26. Recovery With Coherence Transactions Outstanding

The hardest problem in the chapter, and the one where the honest answer is a design requirement rather than an algorithm.

A UCIe link enters recovery, or fails, while an ownership transfer is in flight.

Why the memory-expansion answer does not work here. Chapter 11.2 §17 could say: hold the outstanding entry, and either the recovery completes and the read finishes, or an explicit error path resolves it. That works because a memory read is a request for a value and the value either arrives or does not.

An ownership transfer is not a request for a value. It is a change to state that both parties hold. So the questions multiply:

• Did the far side observe the request? If it did, it may already have invalidated another agent on the strength of it.
• Did the far side send a grant that was lost? If so, ownership has been transferred and only one party knows.
• Did a probe response get lost? Then the host may be waiting on a snoop it will never see resolved, and by its own rules it cannot issue another snoop to that line.
• Was dirty data in flight? Then the only current copy of a line may be in a buffer that a reset is about to clear.

None of those can be answered locally, and that is the point:

Coherence recovery is a distributed-state problem. Whether a coherence transaction took effect is not knowable from one side of a link that just failed.

What the architecture must therefore define, in advance:

Which states may survive a recovery, and which must not. Stable line states describing lines with no transaction in flight are per-cache-line state and have no reason to be affected. Transient states are the problem.

What resolves a transaction whose outcome is unknown. This must be an explicit, defined path. The specification and the platform define error-reporting and containment behaviour for unrecoverable conditions; this chapter does not restate their mechanisms, and inventing a resolution flow would be exactly the fabrication §2 forbids.

Whether dirty data can be lost, and if not, what protects it. If a line's only current copy is held by the device and the transaction that was transferring it has failed, the value must either survive to be transferred later or the failure must be escalated as a data-integrity error rather than silently dropped. The specification provides containment concepts — a Poison indication described as marking data that is corrupted and must not be used, and a viral-error concept — and the existence of those mechanisms is the clue: the architecture's answer to "coherence broke" is usually to contain and report, not to guess.

27. Why a Timeout Cannot Restore the Previous State

The specific wrong answer this section exists to prevent, because it is the intuitive one.

A coherence transaction has not completed. A timeout fires. The tempting recovery:

// WRONG — and dangerously plausible.
always_ff @(posedge clk) begin
  if (coh_txn_timeout[t]) begin
    meta_q[line_of(coh_txn_q[t].line_addr)].state <= C_SHARED;  // "put it back"
    coh_txn_q[t].valid <= 1'b0;
  end
end

Why it is wrong. The timeout says no response arrived. It does not say nothing happened. Those are completely different facts, and the second cannot be inferred from the first.

Enumerate what may actually have happened while the timeout was counting:

Three of four cases produce a device whose state contradicts the host's. And because the state now looks stable, every subsequent check passes: the pairing invariants hold, the transient-state assertions hold, the line is readable and clean. The design has laundered an unknown into a confident wrong answer.

A coherence timeout is an error condition to be contained and reported, not a state to be recovered from by guessing.

What a defensible timeout handler does instead. It marks the line as unusable rather than as any stable state, refuses to serve accesses to it, records the event in diagnostic state that survives reset, and escalates through whatever error path the architecture defines. That is less satisfying and it is correct. Making the failure visible is the whole objective, because the alternative — a silently inconsistent distributed state — is the one bug class this curriculum has repeatedly shown that nothing downstream can detect.

28. Deadlock, and the Structure That Prevents It

Coherence protocols deadlock. This is not a hypothetical risk; it is the reason the channel structure looks the way it does, and the specification's own classification tells you exactly which dependencies are forbidden.

Now the deadlock, and why the structure prevents it.

The dangerous cycle in any coherence protocol is:

1. The device's probe response cannot be sent because a shared queue is full of the device's own outgoing requests.
2. Those requests cannot drain because the host will not accept more until it has resolved the line whose probe it is waiting on.
3. The host is waiting for the probe response from step 1.

A closed cycle. No message is corrupted, no state is wrong, nothing times out for a long while, and the system has stopped.

The structure that prevents it is exactly the specification's classification: because response and data channels are pre-allocated, step 1 cannot happen — the response has a reserved destination and does not compete with requests for it.

Which makes the implementation rule sharp:

A design that merges the response path into the request path, or shares a buffer between them, destroys the property that makes the protocol deadlock-free — and no assertion on either channel will notice.

// WRONG — one queue for everything the device sends. Individually reasonable,
// architecturally fatal: a full queue of outgoing requests now blocks the
// probe response that would let those requests drain.
assign d2h_out_ready = shared_out_queue_space;

// Illustrative — the response and data paths have their own reserved capacity,
// so an outgoing-request backlog cannot block them. The structural expression
// of the classification above.
assign d2h_req_ready  = req_queue_space;    // may block indefinitely — allowed
assign d2h_rsp_ready  = rsp_queue_space;    // reserved; must drain
assign d2h_data_ready = data_queue_space;   // reserved; must drain
 
// And the invariant that says the reservation is real: a probe that has been
// recorded must always have somewhere to put its response.
property p_response_capacity_reserved;
  @(posedge clk) disable iff (!rst_n)
    probe_recorded |-> (rsp_queue_space != '0);
endproperty
a_response_capacity_reserved: assert property (p_response_capacity_reserved);

Note what p_response_capacity_reserved is. It is not a CXL requirement; it is the local expression of the design decision that makes the CXL classification implementable. Which is the pattern to internalise from §2's sourcing rule: the specification tells you the property; your RTL's assertion says how your design achieves it.

29. Safety and Liveness Are Different Failures

A distinction this chapter cannot end without, because the two need different verification and produce different symptoms.

Safety properties say nothing bad happens.

• No two agents hold write ownership of one line simultaneously.
• No access is served from a line the device is not permitted to use.
• Dirty data is never discarded without being transferred or explicitly reported as lost.
• At most one ownership-changing transaction is open per line.

Liveness properties say something good eventually happens.

• An ownership request eventually completes, under fair environment assumptions.
• A recorded probe is eventually answered.
• A transient state is eventually left.

Why the split matters practically. Chapter 5.5 §12 made the general argument and it lands hardest here: every safety assertion in this chapter passes during a deadlock. Nothing bad is happening. Nothing at all is happening. A regression whose pass criterion is "no assertion fired" reports a deadlocked coherence protocol as a pass, until a timeout somewhere else eventually kills the test — and the timeout will point at whatever was unlucky enough to be waiting, not at the cycle in §28.

// Illustrative safety properties. LOCAL invariants for THIS model, not CXL
// requirements — §2's rule, applied.
 
// Dirty data is not discarded silently. If a dirty line leaves a state that
// holds the only current value, either a transfer was issued or the design
// explicitly reported the loss.
property p_dirty_not_silently_dropped;
  @(posedge clk) disable iff (!rst_n)
    (meta_q[idx].dirty && (next_state == C_INVALID))
      |-> (data_transfer_issued || dirty_loss_reported);
endproperty
a_dirty_not_silently_dropped: assert property (p_dirty_not_silently_dropped);
 
// A transient state is never skipped: a line cannot go from INVALID straight
// to a writable state without a transaction having been open.
property p_no_transient_skip;
  @(posedge clk) disable iff (!rst_n)
    ((meta_q[idx].state == C_INVALID) && write_allowed(next_state))
      |-> meta_q[idx].txn_pending;
endproperty
a_no_transient_skip: assert property (p_no_transient_skip);

// Illustrative liveness, and the honesty is the point. This is a BOUNDED
// progress check, not a true liveness proof, and the bound is an engineering
// choice rather than a protocol value.
//
// ASSUMPTIONS, which must be stated or the property is meaningless:
//   - the transport is operational for the whole window
//   - the far side is responding to other traffic
//   - no error injection is active
property p_probe_eventually_answered;
  @(posedge clk) disable iff (!rst_n || error_injection_active)
    probe_recorded |-> ##[1:MAX_PROBE_LATENCY] probe_answered;
endproperty
a_probe_eventually_answered: assert property (p_probe_eventually_answered);

On the single-writer property, and why it is honest to say it cannot live here. "No two agents hold write ownership of one line" is the most important safety property in coherence, and it cannot be expressed at one agent's interface, because the other agents' state is not visible there. It belongs to a system-level model (§36) or to a formal model of the whole protocol. Writing it as a local assertion produces something that looks like the real property and checks something much weaker — which is worse than not writing it, because it creates the belief that the property is covered.

30. The Coherence Scoreboard

The strongest verification section in the batch, and the one whose absence lets every bug in this chapter ship.

per cache line (the model's own view of truth):
  latest_value       — the authoritative current value, from global history
  owner              — which agent, if any, holds write ownership
  sharers[]          — which agents may hold a readable copy
  dirty_at           — which agent holds data that memory does not have
  pending_txn[]      — coherence transactions in flight for this line
  pending_probe      — a probe outstanding to this line, and to which agent
 
per agent:
  observed_reads[]   — every value this agent actually read, in order
  issued_writes[]    — every value this agent actually wrote, in order
  line_state[]       — what the model believes this agent's metadata says
 
per coherence transaction:
  mon_tag            — VERIFICATION-ONLY identity, allocated by the testbench
  line, initiator, target_state, issue_time
  semantic_actions   — how many times this was acted upon (must be exactly 1)

The checks, and what each one uniquely catches.

Every read returned a value the agent was permitted to observe, given the true history of the line and the ordering rules in force. This is the only check that catches the stale-read family — §18's missing data obligation, §9's stale shadow copy, and §20's memory-versus-owner error. No assertion at any agent's interface can see it, because locally nothing is wrong.

No two agents hold write ownership at once. §29's uncheckable-locally property, checkable here because the model sees every agent. This catches §13 and §16.

Every agent's metadata matches the model's belief, compared at quiescent points. Divergence is caught when the state diverges rather than when a stale read eventually results — which may be thousands of cycles later, or never in simulation and immediately in silicon.

Dirty data is never lost. If the model says an agent holds the only current value, then that value must appear — supplied to a requester, written back, or explicitly reported as lost. This catches §26's recovery hazard and §19's unmarked-stale-data case, both of which are silent write losses.

Each coherence transaction was acted upon exactly once. The semantic_actions counter, keyed by the verification-only tag. This catches §25's duplicate, and note that the design has no field with which to check this itself — the tag exists precisely because the protocol identity is reused and the transport identity is invisible.

At most one ownership-changing transaction per line, and at most one probe. The model enforcing §15's published restrictions from the outside, which catches a design that violates them even if the far side happens to tolerate it.

Every transaction reached a defined resolution. End-of-test check. This is what fires on §27's timeout handling if it silently invented a state, because the model will show a line whose ownership history has a gap.

On what the model must not do. It must not compute anything by calling the design's functions, reading its state array, or reusing its permission predicates. A model that shares read_allowed() with the DUT agrees with it about which transient states are readable, which is §8's bug. The model's job is to be an independent opinion, and sharing code with the thing you are checking converts it into an echo.

31. Why a Packet Scoreboard Passes While the System Is Corrupt

Worth stating as its own section because it is the argument for building §30 at all, and it is the argument people push back on.

Consider a regression with a complete, correct transport model. It checks:

• every flit's CRC passed, or a retry recovered it;
• every credit was conserved;
• every message that was sent was delivered;
• every message that was delivered was well formed;
• no ordering the transport was required to preserve was violated.

All of that can pass while the system computes on values that are not true.

Take §13's bug — a probe and a grant landing in the same cycle, with the grant winning. Every message involved was well formed, delivered exactly once, and answered legally. The probe response the host received was a valid response. The grant the device applied was a valid grant. The transport model sees a perfect link, because the link was perfect. The fault is that two correct messages were applied to one piece of state in an order nobody defined, and the result is two write owners.

Or take §18's — a probe answered without data because the state was transient rather than literally modified. The response was legal. The host proceeded correctly on the information it was given. A memory read then returned a stale value, and the only party that knew the truth had just said it did not have it.

A completely clean transport scoreboard is entirely consistent with total coherence failure. If a regression's pass criterion is "transport clean, no protocol errors, no assertion fired", it will pass with every bug in this chapter in it.

The corollary is uncomfortable and worth accepting early: the coherence model is not an optional refinement of the transport model. It is the only thing checking the property the system exists to provide.

32. Coverage

// Illustrative coverage for a device coherence agent. Not CXL-defined. Every
// bin exists to reach a specific bug named in this chapter.
covergroup cg_cxl_coherence @(posedge clk iff coh_event);
 
  // Every state, stable AND transient (§11).
  cp_state      : coverpoint meta_q[idx].state;
  // Every incoming event class.
  cp_event      : coverpoint coh_event_class {
    bins local_rd = {EV_LOCAL_RD};  bins local_wr = {EV_LOCAL_WR};
    bins probe    = {EV_PROBE};     bins grant    = {EV_GRANT};
    bins data     = {EV_DATA};      bins evict    = {EV_EVICT};
  }
  cp_probe_kind : coverpoint probe_kind;          // §17 — each obligation shape
  cp_dirty      : coverpoint meta_q[idx].dirty;
  cp_txn_occ    : coverpoint coh_txn_occupancy {
    bins none = {0}; bins some = {[1:$-1]}; bins full = {MAX_COH_TXN};
  }
  cp_same_line  : coverpoint same_line_conflict_kind {
    bins none            = {0};
    bins txn_vs_txn      = {1};   // §16
    bins probe_vs_txn    = {2};   // §19
    bins probe_vs_probe  = {3};   // forbidden by §15 — must be UNREACHED
  }
  cp_order      : coverpoint data_perm_arrival_order {
    bins data_first = {0};        // §10 — the legal case people forget
    bins perm_first = {1};
    bins same_cycle = {2};
  }
  cp_retry      : coverpoint transport_retry_during_txn;   // §25
  cp_recovery   : coverpoint recovery_with_transient_line; // §26
 
  // THE cross that matters: every event, in every state. This is the real
  // state space, and the transient rows are where the bugs are.
  x_state_event    : cross cp_state, cp_event;
  // A probe in every state, including transient ones — §17's table, executed.
  x_state_probe    : cross cp_state, cp_probe_kind;
  // Probe and local activity colliding on one line at every occupancy — §13.
  x_conflict_occ   : cross cp_same_line, cp_txn_occ;
  // A transport retry while a line is transient — §25 with §11 in play.
  x_retry_state    : cross cp_retry, cp_state;
  // Recovery with a dirty transient line — §26's worst case.
  x_recovery_dirty : cross cp_recovery, cp_dirty;
 
endgroup

Three notes on this covergroup, because the bins encode arguments.

x_state_event is the coverage model. Everything else is a refinement of it. If a regression covers every state crossed with every event class, it has reached the situations the protocol guarantees will occur; if it covers only the stable rows, it has verified a private cache.

cp_same_line has a bin that must stay at zero. probe_vs_probe is forbidden by §15's published restriction. Covering it would mean the environment is generating illegal stimulus — so it is a bin whose value is that it never fills, and that is worth writing down rather than leaving as an assumption.

cp_order exists because of §10. Data arriving before permission is legal and is the case a naive testbench never produces, because a naive testbench sends the response and the data together. It must be a deliberate stimulus mode.

And the stimulus requirement that all of this implies: a small address footprint. Same-line conflicts, probe-versus-transaction races, and repeated ownership transfers are all functions of address locality. A random test over a large address space produces almost none of them, which is exactly why coherence bugs survive large regressions and fail in workloads.

33. Diagnostic Taxonomy

The first and sixth rows are the pair to internalise. They are the two most serious failure classes, they have nothing in common, and neither produces evidence at the layer engineers habitually inspect first. One is silent wrong data; the other is silence itself.

34. Debug Checklist

1. Which cache line failed? Everything else is downstream of getting this right.
2. What does the reference model say the owner and value were? §30 — without this, step 3 has nothing to compare against.
3. What did the device's metadata say? State, dirty, and both pending bits.
4. Was the line stable or transient at the moment of failure? §11 — this splits the investigation in half.
5. Was a coherence transaction open on that line? §14 — and how many.
6. Had a probe arrived and not yet been answered? §19 — probe_pending is the field that records it.
7. Did a probe and a local event land in the same cycle? §13 — the single highest-yield question in this list.
8. Which event won, and was that the stated priority? §12 — compare against the policy, not against intuition.
9. Did the line hold dirty data, and was it transferred? §20 — a missing transfer is a silent lost write.
10. Did data arrive before permission? §10 — legal, and a design that mishandled it looks like a state-machine bug.
11. Did a transport retry or recovery occur during the transaction? §25 and §26.
12. Was any semantic action performed twice? The verification-only tag counter in §30.
13. Did a state transition happen before the response that authorised it completed? §23's two completion points.
14. Is the failure safety or liveness? §29 — if nothing is moving and nothing has fired, stop looking for a wrong value and start looking at §28's dependency cycle.
15. Did the transport model or the coherence model diverge first? The question that routes everything: a clean transport model with a diverged coherence model puts the bug in the agent or the mapping, never in the link.

35. Common Misconceptions

"Coherence means every cache always has current data." It means no agent ever observes a stale value. Memory is routinely stale — whenever any agent holds modified data (§20) — and coherence exists to ensure nobody reads it in that state without asking.

"MESI state names are enough to implement CXL.cache." The specification's own Global Observation description does refer to the cache line state permitted through MESI state, so the vocabulary is not wrong. What is wrong is thinking the stable states are the state space. The protocol guarantees intervals in which data has arrived and permission has not (§10), and in which a probe has hit a line whose eviction is in flight (§19) — and neither is a MESI state.

"A tag hit means the data may be used." A tag hit says the data is in the array. Permission is a separate question answered by the metadata, and forgetting to ask it is the most consequential single line in the chapter (§8).

"Transient states are an optional implementation detail." The specification requires that a device track a snoop that hits a pending eviction, and permits data to precede permission. Both are situations a stable-state-only design cannot represent (§10, §19).

"Two requests to the same line can be handled independently." Multiple Evicts to one line are explicitly not allowed, and only one snoop per line per device may be outstanding. Reads and writes to one line are allowed concurrently — with the ordering burden explicitly placed on the device (§15, §24).

"Probe handling and local completion can update state in separate if-statements." Then the last assignment wins, the order depends on how the file was typed, and a probe-plus-grant collision produces two write owners with no error anywhere (§13).

"Transport CRC correctness proves coherent correctness." A clean transport scoreboard is entirely consistent with total coherence failure, and §31 works through two specific bugs that produce a perfect link and wrong data.

"A timeout can safely restore the previous stable state." A timeout says no response arrived, not that nothing happened. Three of the four things that may actually have happened leave the device contradicting the host — and because the invented state looks stable, every subsequent check passes (§27).

"A UCIe replay may be treated as another coherence request." Then a probe is processed twice, or a grant applied twice, and the corruption is to distributed state rather than to one location (§25).

"Coherence verification is packet matching with extra steps." It is comparison against an independently maintained model of value, owner, sharers, and pending transactions per line. The checks that matter — permitted observation, single write owner, dirty data not lost — are not expressible at any one agent's interface (§29, §30).

"Deadlock is prevented if all the counters are in range." Deadlock is a cyclic dependency, and every safety assertion passes during one. The property that prevents it in CXL.cache is that response and data channels are pre-allocated and must make progress, and a design that shares a buffer between response and request paths destroys it without violating any counter bound (§28).

"The device can rely on issuing requests in order." The specification states that the host will not preserve the order of CXL.cache requests as delivered by the device, and that the device must maintain ordering where it matters (§24).

36. Understanding Check

37. Summary and What Comes Next

Coherence is distributed ownership tracking, and the state that makes it work is mostly the state that exists while ownership is changing.

The architecture: three channels in each direction, with the Home Agent resolving system-wide coherency and the DCOH resolving it for device caches — and a forward-progress classification in which requests may block indefinitely while responses and data are pre-allocated and must make progress, which is the property that keeps the protocol deadlock-free. Plus a revision boundary that cannot be papered over: enhanced coherency replaced bias-based coherency in CXL 3.0, changing which direction a snoop may travel.

The mechanisms: a tag hit is not permission, and the version of that bug that ships is a permission check reading a state copy one cycle stale. Transient states are required, not prudent — the specification permits data to arrive before the permission that says what to do with it, and requires the device to track a snoop that hits a pending eviction. One state writer with one stated priority, because a probe and a grant landing together with two writers produces two write owners and no error anywhere. At most one ownership-changing transaction per line, which is a published restriction rather than a design preference. Dirty data must be supplied when probed, because memory is routinely stale and that is a correct state of the system. And the device owns its own ordering, because the host explicitly does not preserve it.

The two failures to recognise on sight: stale data with a clean link, which no assertion at any interface can see, and silence — a channel dependency cycle through which every safety property passes.

The rule that keeps recovery honest: a timeout is an error to contain and report, not a state to guess. Three of the four things that may have happened leave the device contradicting the host, and the invented state looks stable enough that every later check agrees with it.

And the verification conclusion: a clean transport scoreboard is entirely consistent with total coherence failure. The coherence model — value, owner, sharers, and pending transactions per line, computed independently — is not a refinement of the transport model. It is the only thing checking the property the system exists to provide.

Memory semantics and coherence semantics are now both understood as semantics: obligations about what an agent may observe and what it owes. What has been assumed throughout is that those semantics arrive at the far die intact, exactly once, in an order the protocol permits. That assumption is a whole layer's worth of work:

• 11.4 — CXL Transport on UCIe — tunnelling CXL flits through the UCIe stack.

Browse the full path on the UCIe tutorials index.