Coherent Communication Model

Chapters 3.1 to 3.3 described where things are. None of them described what the host and the device actually say to each other when a single line of memory has to stay correct across both.

This chapter is that conversation, and it starts as small as it possibly can.

1. The Engineering Problem — One Line, Two Wishes

Forget protocols. There is one 64-byte line at physical address X.

   CPU cache      holds a copy of X, and has modified it
   Device         wants to write X

Two questions follow, and every coherence mechanism in existence is an answer to them:

Who has the authoritative value of X?

Who is allowed to change it?

Notice that the first question has a surprising answer. Memory does not have the authoritative value — the CPU modified its copy, so memory holds a value that used to be correct. Anything that reads memory to answer "what is at X" gets the wrong answer, with no error, no exception, and nothing in the returned data marking it as old.

And the second question has a subtle one. If the device is allowed to write, then the CPU's copy must stop being readable — otherwise two agents disagree about the same address. But the CPU cannot be told to stop instantaneously. There is a gap between asking it to stop and knowing it has stopped, and what happens in that gap is where coherence bugs live.

2. The One-Sentence Model

Coherence is a negotiation with one arbiter: every line has a single agent that serialises requests to it, knows which caches hold copies, invalidates them before granting a writer, and returns the authoritative value from whichever cache holds it rather than from memory — and none of that can be skipped, because each step exists to close a window in which two agents would disagree.

3. What This Chapter Owns

Chapter 3.1 built a home agent as a structure. This chapter is about the conversation it conducts — including the parts that structure did not cover: where data comes from, how conflicts are deferred rather than refused, and what a missing response does.

4. Vocabulary — Architectural, Not Protocol

These words are used loosely in industry discussion. Fixing them is worth a section, and the distinction from CXL's own message names matters.

5. The Mental Model — Home Is a Serialisation Point

The picture to carry:

        requester ──ask──►  ┌────────┐
                            │  HOME  │  ◄── knows: owner, sharers, dirty
        requester ──ask──►  └────────┘
                                │
                          snoop │ ▲ response
                                ▼ │
                        ┌───────────────┐
                        │ caches holding │
                        │ copies of X    │
                        └───────────────┘

Home is not a router and not an arbiter — it is a serialiser. The difference matters. A router forwards. An arbiter picks a winner and the loser goes away. A serialiser picks an order and the loser waits, which is why Section 10's model has a deferred set and not just a grant.

6. Asymmetry — Why the Host Orchestrates

The Consortium's phrasing — the host processor orchestrating the coherency management — describes an asymmetric model, and the CXL 2.0 material is explicit about the design intent, listing "Simple coherency flows for device w/ asymmetry" as easing adoption.

Read as a hardware statement, asymmetry means the two ends are not peers:

The device's coherence obligation is a short list: hold copies correctly, and answer snoops promptly. It does not need to know what other agents exist, which is the same information argument Chapter 3.1 made and the reason the device cannot be the coherence point.

Why asymmetry was the right call is an adoption argument, not a purity argument. A symmetric protocol requires every participant to implement the full coherence engine, which is a large, subtle block that must interoperate with every other vendor's version of it. Asymmetry concentrates that difficulty on the host — where it already existed, because CPUs have had coherence engines for decades — and leaves the device with the smaller half. That is why an accelerator team can add .cache without building a CPU's coherence logic.

The cost is that every coherence decision is a round trip to the host. A device cannot resolve a conflict locally even when both parties are on the same device, which is one of the pressures behind later peer-to-peer work. Chapter 2.3 noted that CXL 3.1 material describes adding a symmetric .mem link-layer definition for devices — evidence that the asymmetric choice was a starting point rather than a permanent constraint.

7. The Read Flow

Conceptually, and deliberately without protocol names:

1.  device asks home for a readable copy of X
2.  home consults the directory
3.  if a cache holds X modified, home snoops that owner
4.  the authoritative value comes from wherever it actually is
5.  home records the device as a sharer
6.  home completes to the device

Step 4 is the one people get wrong, and Section 12 measures it. If a cache holds X modified, memory is stale, so the value must come from that cache. A home agent that always reads memory returns a value that was correct at some point in the past.

Step 3 is conditional and step 5 is not. If nothing holds X modified, no snoop is needed and the read is cheap. That is why read latency to a coherent line is bimodal, and why an average hides the interesting behaviour.

8. The Write Flow

1.  device asks home for permission to modify X
2.  home consults the directory
3.  home snoops every agent holding a copy
4.  home WAITS for every response
5.  home records the device as owner and clears the sharers
6.  home completes to the device, which may now write

Step 4 is the whole difficulty. Between issuing the snoops and collecting the last response, the line is in a state where the old holders may still be serving reads and the new writer has not yet been permitted. Granting during that window is the defect Section 11 measures.

Steps 5 and 6 must be indivisible with respect to observers. If the sharers are cleared a cycle after the owner is installed, there is a cycle in which a writer and readers coexist — the single-writer invariant broken for exactly one cycle, which is enough.

9. RTL 1 — The Line Directory

Purpose

Decide what must be remembered, and refuse to remember something impossible.

// What the coherence authority remembers about ONE line.
//
// GENERIC pedagogical model. These fields are a teaching abstraction, NOT a
// CXL directory format, NOT MESI/MOESI state encoding, and NOT any
// specification-defined structure.
//
// The teaching point is which facts must be remembered at all:
//   valid       -- is anyone holding this line?
//   owner       -- who, if anyone, may write it
//   sharers     -- who holds a readable copy
//   dirty       -- is the authoritative value in a cache rather than memory?
//   in_transit  -- is a state change in progress right now?
module line_directory #(
  parameter int unsigned NAGENT = 4
) (
  input  logic              clk,
  input  logic              rst_n,
  input  logic              we,
  input  logic              w_valid,
  input  logic [NAGENT-1:0] w_owner,
  input  logic [NAGENT-1:0] w_sharers,
  input  logic              w_dirty,
  input  logic              w_transit,
  output logic              valid_q,
  output logic [NAGENT-1:0] owner_q,
  output logic [NAGENT-1:0] sharers_q,
  output logic              dirty_q,
  output logic              transit_q,
  output logic              two_owner_err,      // more than one writer
  output logic              owner_sharer_err,   // a reader coexists with a writer
  output logic              dirty_no_owner_err  // dirty with nobody holding it
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      valid_q <= 1'b0; owner_q <= '0; sharers_q <= '0;
      dirty_q <= 1'b0; transit_q <= 1'b0;
      two_owner_err <= 1'b0; owner_sharer_err <= 1'b0; dirty_no_owner_err <= 1'b0;
    end else begin
      if (we) begin
        valid_q   <= w_valid;   owner_q   <= w_owner;
        sharers_q <= w_sharers; dirty_q   <= w_dirty;
        transit_q <= w_transit;
      end
      // The three structural invariants, checked on the STORED state so a bad
      // write is caught even if the writer believed it was consistent.
      if ($countones(owner_q) > 1)              two_owner_err      <= 1'b1;
      if ((owner_q != '0) && (sharers_q != '0)) owner_sharer_err   <= 1'b1;
      if (dirty_q && (owner_q == '0))           dirty_no_owner_err <= 1'b1;
    end
  end
endmodule

dirty is a separate fact from owner, and that is the field people omit. Knowing who may write is not the same as knowing whether the current value has been written. A line can have an owner whose copy is still identical to memory — in which case memory is fine — and the same line can be owned and modified, in which case memory is wrong. Section 12 is entirely about that distinction.

in_transit exists so home can refuse. Without it there is no way to express "a change is happening, come back", and every conflicting request has to be either granted or dropped. Section 10 uses it.

Checking the stored state rather than the write is deliberate. A writer that computed an inconsistent state believed it was consistent, so a check on the write inputs is a check by the same logic that made the mistake.

Simulation evidence

Two legal states, then the same three illegal ones into a directory with no checks:

=== EXP1: what the directory must remember, and what it refuses ===
  three readers      : owner=0000 sharers=0111 dirty=0  errors=000
  one dirty owner    : owner=1000 sharers=0000 dirty=1  errors=000
 
  -- the same three writes into a directory with no consistency checks --
  two owners         : owner=1010 -> two_owner_err=1
  owner AND sharers  : owner=1000 sharers=0011 -> owner_sharer_err=1
  dirty, nobody owns : owner=0000 dirty=1 -> dirty_no_owner_err=1
  -> each of these is a state the coherence model says cannot exist

Each of those three is a representable state that the model forbids. That gap — between what the encoding can hold and what the architecture permits — is where coherence bugs are stored, and the three checks cost three comparators.

10. RTL 2 — Serialising a Conflict

Purpose

Two agents want the same line. Order them, and lose neither.

// Two agents want the same line. One proceeds; the other is DEFERRED, not
// refused -- deferral is what makes this serialization rather than arbitration.
//
// GENERIC teaching model. No CXL message, channel or ordering rule is modelled.
module conflict_serializer #(
  parameter int unsigned NAGENT = 4
) (
  input  logic              clk,
  input  logic              rst_n,
  input  logic [NAGENT-1:0] req,
  input  logic              line_busy,        // a state change is in progress
  input  logic              release_pulse,    // the in-progress change finished
  output logic [NAGENT-1:0] active_q,         // the one being serviced
  output logic [NAGENT-1:0] deferred_q,       // waiting their turn
  output logic              accept,
  output logic [7:0]        wait_q [NAGENT-1:0],
  output logic [7:0]        max_wait_q,
  output logic              lost_request_err, // a requester vanished from both sets
  output logic              double_active_err
);
  assign pending = deferred_q | req;
 
  // Rotating choice among everyone waiting, so no agent is starved on a hot line.
  always_comb begin
    pick = '0; found = 1'b0;
    for (j = 0; j < NAGENT; j = j + 1) begin
      k = (ptr_q + j) % NAGENT;
      if (!found && pending[k]) begin pick[k] = 1'b1; found = 1'b1; end
    end
  end
  assign accept = !line_busy && (active_q == '0) && found;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin /* ... */ end
    else begin
      if ($countones(active_q) > 1) double_active_err <= 1'b1;
 
      // A new requester that cannot be served right now is REMEMBERED.
      // Dropping it here is how a request silently disappears.
      deferred_q <= (deferred_q | req) & ~(accept ? pick : {NAGENT{1'b0}});
 
      if (accept) begin
        active_q <= pick;
        for (i = 0; i < NAGENT; i = i + 1) if (pick[i]) ptr_q <= i[1:0] + 2'd1;
      end else if (release_pulse) begin
        active_q <= '0;
      end
      // ... wait counters and max_wait_q ...
 
      // Anyone who asked must be either active or deferred on the next cycle.
      next_kept = (deferred_q | req) & ~(accept ? pick : {NAGENT{1'b0}});
      for (i = 0; i < NAGENT; i = i + 1)
        if (req[i] && !(accept && pick[i]) && !next_kept[i]) lost_request_err <= 1'b1;
    end
  end
endmodule

lost_request_err is the invariant that matters most here and the one that is hardest to check any other way. A coherence request that is neither served nor remembered does not produce an error anywhere — it produces a requester waiting forever for a completion that will never come, which surfaces as a hang in a completely different part of the system. The property is: everyone who asked is, next cycle, either active or deferred.

The rotating pointer prevents starvation on a hot line, which is a real workload shape rather than a corner case. A single contended line with a fixed-priority serialiser gives the lowest-numbered agent unlimited access, and Chapter 3.3 measured what that looks like.

Simulation evidence

Four agents request the same line in the same cycle:

=== EXP2: one line, four agents asking at once ===
  cyc 0: active=0001 deferred=1110
  turn 1: active=0010 deferred=1100
  turn 2: active=0100 deferred=1000
  turn 3: active=1000 deferred=0000
  turn 4: active=0000 deferred=0000
  max wait on a contended line = 6 cycles; lost_request_err=0

One active, three deferred, and nobody lost. Each turn promotes exactly one and the deferred set shrinks monotonically. The worst wait was 6 cycles for four agents on one line — and that number is the cost of contention on a single address, which is why false sharing is expensive: two unrelated variables in one line make every access pay this.

11. RTL 3 — Waiting for the Snoops

Purpose

The step that cannot be skipped.

// Collect the acknowledgements that must arrive before ownership can move.
//
// The set is a VECTOR, not a count: clearing a bit is idempotent, so a
// duplicate acknowledgement is harmless, and when something hangs the vector
// names the agent that did not answer.
//
// EARLY_GRANT=1 grants as soon as the snoops are SENT, which is the classic
// coherence bug: issuing a snoop is not the same as it having taken effect.
//
// GENERIC teaching model. NOT a CXL snoop mechanism.
module snoop_tracker #(
  parameter int unsigned NAGENT      = 4,
  parameter int unsigned TIMEOUT     = 16,
  parameter bit          EARLY_GRANT = 1'b0
) (
  input  logic              clk,
  input  logic              rst_n,
  input  logic              start,
  input  logic [NAGENT-1:0] snoop_set,     // who must be invalidated
  input  logic [NAGENT-1:0] ack,
  output logic [NAGENT-1:0] snoop_out,
  output logic [NAGENT-1:0] awaiting_q,
  output logic              busy_q,
  output logic              grant,
  output logic [7:0]        age_q,
  output logic              timeout_err,
  output logic              grant_with_pending_err
);
  assign remaining = awaiting_q & ~ack;
 
  // The whole difference between a correct and a broken coherence point.
  assign grant = EARLY_GRANT ? start
                             : (busy_q && (remaining == {NAGENT{1'b0}}));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin /* ... */ end
    else begin
      snoop_out <= '0;
      if (start && !busy_q) begin
        snoop_out  <= snoop_set;
        awaiting_q <= snoop_set;
        busy_q     <= (snoop_set != {NAGENT{1'b0}});
        age_q      <= 8'd0;
      end else if (busy_q) begin
        awaiting_q <= remaining;
        age_q      <= age_q + 8'd1;
        if (remaining == {NAGENT{1'b0}}) busy_q <= 1'b0;
        // A hang is not a coherence error and no safety property reports it.
        if (age_q + 8'd1 >= TIMEOUT[7:0]) timeout_err <= 1'b1;
      end
      // Ownership moved while somebody still held a readable copy.
      if (grant && ((busy_q ? remaining : snoop_set) != {NAGENT{1'b0}}))
        grant_with_pending_err <= 1'b1;
    end
  end
endmodule

awaiting_q & ~ack and not a counter. Two reasons, and both are load-bearing. Clearing a bit is idempotent, so a duplicate acknowledgement is harmless — a counter decrements twice and can reach zero early, granting a writer with a live sharer. And when nothing arrives, the vector names the agents, which is the difference between a five-minute investigation and a week of it.

age_q and timeout_err exist because the failure is a hang. A snoop that never returns is not a coherence violation; it is an absence, and no safety property can express an absence. Section 15's liveness property is the only thing that catches it.

Simulation evidence — the correct sequence

=== EXP3: invalidate before granting, or grant and hope ===
  start asserted, snoops going out this cycle:
    correct tracker : grant=0  <-- nothing granted yet
    early-grant     : grant=1  <-- granted before any ack exists
  snoops sent : awaiting=0111  correct grant=0
  ack from a0 : awaiting=0110  correct grant=0
  ack from a1 : awaiting=0100  correct grant=0
  ack from a2 : remaining=0  correct grant=1  <-- now, and not before
 
  early-grant instance: grant_with_pending_err=1

The early-grant instance grants in the same cycle the snoops leave, before any cache has had the opportunity to respond, and grant_with_pending_err confirms it. The correct tracker granted only when remaining reached zero — three cycles later in this run, and in general as many cycles as the slowest cache takes.

Simulation evidence — a snoop that never returns

=== EXP4: a snoop that never comes back ===
  after 18 cycles with no acks: awaiting=1111 busy=1 age=18 timeout_err=1
  -> the vector names agents 1111 as the ones that never answered

The line is permanently unwritable. Nothing in the coherence model was violated — no two writers, no stale read, no illegal state — and the system has stopped. That is the signature of a liveness failure, and the vector is what turns "something is stuck" into "these four agents did not respond".

12. RTL 4 — Where the Authoritative Value Lives

Purpose

The read flow's step 4, and the reason memory is not the source of truth.

// Where does the authoritative value come from?
//
// If a cached copy is dirty, memory is STALE -- the value in memory was
// correct before the owner modified it and has not been updated since. A
// coherence point that always reads memory returns old data with no error.
//
// GENERIC teaching model; the "forward from owner" behaviour here is an
// architectural abstraction, NOT a claim about any CXL data-return mechanism.
module data_source_select #(
  parameter bit ALWAYS_MEMORY = 1'b0     // 1 = the bug shape
) (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        req,
  input  logic        dirty,
  input  logic        owner_present,
  input  logic [31:0] memory_value,
  input  logic [31:0] owner_value,
  output logic [31:0] data_out,
  output logic        from_owner,
  output logic        stale_data_err
);
  logic must_forward;
 
  // Memory is authoritative only when nobody holds a modified copy.
  assign must_forward = dirty && owner_present;
  assign from_owner   = req && !ALWAYS_MEMORY && must_forward;
  assign data_out     = from_owner ? owner_value : memory_value;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) stale_data_err <= 1'b0;
    // Returned memory while a modified copy existed elsewhere.
    else if (req && must_forward && !from_owner) stale_data_err <= 1'b1;
  end
endmodule

must_forward requires both terms. dirty alone is not enough — a dirty bit with no owner is one of the illegal directory states from Section 9, and forwarding from a nonexistent owner would return whatever the data path happens to present. That is why the two facts are stored separately and checked together.

Simulation evidence

Two instances, identical inputs, memory holding dead0000 and the owner's cache holding beef1234:

=== EXP5: where the authoritative value lives ===
  clean, no owner  : correct=dead0000 from_owner=0 | always-memory=dead0000
  DIRTY owner held : correct=beef1234 from_owner=1 | always-memory=dead0000  <-- stale
 
  always-memory instance: stale_data_err=1

Row one is identical between the two designs, which is the entire reason this bug ships. Every read of a clean line — the overwhelming majority of reads — behaves correctly. Only a read of a line that some cache has modified diverges, and the divergence is a plausible value: dead0000 is not an error code, it is the value that used to be at that address.

This is the failure mode with no signature. A wrong value that looks like a right value produces a computation that completes, returns a result, and is wrong. There is no exception to catch and no log entry to find — which is why the invariant has to be asserted rather than tested for by observation.

13. RTL 5 — The Transaction Lifecycle

Purpose

Bound a coherent operation in time, so a response can be matched and retired exactly once.

// The lifecycle of one coherent operation, from accept to retire.
//
// GENERIC teaching model. NOT a CXL transaction-ID mechanism.
module coh_tag_tracker #(
  parameter int unsigned NTAG = 8
) (
  input  logic                    clk,
  input  logic                    rst_n,
  input  logic                    open,
  input  logic [3:0]              open_agent,
  input  logic                    close,
  input  logic [$clog2(NTAG)-1:0] close_tag,
  output logic                    open_ok,
  output logic [$clog2(NTAG)-1:0] open_tag,
  output logic [3:0]              close_agent,
  output logic                    close_matched,
  output logic                    unknown_close_err,
  output logic                    premature_retire_err,
  output logic [NTAG-1:0]         live_vec,
  output logic [7:0]              live_q
);
  // ... lowest free tag; open_ok requires one to exist ...
 
  assign close_agent   = agent_q[close_tag];
  assign close_matched = close && live[close_tag];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin /* ... */ end
    else begin
      if (open_ok) begin
        live[open_tag]    <= 1'b1;
        agent_q[open_tag] <= open_agent;
      end
      if (close) begin
        // A close for a tag nobody owns is a duplicate response, or a
        // transaction that was retired too early. Both are reportable.
        if (!live[close_tag]) unknown_close_err <= 1'b1;
        else                  live[close_tag] <= 1'b0;
      end
      live_q <= live_q + {7'b0, open_ok} - {7'b0, close_matched};
    end
  end
endmodule

The else on the close is the important line. A close for a tag that is not live must not clear anything — it is a duplicate, and treating it as valid would retire whatever happens to be at that index next. This is Chapter 3.2's wrong-slot lesson in its coherence form, where the consequence is a coherence transaction believed complete while its state change has not happened.

Simulation evidence

=== EXP6: coherent operation lifecycle ===
  2 open: live=00000011 count=2
  close tag 1: matched=1 agent=9
  close tag 1 AGAIN: unknown_close_err=1  (a duplicate response)
  live now: 00000001 count=1

The duplicate was detected and, crucially, changed nothing — the live vector still shows tag 0 outstanding. A tracker without the guard would have cleared tag 1 again, which is harmless here and would not be if tag 1 had been reallocated in between.

14. Waveform — The Ownership Transfer, Cycle by Cycle

This is the most important figure in the chapter. It is a transcription of the simulated run, and every value in it came from the trace.

Reading it cycle by cycle

Cycle 0. Idle. Three CPU caches hold readable copies of the line; nothing is in flight.

Cycle 1. dev_wr_req pulses. The device has asked. Nothing else changes — home has not yet acted, and this cycle is where the request enters the serialiser from Section 10.

Cycle 2. snoop_out reads 0111: home has asked all three sharers to invalidate. pending becomes 0111 and busy asserts. The grant is zero, and this is the cycle where the early-grant bug would have asserted it.

Cycle 3. cpu_ack reads 0001. Agent 0 has complied. pending drops to 0110. Two agents may still be serving reads from their copies, so the grant stays low.

Cycle 4. Agent 1 acknowledges. pending drops to 0100. One agent still holds a copy — and one is enough to make a grant wrong.

Cycle 5. Agent 2 acknowledges. pending reaches 0000 and grant asserts in the same cycle. This simultaneity is not an optimisation; it is the requirement. A grant one cycle earlier is a coherence violation and one cycle later is pure added latency.

Cycle 6. busy falls. The device owns the line and may write. Home's directory now records the device as owner with an empty sharer set — updated together, per Section 8's step 5.

Cycles 7–8. Steady state. The line is exclusively held.

The bug signatures visible in this waveform

Grant asserting at cycle 2 — the early-grant defect. The device writes while three caches still serve the old value.

Grant asserting at cycle 4 — a counter that decremented twice on a duplicate acknowledgement. Two acks arrived and the count reached zero with agent 2 still live.

pending never reaching 0000 — a lost acknowledgement. busy stays high forever, the grant never comes, and the line is permanently unwritable. This one is a hang, not a corruption, and no safety property reports it.

sharers clearing at cycle 6 instead of 5 — a one-cycle window in which the device is owner and three caches are sharers. The single-writer invariant is broken for one cycle, and one cycle is enough.

15. The Read and the Write, as Sequences

Compare the two diagrams. The read snoops one cache and returns data; the write snoops every holder and returns only permission. That asymmetry is why write latency on a shared line scales with the number of sharers and read latency generally does not — and it is the mechanism behind Chapter 1.7's coherence cost.

16. Assertions

Icarus does not execute concurrent SVA, so these were not run; the table gives the procedural check that stood in for each.

// C1 — SINGLE WRITER: at most one owner, ever.
a_single_writer: assert property (@(posedge clk) disable iff (!rst_n)
  $countones(owner_q) <= 1);
 
// C2 — no reader coexists with a writer.
a_no_sharer_with_owner: assert property (@(posedge clk) disable iff (!rst_n)
  (owner_q != '0) |-> (sharers_q == '0));
 
// C3 — dirty data always has exactly one authoritative holder.
a_dirty_has_owner: assert property (@(posedge clk) disable iff (!rst_n)
  dirty_q |-> ($countones(owner_q) == 1));
 
// C4 — NOTHING is granted while invalidations are outstanding.
a_no_early_grant: assert property (@(posedge clk) disable iff (!rst_n)
  grant |-> ((awaiting_q & ~ack) == '0));
 
// C5 — a requester is never lost: next cycle it is active or deferred.
a_request_kept: assert property (@(posedge clk) disable iff (!rst_n)
  req[a] |=> (active_q[a] || deferred_q[a]));
 
// C6 — at most one request is active on a line.
a_one_active: assert property (@(posedge clk) disable iff (!rst_n)
  $countones(active_q) <= 1);
 
// C7 — memory is never the source while a modified copy exists.
a_no_stale_read: assert property (@(posedge clk) disable iff (!rst_n)
  (req && dirty && owner_present) |-> from_owner);
 
// C8 — a completion always corresponds to a live transaction.
a_close_live: assert property (@(posedge clk) disable iff (!rst_n)
  close |-> live[close_tag]);
 
// C9 — LIVENESS: the transient state terminates.
// ASSUMPTION: every snooped agent eventually responds. Without that
// assumption this property is unprovable, and stating it is the point --
// the hardware's obligation is bounded only if its peers' is.
a_transient_terminates: assert property (@(posedge clk) disable iff (!rst_n)
  busy_q |-> ##[1:TIMEOUT] !busy_q);

17. Verification Architecture

Coherence is the hardest thing on this track to verify, because the interesting states are combinations and the failures are silent. A workable structure:

A reference model that tracks ownership per line. For every address the model holds the same five facts as Section 9's directory. On every observed event it updates independently, and after every event it compares. The comparison catches the directory diverging from what the message sequence implies — which no single-module assertion can see.

A scoreboard keyed on address, not on transaction. Coherence bugs are relationships between transactions on the same line, so a scoreboard organised by transaction ID will not find them. Keying on address makes "two writers to X" a single-line check.

A last-writer table for data checking. Record the value the most recent granted owner wrote. Every subsequent read of that line must return that value; a read returning anything else is the stale-data defect, and it is the only way to catch it, because Section 12 showed the wrong value looks legitimate.

The stimulus list, from the measured defects:

The two in bold are the ones most often missing, and each corresponds to a defect no safety property catches: a duplicate that makes a counter reach zero early, and an absence that stops the system without violating anything.

18. Debug Lab

// The snoops are going out, so the sharers are as good as gone.
if (req_write) begin
  snoop_out  <= sharers_q;
  owner_q    <= requester;
  grant      <= 1'b1;          // same cycle
end

  start asserted, snoops going out this cycle:
    correct tracker : grant=0  <-- nothing granted yet
    early-grant     : grant=1  <-- granted before any ack exists
 
  early-grant instance: grant_with_pending_err=1

assign grant = busy_q && ((awaiting_q & ~ack) == '0);
// and install the owner and clear the sharers in the SAME transition
if (grant) begin owner_q <= pending_owner; sharers_q <= '0; end

// Count down the outstanding invalidations.
if (|ack) ack_count_q <= ack_count_q - $countones(ack);
assign grant = busy_q && (ack_count_q == 0);

  ack from a0 : awaiting=0110  correct grant=0
  ack from a1 : awaiting=0100  correct grant=0
  ack from a2 : remaining=0  correct grant=1  <-- now, and not before

assign remaining = awaiting_q & ~ack;        // idempotent
assign grant     = busy_q && (remaining == '0);
awaiting_q <= remaining;

// The line is in memory; read it.
assign data_out = memory_value;

  clean, no owner  : correct=dead0000 from_owner=0 | always-memory=dead0000
  DIRTY owner held : correct=beef1234 from_owner=1 | always-memory=dead0000  <-- stale

assign must_forward = dirty && owner_present;   // BOTH terms
assign from_owner   = req && must_forward;
assign data_out     = from_owner ? owner_value : memory_value;

// The line is busy; this requester will ask again.
if (line_busy) ;               // request simply not recorded
else           active_q <= requester;

  cyc 0: active=0001 deferred=1110
  turn 1: active=0010 deferred=1100
  turn 2: active=0100 deferred=1000
  turn 3: active=1000 deferred=0000
  max wait on a contended line = 6 cycles; lost_request_err=0

deferred_q <= (deferred_q | req) & ~(accept ? pick : '0);
// every requester is, next cycle, active or deferred
a_request_kept: assert property (req[a] |=> (active_q[a] || deferred_q[a]));

// A response arrived for this tag; retire it.
if (close) live[close_tag] <= 1'b0;

  close tag 1: matched=1 agent=9
  close tag 1 AGAIN: unknown_close_err=1  (a duplicate response)
  live now: 00000001 count=1

if (close) begin
  if (!live[close_tag]) unknown_close_err <= 1'b1;   // duplicate, or too-early retire
  else                  live[close_tag] <= 1'b0;
end

// Wait for the acknowledgements.
if (busy_q && (remaining == '0)) busy_q <= 1'b0;
// ... and nothing else. No age, no timeout, no report.

  after 18 cycles with no acks: awaiting=1111 busy=1 age=18 timeout_err=1
  -> the vector names agents 1111 as the ones that never answered

age_q <= age_q + 1;
if (age_q + 1 >= TIMEOUT) timeout_err <= 1'b1;   // awaiting_q names who

19. Quantitative Reasoning — What Coherence Costs

Two numbers worth being able to derive.

Invalidation latency scales with the sharer count. With S sharers and a per-agent response latency of L cycles, the transient state lasts at least:

T_transient  ≈  L  +  (S − 1) × spacing

In the measured run, three sharers responding one per cycle gave three cycles. The important consequence is that the more widely a line is read, the more expensive it is to write — so a line read by 32 cores is dramatically more expensive to write than one read by 2, and the cost is paid by the writer.

That is the mechanism behind false sharing. Two unrelated variables in one 64-byte line make every write to either one pay the other's sharer count, and the penalty grows with core count — which is why it gets worse on newer hardware rather than better.

Serialisation cost on a hot line. With N agents contending for one line and a service time of T per turn, the last agent waits (N − 1) × T. Measured, four agents on one line gave a worst wait of 6 cycles. Scale N and the wait grows linearly — and because home serialises per line, this cost is invisible in any aggregate throughput number and appears only as tail latency on specific addresses.

Neither number is a CXL number. Both are properties of coherence itself, which is why the reasoning transfers to any coherent interconnect and why Chapter 1.7 framed the trade before any protocol was named.

20. Design Review — Reading a Coherence Point

On the directory. Are owner and dirty separate fields? Is dirty ever true with no owner? Is there a transient indication, and can home express "come back later" without dropping a request? Are the invariants checked on the stored state or on the write inputs?

On serialisation. Is a conflicting requester deferred or dropped? Is there a property that every requester is next-cycle active or deferred? Is the selection rotating, so a hot line cannot starve an agent?

On snoops. Is the outstanding set a vector or a count? Is anything granted while the set is non-empty? Are the owner installation and the sharer clear in the same transition, or one cycle apart? Is there an age and a timeout, and does the report name the non-responders?

On data. Does the read path consult dirty at all? Does forwarding require both dirty and an owner? Is there a last-writer check anywhere in the verification environment?

On the lifecycle. Is a close for a non-live tag guarded and reported? Does the regression run at occupancy high enough for tags to be reused?

And the assumption question. Which of this design's liveness properties depend on peers behaving, and is that dependency written down? A timeout is the admission that it cannot be guaranteed — and a design without one has the same dependency, undocumented.

21. How This Appears in Real Engineering

Coherency architect

The asymmetry is the defining decision: the host orchestrates, so the device's obligation is to hold copies correctly and answer promptly. That choice trades per-transaction latency for adoption, and later peer-to-peer and symmetric-link work is the industry revisiting the trade rather than repudiating it.

RTL engineer

Five rules, all measured here. Separate owner from dirty. Defer, never drop. Track the outstanding set as a vector. Grant only when it is empty, and clear the sharers in the same transition. Age the transient state.

Verification engineer

Three things this chapter's defects demand. A reference model per line, because the interesting failures are relationships between transactions on one address. A last-writer data check, because the stale-read defect has no signature and cannot be observed. And duplicate and lost messages injected deliberately, because real links retry and real caches hang, and both defects are invisible in a bench that never does either.

Performance engineer

Instrument the transient-state duration as a maximum, not a mean, and instrument it per line if you can. Coherence cost is concentrated on hot lines, so an average across all addresses reports a healthy system that has a few pathologically expensive addresses in it. When write latency is high and read latency is not, the sharer count is the first thing to look at.

Firmware and system software

The layout decisions that avoid false sharing live here. Two variables written by different agents must not share a line, and the cost of getting that wrong grows with core count. There is no hardware fix — the coherence protocol is doing exactly what it should.

Silicon debug

Learn the four waveform signatures in Section 14. A grant at the snoop cycle is an early grant; a grant partway through the acknowledgements is a duplicate-decremented counter; a pending set that never empties is a lost response; sharers clearing one cycle after the owner installs is a one-cycle invariant break. Each points at a different fix.

22. Common Misconceptions

23. Interview Reasoning

24. Exercises

1. Derive the illegal states. Section 9's directory has 5 fields. Enumerate the representable combinations for NAGENT = 2 and mark which the coherence model forbids. What fraction of the encoding space is illegal, and what does that ratio tell you about how much of coherence verification is checking for impossible states?

2. Time the write. A line has 8 sharers, each responding with latency uniformly distributed between 4 and 20 cycles, responses fully parallel. What is the expected transient duration? Now make them serialised at one per cycle after the first response. Which model matches the measured 3-cycle result for 3 sharers?

3. Break C4 a third way. Debug Labs 1 and 2 both produce a grant with a live sharer. Construct a third mechanism with the same symptom, and determine whether grant |-> ((awaiting_q & ~ack) == 0) catches it.

4. Write the assumption. State C9's environment assumption as an SVA assume. Then argue what the design must do when the assumption is violated, and why a timeout is a policy decision rather than a correctness fix.

5. Design the last-writer check. Sketch the testbench structure that catches the stale-read defect. What does it store, when does it update, and what happens on an eviction of a dirty line? Explain why an assertion inside the coherence point cannot replace it.

25. Summary

Coherence answers two questions about one line: who has the authoritative value, and who may change it. Every mechanism in this chapter exists to answer one of them without ever letting two agents disagree.

Home is a serialiser, not an arbiter. Four agents requesting one line produced one active and three deferred, with nothing lost and a worst wait of 6 cycles. A serialiser that drops the loser produces a requester waiting forever for a completion that will never be sent — and the hang appears in a subsystem unrelated to coherence.

Memory is authoritative only when no cache holds a modified copy. Measured, a read against a dirty owner returned dead0000 from memory while beef1234 sat in the owning cache. Clean-line reads were identical between the correct and broken designs, which is why the defect ships — and the wrong value is a plausible value, so nothing downstream can detect it.

Sending a snoop is not the same as the copy being gone. The early-grant design asserted its grant in the same cycle the snoops left, before any cache could respond. The correct tracker granted when the outstanding set reached zero — three cycles later here, and in general as long as the slowest cache takes. The waveform in Section 14 shows the grant landing in the same cycle as the last acknowledgement, which is a requirement rather than an optimisation.

Track the set, not the count. Clearing a bit is idempotent, so a duplicate acknowledgement is harmless; a counter decrements twice and can grant over a live sharer. And when a response never arrives, the vector named all four agents where a counter would have said "four missing".

And the model is asymmetric on purpose. Consortium material describes the host orchestrating the coherency management and names that asymmetry as easing device adoption. The device's obligation is short — hold copies correctly, answer promptly — which is why an accelerator can participate in coherence without building a CPU's coherence engine. The cost is a round trip for every decision, which later peer-to-peer and symmetric-link work addresses.

Two things carry beyond coherence. A liveness failure satisfies every safety property — the lost-response run halted with nothing violated — and the liveness property that catches it depends on an assumption about peers that must be written down, because a timeout is the admission that it cannot be guaranteed. And the worst defects have no signature: a stale read completes, returns a plausible value, and is wrong, so it can only be caught by a model that independently knows what the value should be.

26. What Comes Next

This chapter described a conversation without saying anything about how the messages travel. That was deliberate: coherence semantics and message transport are different concerns, and keeping them apart is what makes both tractable.

Chapter 3.5 is that separation stated as architecture — which layer owns request semantics, which owns reliable delivery, which owns signalling, and what goes wrong when a responsibility lands in the wrong one.

For adjacent material: Why Coherent Attach Matters has the cost argument this chapter measures, The CXL Host has the home agent as a structure, The CXL Device has the cache engine that answers the snoops, and The CXL Fabric explains why coherent traffic is the constrained one through a switch. The path is on the CXL tutorials index.