Coherency Review Checklist

30.2 reviewed the RTL and 30.3 reviewed the environment that judges it. This chapter reviews the one property neither of them can check locally, because it is not a property of any single agent.

The review question this chapter turns on, asked once per dimension:

For this cache line, who has authority over the newest value now — and what must happen before that authority can safely change?

Every item below is a different way of asking it. Every defect below is a design where the answer is "two agents", "nobody", or "an agent that is gone".

1. Coherence Is Not Consistency

These two are routinely merged and they are different properties with different mechanisms, different failure modes and different reviews.

A system can be perfectly coherent and have a weak consistency model, and that is not a bug — it is a design decision, documented and programmed against. A system can also have a strict consistency model and be incoherent, and that is always a bug.

Do not merge them in a review. A coherency finding is "this line had two owners". A consistency finding is "this ordering was observable and the model forbids it". They are found by different questions, and a reviewer who asks only one will miss the other entirely.

This chapter reviews coherence. Consistency is named here only so the boundary is explicit.

2. How To Use This Chapter

Each of the nine review dimensions below is a working review item, and every one answers the same eight questions:

3. The One-Sentence Model

A coherency review is sound when the protocol is claimed coherent, when authority over every line is single-valued, when a writer excludes every reader, when every invalidation is acknowledged before ownership moves, when every acknowledgement is qualified by its epoch, and when recovery reclaims every line owned by an agent that is gone — and "the protocol is coherent" is bit 0.

4. What This Chapter Owns

The distinction from 30.1 is worth stating. 30.1's authority item asks whether any resource has single-valued authority. This chapter asks it of a cache line, where the resource is replicated, the copies are the whole point, and the mechanism has to work while the copies exist.

5. Teaching-Model Boundary And Source Discipline

Every model in this chapter is a teaching model. Each isolates one coherency invariant so it can be examined, mutated and broken on purpose. None is a CXL directory, a coherence controller, or an implementation of any specification flow.

Nothing here states a normative CXL detail. No opcode, packet layout, bit position, field width, response encoding, snoop encoding, retry rule, timeout constant, latency figure or register definition from the specification appears anywhere in this chapter. No state name from any published protocol is used, and the states here are named for what they mean rather than borrowed. The invariants reviewed — single authority, writer-reader exclusion, acknowledgement conservation, epoch qualification — are general properties any coherent system must satisfy, and they are examined in their general form deliberately, so the review technique transfers.

6. Review Item 1 — Who Has Authority Over The Newest Value?

Under review. The directory, the snoop filter, the ownership record — whatever structure answers the question.

Invariant at risk. At every instant, exactly one agent holds the authoritative copy of a line, and every other holder either matches it or knows it does not.

Where it lives. The distinction between a set of holders and an owner.

The failure. A structure that records who has a copy cannot answer whose copy is newest. It is not a weaker version of the right structure; it answers a different question, and the difference only appears when somebody writes.

// RTL 1 - who has authority over the newest value of this line?
//
// The central coherency question. At every instant exactly one agent must hold
// the authoritative copy of a line, and every other holder must either match it
// or know that it does not. A directory that records a set of holders WITHOUT
// recording which one is authoritative cannot answer the question at all.
//
//   BAD  : holders = {A, B}                   // which one is newest?
//   GOOD : owner = A, sharers = {B}, and only the owner may write
//
// TEACHING MODEL. Isolates one coherency invariant. It is NOT a CXL directory,
// not an implementation of any specification flow, and contains no opcode,
// message name, encoding or field layout from any specification.
module newest_authority #(parameter int SET_WITHOUT_OWNER = 0) (
  input  logic clk, rst_n,
  input  logic       grant_excl, release_excl, add_sharer, write_req,
  input  logic [1:0] agent,
  output logic [1:0] owner,
  output logic       owner_valid, write_allowed, newest_authoritative,
  output logic [3:0] sharers,
  output logic [7:0] n_writes, n_unowned_writes, n_claimants,
  output logic       auth_err
);
  logic [1:0] own_q;
  logic       ov_q;
  logic [3:0] shr_q;
  logic [7:0] pc;
  integer i;

  always_comb begin
    pc = 8'd0;
    for (i = 0; i < 4; i = i + 1) if (shr_q[i]) pc = pc + 8'd1;
  end

  assign owner       = own_q;
  assign owner_valid = ov_q;
  assign sharers     = shr_q;
  assign n_claimants = pc + {7'd0, ov_q};
  // The whole review point. The set-only build permits a write from anybody in
  // the set, because it has no notion of which member is authoritative.
  assign write_allowed = (SET_WITHOUT_OWNER != 0)
                       ? (write_req && (shr_q[agent] || (ov_q && (own_q == agent))))
                       : (write_req && ov_q && (own_q == agent));
  // The line has a single newest value exactly when exactly one agent may write.
  assign newest_authoritative = ov_q;
  // SAFETY VIOLATION: a write was allowed by an agent that does not own the line.
  assign auth_err = write_allowed && !(ov_q && (own_q == agent));

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      own_q <= 2'd0; ov_q <= 1'b0; shr_q <= 4'd0;
      n_writes <= 8'd0; n_unowned_writes <= 8'd0;
    end else begin
      if (grant_excl) begin
        own_q <= agent; ov_q <= 1'b1; shr_q <= 4'd0;
      end else if (release_excl) begin
        ov_q <= 1'b0;
      end else if (add_sharer) begin
        shr_q[agent] <= 1'b1;
      end
      if (write_allowed) n_writes <= n_writes + 8'd1;
      if (auth_err)      n_unowned_writes <= n_unowned_writes + 8'd1;
    end
  end
endmodule

The measurement. Agent 1 holds the line exclusively. Agent 2 is added to the holder set. Agent 2 then writes:

agent 2 writes : owner=1 owner_valid=1 owned_write=0 set_write=1

The owner-qualified build refuses. The set-only build allows it, because agent 2 is indeed in the set. Over the run the set-only build records one write and one unowned write — the same event, counted twice, because the second counter is the escape and the first is the work.

Both builds report the line as authoritative. That is the part to sit with: the set-only build's newest_authoritative output reads 1 while two agents may write. The structure is reporting a property it cannot evaluate.

Evidence to demand. Point at the field that names the owner. If the answer is a bitmask, ask which bit is the owner. "The first one set" is not an answer; it is an ordering imposed by the reader on a structure that does not carry one.

What escapes. Two agents writing one line. This is the worst escape in the chapter: silent, data-corrupting, and separated from its cause by however long the two copies diverge before anybody reads.

How DV proves it. Add a second holder and have it write. A test that only ever writes from the agent that requested the line cannot find this, and that is the natural directed test.

Telemetry. An unowned-write counter that must read permanently zero, and the claimant count — owner plus sharers — as a distribution.

Misleading evidence. A directory that always shows exactly one entry set, because the test never created a second holder.

Figure 1 — the two structures record the same agents. Both know agent 1 and agent 2 hold the line. Only one of them records which holder the newest value belongs to, and that field is the entire difference between a refused write and a corrupted line.

7. Review Item 2 — Does A Writer Exclude Every Reader?

Under review. The invalidation that accompanies an exclusive grant.

Invariant at risk. Two properties that are usually stated as one:

• Single writer. At most one agent may write the line at a time.
• Exclusion. While an agent may write, no other agent may read.

Where it lives. What the grant does to the read copies.

Why they are different. A design can satisfy the first and violate the second. One writer plus a stale reader is not a write-write race; it is a reader holding a value that is no longer the newest one — the quieter of the two failures, and the harder to trace.

// RTL 2 - single writer, and writer-reader exclusion.
//
// Two distinct invariants that are usually stated as one:
//
//   SINGLE WRITER : at most one agent may write the line at a time.
//   EXCLUSION     : while an agent may write, no OTHER agent may read.
//
// A design can satisfy the first and violate the second. One writer plus a
// stale reader is not a write-write race; it is a reader holding a value that
// is no longer the newest one, which is the quieter of the two failures.
//
// TEACHING MODEL.
module writer_exclusion #(parameter int READERS_MAY_LINGER = 0) (
  input  logic clk, rst_n,
  input  logic       take_excl, drop_excl, do_read, do_write,
  input  logic [3:0] reader_mask,
  input  logic [1:0] agent,
  output logic [3:0] readers, writers,
  output logic [7:0] n_writers, n_readers, n_overlap_cycles,
  output logic       single_writer_ok, exclusion_ok, read_allowed, write_allowed,
  output logic       excl_err
);
  logic [3:0] rd_q, wr_q, rd_next, wr_next;
  logic [7:0] wc, rc;

  // ONE assignment to each vector, computed from ALL events. Written as
  // independent `if` statements, a reader joining in the same cycle as an
  // exclusive grant overwrote the invalidation and survived it - which is
  // precisely the defect this model exists to show, appearing in the build that
  // is supposed to be correct. STATED PRIORITY: a take wins its own agent over
  // a drop, and the invalidation is applied LAST so it also catches a reader
  // that joins in the grant cycle.
  always_comb begin
    wr_next = wr_q;
    if (drop_excl) wr_next[agent] = 1'b0;
    if (take_excl) wr_next[agent] = 1'b1;
    rd_next = rd_q;
    if (|reader_mask) rd_next = rd_next | reader_mask;
    if (take_excl && (READERS_MAY_LINGER == 0)) rd_next = 4'd0;
  end
  integer i;

  always_comb begin
    wc = 8'd0; rc = 8'd0;
    for (i = 0; i < 4; i = i + 1) begin
      if (wr_q[i]) wc = wc + 8'd1;
      if (rd_q[i]) rc = rc + 8'd1;
    end
  end

  assign readers   = rd_q;
  assign writers   = wr_q;
  assign n_writers = wc;
  assign n_readers = rc;
  assign single_writer_ok = (wc <= 8'd1);
  // Exclusion holds when no reader coexists with a writer.
  assign exclusion_ok     = (wc == 8'd0) || (rc == 8'd0);
  assign write_allowed    = do_write && wr_q[agent];
  // The whole review point. The lingering build lets a reader keep its copy
  // while an exclusive writer is live.
  assign read_allowed     = (READERS_MAY_LINGER != 0)
                          ? (do_read && rd_q[agent])
                          : (do_read && rd_q[agent] && (wc == 8'd0));
  // SAFETY VIOLATION: a read was permitted while a writer holds the line.
  assign excl_err = read_allowed && (wc != 8'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rd_q <= 4'd0; wr_q <= 4'd0; n_overlap_cycles <= 8'd0;
    end else begin
      wr_q <= wr_next;
      rd_q <= rd_next;
      if (!exclusion_ok) n_overlap_cycles <= n_overlap_cycles + 8'd1;
    end
  end
endmodule

The measurement. Agents 1 and 2 hold read copies. Agent 0 takes the line exclusively:

exclusive taken : writers=1 excl_readers=0 lingering_readers=2

There is exactly one writer in both builds. The single-writer invariant holds either way, and a review that checks only that invariant signs both designs off. The difference is entirely in what the grant did to the readers: the invalidating build cleared them; the lingering build left both in place, so a writer and two readers coexist and the reads return a value that is no longer current.

The run also drives the other half, where two agents take the line for writing at once: the single-writer invariant is violated and exclusion still holds, because there are no readers left to violate it against. Two invariants, four combinations, and a review that collapses them into one covers two of the four.

Evidence to demand. The invalidation that accompanies the grant, and the point at which the grant is considered complete relative to it. "The readers are invalidated" is a claim about ordering, and section 9 is about what makes that ordering real.

What escapes. A reader consuming stale data with no error anywhere. The write succeeded, the read succeeded, and the values differ.

How DV proves it. Establish readers first, then grant exclusive, then read from a former reader. A test that grants exclusive on a line nobody holds cannot find this, and that is the natural order to write a test in.

Telemetry. Overlap cycles — cycles in which a writer and at least one reader both hold the line. Must read permanently zero.

Misleading evidence. A single-writer assertion that passes. It does pass. It is checking the other invariant.

8. Review Item 3 — Who Owes The Write-Back?

Under review. Every eviction, every capacity replacement, every downgrade of a modified line.

Invariant at risk. A modified line exists in exactly one place in its newest form, and whoever holds that form owes a write-back before dropping it.

Where it lives. The eviction path's handling of the dirty bit.

The failure. A design that evicts a modified line without writing it back has not corrupted anything visibly. It has lost the newest data, and memory still holds a value that reads perfectly well.

// RTL 3 - dirty ownership. Who owes the write-back?
//
// A line that has been modified exists in exactly one place in its newest form.
// Whoever holds that form owes a write-back before the line can be dropped. A
// design that evicts a modified line without writing it back has not corrupted
// anything visibly - it has simply lost the newest data, and memory still holds
// a value that reads perfectly well.
//
//   BAD  : on evict, invalidate the line
//   GOOD : on evict, if dirty, write back FIRST, then invalidate
//
// TEACHING MODEL. Sequential.
//   State remembered : one valid bit, one dirty bit, the held data.
//   Safety           : a modified line is never dropped without a write-back.
module dirty_ownership #(parameter int EVICT_WITHOUT_WRITEBACK = 0) (
  input  logic clk, rst_n,
  input  logic       fill, modify, evict,
  input  logic [7:0] fill_data, write_data,
  output logic [7:0] line_data, mem_data, n_writebacks, n_lost,
  output logic       valid_q, dirty_q, writeback, data_lost,
  output logic       dirty_err
);
  logic       v_q, d_q;
  logic [7:0] ln_q, mem_q;

  assign valid_q   = v_q;
  assign dirty_q   = d_q;
  assign line_data = ln_q;
  assign mem_data  = mem_q;
  // The whole review point. The robust build writes back when evicting dirty.
  assign writeback = evict && v_q && d_q && (EVICT_WITHOUT_WRITEBACK == 0);
  // The newest value is about to disappear and memory will not receive it.
  assign data_lost = evict && v_q && d_q && (EVICT_WITHOUT_WRITEBACK != 0);
  // SAFETY VIOLATION: the only copy of the newest value was dropped.
  assign dirty_err = data_lost;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_q <= 1'b0; d_q <= 1'b0; ln_q <= 8'd0; mem_q <= 8'd0;
      n_writebacks <= 8'd0; n_lost <= 8'd0;
    end else begin
      if (fill) begin
        v_q <= 1'b1; d_q <= 1'b0; ln_q <= fill_data;
      end else if (modify && v_q) begin
        d_q <= 1'b1; ln_q <= write_data;
      end else if (evict) begin
        v_q <= 1'b0; d_q <= 1'b0;
        if (writeback) mem_q <= ln_q;
      end
      if (writeback) n_writebacks <= n_writebacks + 8'd1;
      if (data_lost) n_lost       <= n_lost + 8'd1;
    end
  end
endmodule

The measurement. The line is filled with A0 and modified to 5C. Memory still holds 00:

evicting a dirty line : writeback=1 data_lost=1

After the eviction, the writing-back build's memory holds 5C and the dropping build's holds 00 — the value from before the line was ever filled. The eviction itself worked perfectly in both builds: the line is invalid, the tags are clean, the structure is consistent. Only the data is gone.

This is the failure mode with the longest distance between cause and symptom in the chapter. Nothing is inconsistent. No counter is wrong. A later read hits memory, gets 00, and 00 is a completely plausible value.

Evidence to demand. The eviction path, and specifically the ordering between the write-back and the invalidation. Ask what happens if the write-back is refused or retried — an eviction that invalidates first and writes back second has a window in which the newest value exists nowhere.

What escapes. Silent data loss, indistinguishable from a program that wrote the old value.

How DV proves it. Fill, modify, evict, then read memory. The read is the check — asserting that the line went invalid proves the eviction ran, not that it preserved anything.

Telemetry. Write-backs counted against dirty evictions. The two must be equal, and a design that drops data cannot populate the first counter at all.

Misleading evidence. A clean eviction, which needs no write-back and behaves identically in both builds. The run drives it explicitly for that reason.

9. Review Item 4 — Do The Acknowledgements Balance Before The Line Moves?

Under review. Every ownership transfer, exclusive upgrade and invalidation round.

Invariant at risk. Ownership moves only after every copy that had to be invalidated has acknowledged.

Where it lives. The condition on the transfer.

The mechanism is an equation, not an assurance:

invalidations sent == acknowledgements received, before the transfer

A design that transfers on a timer, on a count that was never checked, or on the first acknowledgement, hands the line over while a stale copy is still live somewhere.

// RTL 4 - invalidation acknowledgement conservation.
//
// Ownership may transfer only after every copy that had to be invalidated has
// acknowledged. The mechanism is an equation, not an assurance:
//
//   invalidations sent == acknowledgements received, before the transfer
//
// A design that transfers on a TIMER, on a count that was never checked, or on
// the first acknowledgement, hands the line over while a stale copy is still
// live somewhere.
//
// TEACHING MODEL. Sequential.
//   Safety : ownership never transfers with acknowledgements outstanding.
module ack_conservation #(parameter int TRANSFER_EARLY = 0) (
  input  logic clk, rst_n,
  input  logic       send_invs, ack_in, request_transfer,
  input  logic [3:0] inv_count,
  output logic [7:0] invs_sent, acks_rcvd, acks_outstanding, n_transfers, n_early,
  output logic       transfer_ok, transfer_now, all_acked,
  output logic       ack_err
);
  logic [7:0] sent_q, ack_q, sent_next, ack_next;

  // ONE assignment to each counter, computed from ALL events. Written as
  // independent `if` statements the transfer's clear came last and discarded a
  // send issued in the same cycle. STATED PRIORITY: the transfer closes the
  // round, so both counters clear; a send in that cycle OPENS THE NEXT ROUND
  // and survives the clear, while an acknowledgement in that cycle answers the
  // round that just closed and is dropped.
  always_comb begin
    sent_next = transfer_now ? 8'd0 : sent_q;
    ack_next  = transfer_now ? 8'd0 : ack_q;
    if (send_invs)               sent_next = sent_next + {4'd0, inv_count};
    if (ack_in && !transfer_now) ack_next  = ack_next + 8'd1;
  end

  assign invs_sent        = sent_q;
  assign acks_rcvd        = ack_q;
  assign acks_outstanding = (sent_q >= ack_q) ? (sent_q - ack_q) : 8'd0;
  assign all_acked        = (acks_outstanding == 8'd0);
  // The whole review point.
  assign transfer_ok      = (TRANSFER_EARLY != 0) ? 1'b1 : all_acked;
  assign transfer_now     = request_transfer && transfer_ok;
  // SAFETY VIOLATION: the line changed hands with a live stale copy elsewhere.
  assign ack_err          = transfer_now && !all_acked;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      sent_q <= 8'd0; ack_q <= 8'd0; n_transfers <= 8'd0; n_early <= 8'd0;
    end else begin
      sent_q <= sent_next;
      ack_q  <= ack_next;
      if (transfer_now) n_transfers <= n_transfers + 8'd1;
      if (ack_err) n_early <= n_early + 8'd1;
    end
  end
endmodule

The measurement. Three invalidations sent, two acknowledged, a transfer requested:

transfer requested : sent=3 acked=2 outstanding=1 balanced_ok=0 early_ok=1

Both builds know one acknowledgement is outstanding. The balanced build refuses the transfer; the early build permits it and records one early transfer. One agent now believes it owns the line exclusively while another still holds a copy it was told to drop and has not yet dropped.

The boundary case matters as much as the failure. With zero invalidations to send — a line with no sharers — the equation balances trivially and the transfer is immediate, with no violation. A mechanism that cannot distinguish "nothing to wait for" from "not waiting" would stall every uncontended transfer, and that is the performance cost people cite when arguing for the early build.

Evidence to demand. The counter pair and the comparison, and what clears them between rounds. A design that clears only the sent counter carries acknowledgements from the previous round into the next one — which is section 10.

What escapes. A line owned exclusively by one agent while another holds a readable copy. The writes diverge from that moment.

How DV proves it. Send N invalidations, acknowledge N−1, request the transfer, and require a refusal. Then acknowledge the last one and require the transfer to proceed — a mechanism that never permits anything is not a mechanism.

Telemetry. Outstanding acknowledgements as a distribution, and an early-transfer counter that must read permanently zero.

Misleading evidence. A transfer latency that looks excellent. The early build is genuinely faster, and it is faster because it skipped the wait.

10. Review Item 5 — Which Round Does This Acknowledgement Answer?

Under review. Every acknowledgement, response and completion that carries an identity.

Invariant at risk. No acknowledgement is counted twice, and none from a past round is counted at all.

Where it lives. The counting condition.

The failure. An acknowledgement carries an identity. That identity says which request it answers; it does not say which round. After a retry, a recovery or a second invalidation of the same line, an acknowledgement from the previous round can still arrive, still carry a live identity, and still be counted — satisfying section 9's conservation equation with an acknowledgement nobody is waiting for.

// RTL 5 - stale and duplicate acknowledgements.
//
// An acknowledgement carries an identity. That identity says WHICH request it
// answers; it does not say WHICH ROUND. After a retry, a recovery or a second
// invalidation of the same line, an acknowledgement from the previous round can
// still arrive, still carry a live id, and still be counted - satisfying the
// conservation equation of RTL 4 with an acknowledgement nobody is waiting for.
//
//   BAD  : count every acknowledgement bearing a live id
//   GOOD : count it once, and only if its epoch is the current one
//
// TEACHING MODEL. Sequential.
//   Safety : no acknowledgement is counted twice and none from a past epoch.
module ack_identity #(parameter int COUNT_ANY_ACK = 0) (
  input  logic clk, rst_n,
  input  logic       start_round, ack_valid,
  input  logic [1:0] ack_id,
  input  logic [3:0] ack_epoch,
  output logic [3:0] epoch_now, pending,
  output logic [7:0] n_counted, n_stale, n_dup,
  output logic       stale_ack, dup_ack, counted,
  output logic       id_err
);
  logic [3:0] ep_q, pend_q;
  logic       epoch_ok, id_live;

  assign epoch_now = ep_q;
  assign pending   = pend_q;
  assign epoch_ok  = (ack_epoch == ep_q);
  assign id_live   = pend_q[ack_id];
  assign stale_ack = ack_valid && !epoch_ok;
  assign dup_ack   = ack_valid && epoch_ok && !id_live;
  // The whole review point.
  assign counted   = (COUNT_ANY_ACK != 0) ? ack_valid
                                          : (ack_valid && epoch_ok && id_live);
  // SAFETY VIOLATION: an acknowledgement was counted that answers nothing
  // outstanding in this epoch.
  assign id_err    = counted && !(epoch_ok && id_live);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ep_q <= 4'd0; pend_q <= 4'd0;
      n_counted <= 8'd0; n_stale <= 8'd0; n_dup <= 8'd0;
    end else begin
      if (start_round) begin
        ep_q   <= ep_q + 4'd1;
        pend_q <= 4'hF;                 // every peer owes an acknowledgement
      end else if (counted) begin
        pend_q[ack_id] <= 1'b0;
      end
      if (counted)   n_counted <= n_counted + 8'd1;
      if (stale_ack) n_stale   <= n_stale + 8'd1;
      if (dup_ack)   n_dup     <= n_dup + 8'd1;
    end
  end
endmodule

The measurement. A round starts (epoch 1, four peers owe). A second round starts (epoch 2, four owe again). An acknowledgement arrives stamped epoch 1:

stale ack : epoch_now=2 ack_epoch=1 epoched_count=0 any_count=1

Both builds detect that it is stale. The information is present in the lenient build and it does nothing with it. The epoch-qualified build refuses; the count-any build counts it and clears peer 0's pending bit with an answer to a different question.

One stale answer manufactures a second fault

This is the finding the run produced, and it corrected the lesson I had written down. After the stale acceptance, the legitimate current-epoch acknowledgement from peer 0 arrives — and the count-any build has already cleared peer 0's pending bit, so the real answer looks like a duplicate. Over the sequence the count-any build records two duplicates where the qualified build records one, and three counted acknowledgements for one real answer.

Accepting one stale answer does not cost one acknowledgement. It costs the stale one, the real one that follows, and the accuracy of every count derived from both.

Evidence to demand. The complete counting key: identity and epoch and still-pending. If the key is the identity alone, ask what makes it unique across time rather than only within a round.

What escapes. An invalidation round that completes without every copy actually being dropped — which is section 9's escape, reached through a different door and past a mechanism that was working.

How DV proves it. Start a round, start another, then deliver an acknowledgement stamped with the first. And separately, deliver the same acknowledgement twice inside one round. A four-bit epoch wraps after sixteen rounds, which the run asserts.

Telemetry. Stale acknowledgements detected, stale counted, duplicates detected, duplicates counted. The detected counts are fabric properties. Both counted figures must read permanently zero.

Misleading evidence. A round that completes promptly, every time. The count-any build completes faster, because stale answers from the previous round are doing some of the work.

11. Review Item 6 — What Does The Line Do While It Is Changing Hands?

Under review. The state encoding, and specifically whether it has one.

Invariant at risk. No conflicting request is answered from a state the line is in the middle of leaving.

Where it lives. The presence or absence of a transient state.

The claim. A line is not only invalid, shared or modified. Between those it is in transition — a request has been issued and its response has not arrived — and during that window it must refuse conflicting requests rather than answer them from a state it is about to leave.

// RTL 6 - transient states, and what a line does while it is changing hands.
//
// A line is not only Invalid, Shared or Modified. Between those it is IN
// TRANSITION - a request has been issued and its response has not arrived - and
// during that window it must refuse conflicting requests rather than answer
// them from a state it is in the middle of leaving.
//
//   BAD  : a two-state view - the line is either owned or it is not
//   GOOD : an explicit transient state that refuses conflicts and is exited
//          only by the response it is waiting for
//
// TEACHING MODEL. Sequential.
//   Safety : no conflicting request is answered from a transient state.
module transient_states #(parameter int NO_TRANSIENT = 0) (
  input  logic clk, rst_n,
  input  logic       request, response, conflict_req,
  output logic [1:0] st,
  output logic       transient_now, conflict_refused, conflict_answered,
  output logic [7:0] n_conflicts, n_refused, n_answered,
  output logic       trans_err
);
  localparam logic [1:0] INVALID = 2'd0, PENDING = 2'd1, OWNED = 2'd2;
  logic [1:0] st_q;

  assign st            = st_q;
  // The two-state build has no PENDING encoding at all; it goes straight to
  // OWNED on the request and is therefore never transient.
  assign transient_now = (NO_TRANSIENT != 0) ? 1'b0 : (st_q == PENDING);
  assign conflict_refused  = conflict_req && transient_now;
  assign conflict_answered = conflict_req && !transient_now && (st_q == OWNED);
  // SAFETY VIOLATION: a conflicting request was answered while the line was
  // genuinely mid-transition, whatever this build calls that state.
  assign trans_err = conflict_answered && (st_q == OWNED) && (NO_TRANSIENT != 0)
                     && !response;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= INVALID; n_conflicts <= 8'd0; n_refused <= 8'd0; n_answered <= 8'd0;
    end else begin
      case (st_q)
        INVALID: if (request) st_q <= (NO_TRANSIENT != 0) ? OWNED : PENDING;
        PENDING: if (response) st_q <= OWNED;
        OWNED:   if (conflict_req && !transient_now) st_q <= INVALID;
        default: st_q <= INVALID;
      endcase
      if (conflict_req)      n_conflicts <= n_conflicts + 8'd1;
      if (conflict_refused)  n_refused   <= n_refused + 8'd1;
      if (conflict_answered) n_answered  <= n_answered + 8'd1;
    end
  end
endmodule

The measurement. A request is issued and no response has arrived. A conflicting request arrives:

conflict while in transition : pending_refuses=1 two_state_answers=1

The three-state design refuses. The two-state design has already declared itself the owner — it has no encoding for "requested but not yet granted" — and answers a conflict on the strength of an ownership it does not yet have.

A transient state is exited by its response, not by time. The run drives a second clock with no response and asserts the line is still in transition, then drives a second conflict and requires a second refusal. That case was a mutation survivor on the first campaign — the environment had only ever spent one clock in the transient state — and section 19 records it.

The two-state design's later behaviour is instructive. Having answered the first conflict, it gives the line up entirely and is invalid by the time the second conflict arrives, so it answers one of two rather than both. The failure is not uniform, which is why it is intermittent in the lab.

Evidence to demand. The complete state list, including every transient one, and for each: which request enters it, which response leaves it, and what it does to a conflict while occupied. A state diagram with no transient states is either a very simple protocol or an incomplete diagram.

What escapes. A conflicting request answered from an ownership that had not been granted — so two agents both believe a transfer succeeded.

How DV proves it. Hold the response and drive conflicts into the window. A test that supplies the response immediately never occupies the transient state, and supplying it immediately is what a directed test does.

Telemetry. Conflicts refused while transient, as a rate. A design that has never refused one has either never been contended or has no transient state.

Misleading evidence. A protocol description with three states. Three states is what the steady behaviour needs; the transient ones are usually left out of the diagram and present in the RTL, or left out of both.

12. Review Item 7 — Two Requests, One Line: What Decides The Order?

Under review. The ordering point, and what the design compares to decide whether it is needed.

Invariant at risk. Coherency for a line is decided at exactly one place.

Where it lives. The comparison.

The trade. A design that serialises everything is slow and correct. A design that serialises nothing is fast and wrong. A design that decides by comparing something other than the line address is the one under review — and the comparison is where the bug lives.

// RTL 7 - two requesters, one line, and the ordering point.
//
// Coherency for a line is decided at ONE place. Two requests for the SAME line
// must be serialised there; two requests for DIFFERENT lines need not be, and
// serialising them costs throughput for nothing.
//
// A design that serialises everything is slow and correct. A design that
// serialises nothing is fast and wrong. A design that decides by comparing the
// line addresses is the one under review - and the comparison is where the bug
// lives.
//
//   BAD  : grant both whenever they are not bit-identical requests
//   GOOD : grant both only when the LINE addresses differ
//
// TEACHING MODEL.
module same_line_order #(parameter int NO_LINE_COMPARE = 0) (
  input  logic clk, rst_n,
  input  logic       req_a, req_b,
  input  logic [3:0] line_a, line_b,
  input  logic [1:0] op_a, op_b,
  output logic       line_same, both_granted, serialised,
  output logic [1:0] granted_id,
  output logic [7:0] n_grants, n_parallel, n_same_line_parallel,
  output logic       conc_err
);
  assign line_same = (line_a == line_b);
  // The whole review point. The lenient build compares the OPERATIONS rather
  // than the lines, so two different operations on the same line run together.
  assign both_granted = (NO_LINE_COMPARE != 0)
                      ? (req_a && req_b && (op_a != op_b))
                      : (req_a && req_b && !line_same);
  assign serialised  = req_a && req_b && !both_granted;
  assign granted_id  = req_a ? 2'd0 : (req_b ? 2'd1 : 2'd2);
  // SAFETY VIOLATION: two requests for the SAME line were granted together, so
  // no single point decided the order of the two.
  assign conc_err = both_granted && line_same;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_grants <= 8'd0; n_parallel <= 8'd0; n_same_line_parallel <= 8'd0;
    end else begin
      if (req_a || req_b) n_grants   <= n_grants + 8'd1;
      if (both_granted)   n_parallel <= n_parallel + 8'd1;
      if (conc_err)       n_same_line_parallel <= n_same_line_parallel + 8'd1;
    end
  end
endmodule

The measurement. Two requests for line 5, carrying different operations:

same line, different ops : line_same=1 line_cmp_grants=0 op_cmp_grants=1

Both builds know the lines are the same. The line-comparing build serialises them. The operation-comparing build grants both, because the operations differ — so nothing decided which of the two happened first.

The accidental agreement is the dangerous part. The run drives two identical operations on one line, and the operation-comparing build serialises them correctly. A test suite built from repeated identical operations reports both designs correct, and repeated identical operations are exactly what a simple stress test generates.

Different lines cost nothing. Both builds grant in parallel and neither is a violation, which is the throughput argument for having the comparison at all.

Evidence to demand. The exact expression the ordering decision is made on. Then ask what it compares when the two requests differ in every field except the line. An ordering decision that reads any field other than the line address is a finding.

What escapes. Two agents both granted a line, with no ordering point — so the outcome depends on arrival timing at a place that was never designed to arbitrate.

How DV proves it. Two requests, same line, different operations, in the same cycle. The identical-operation case passes in both builds.

Telemetry. Same-line parallel grants. Must read permanently zero. Parallel grants overall are a throughput metric and should be high.

Misleading evidence. Excellent parallelism figures. The broken design is genuinely more parallel.

13. Review Item 8 — Deadlock, Livelock And Starvation Are Three Failures

Under review. The progress monitor, and which of the three it can see.

Invariant at risk. None of them — all three are liveness failures, and no safety property is violated by any of them. That is what makes them hard.

Where it lives. The monitor's trigger condition.

// RTL 8 - deadlock, livelock and starvation are three different failures.
//
//   DEADLOCK   : nothing moves and nothing ever will. No forward progress
//                anywhere, and the system is quiet.
//   LIVELOCK   : everything moves and nothing completes. Retries fire forever,
//                the fabric is busy, and no transaction finishes.
//   STARVATION : the system makes progress and one agent never does.
//
// A monitor that watches only for "no activity" finds the first and is blind to
// the other two, which are the ones a busy machine actually produces.
//
// TEACHING MODEL. Sequential.
//   Safety   : none of these is a safety failure. All three are liveness.
//   Liveness : a request completes - ASSUMING the retry budget is finite and
//              the arbiter rotates. Both assumptions are withdrawable here.
module progress_monitor #(parameter int QUIET_MEANS_STUCK = 0) (
  input  logic clk, rst_n,
  input  logic       any_activity, any_completion, req_live,
  input  logic [7:0] limit,
  output logic [7:0] age, retries, n_reported, n_true_stall,
  output logic       deadlock, livelock, starved, reported,
  output logic       live_err
);
  logic [7:0] age_q, rty_q;
  logic       truly_stalled;

  assign age     = age_q;
  assign retries = rty_q;
  // Nothing is moving at all.
  assign deadlock = req_live && (limit != 8'd0) && (age_q >= limit) && !any_activity;
  // Plenty is moving and nothing is finishing.
  assign livelock = req_live && (limit != 8'd0) && (age_q >= limit) && any_activity;
  assign starved  = req_live && (limit != 8'd0) && (rty_q >= limit);
  // The truth: a live request that has not completed inside the bound, however
  // busy the fabric is. Computed identically in both builds.
  assign truly_stalled = req_live && (limit != 8'd0) && (age_q >= limit);
  // The whole review point.
  assign reported = (QUIET_MEANS_STUCK != 0) ? deadlock : truly_stalled;
  // SAFETY-OF-EVIDENCE VIOLATION: forward progress stopped and nothing said so.
  assign live_err = truly_stalled && !reported;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      age_q <= 8'd0; rty_q <= 8'd0; n_reported <= 8'd0; n_true_stall <= 8'd0;
    end else begin
      if (any_completion)                       age_q <= 8'd0;
      else if (req_live && (age_q != 8'hFF))    age_q <= age_q + 8'd1;
      if (any_completion)                       rty_q <= 8'd0;
      else if (any_activity && (rty_q != 8'hFF)) rty_q <= rty_q + 8'd1;
      if (reported)      n_reported   <= n_reported + 8'd1;
      if (truly_stalled) n_true_stall <= n_true_stall + 8'd1;
    end
  end
endmodule

The measurement. A live request, a busy fabric, no completions, a limit of 4:

busy and stalled : age=4 retries=4 deadlock=0 livelock=1 quiet_monitor=0

This is not a deadlock and the quiet monitor is looking for one. The fabric is busy, the retries are firing, nothing is completing, and the monitor that watches for absence of activity reports nothing.

The quiet monitor is incomplete, not useless, and the run proves that too: when the fabric genuinely goes quiet, it fires. It catches the idle failure and misses the busy one — and the busy one is the one a loaded machine produces.

The retry counter follows activity, not liveness, which the run asserts explicitly: at the deadlock step the age keeps advancing and the retry count does not. Those are two different quantities and a monitor that conflates them cannot distinguish livelock from deadlock.

Evidence to demand. For each of the three failures, the specific signal that would report it. Three answers, or the design can see fewer than three.

What escapes. Hangs under load, which is when hangs happen.

How DV proves it. Drive each of the three separately: busy with no completion, quiet with no completion, and progress everywhere except one agent. A single hang test finds one of three.

The withdrawal. With the limit at zero every claim is withdrawn: the request ages indefinitely, nothing is reported, and no safety property is violated — which the run asserts. A monitor with its limit disabled is a configuration state a review must ask about.

Telemetry. Age distribution, retries-per-transaction as a distribution, and per-requester waits. Retries as a total cannot distinguish a thousand retries over a thousand transactions from a thousand on one.

Misleading evidence. Every aggregate metric during starvation. Utilisation, throughput and average latency are all healthy.

14. Review Item 9 — What Does Recovery Do To The Directory?

Under review. Reset, error recovery, link retraining, hot-remove — every path that changes which agents exist.

Invariant at risk. After recovery, no line is owned by an agent that is gone.

Where it lives. What the recovery path does to the ownership record.

The failure. A recovery that clears the fabric and leaves the directory intact produces an orphaned line: permanently owned by an agent that will never respond, and therefore permanently unobtainable by anybody else. No error is raised. The line simply stops being available.

// RTL 9 - recovery, and the line that is still owned by an agent that is gone.
//
// Reset and error recovery must leave the coherency state consistent with the
// agents that actually exist afterwards. A recovery that clears the fabric but
// leaves the directory intact produces an ORPHANED line: permanently owned by
// an agent that will never respond, and therefore permanently unobtainable by
// anybody else.
//
//   BAD  : on recovery, clear the queues
//   GOOD : on recovery, reclaim every line owned by an agent that is gone
//
// TEACHING MODEL. Sequential.
//   Safety : after recovery, no line is owned by a departed agent.
module recovery_reclaim #(parameter int KEEP_DIRECTORY = 0) (
  input  logic clk, rst_n,
  input  logic       grant, recover,
  input  logic [1:0] agent,
  input  logic [3:0] agents_alive,
  output logic [3:0] owned_by,
  output logic [7:0] n_recoveries, n_reclaimed, n_orphans,
  output logic       orphan_now, reclaim_now,
  output logic       rec_err
);
  logic [3:0] own_q, own_next;
  logic [3:0] orph;

  // ONE assignment to the ownership vector, computed from BOTH events. Written
  // as two separate `if` statements - a bit-set for the grant and a full-vector
  // reclaim - the reclaim is later in source order and silently discards a
  // grant that lands in the same cycle. That is 30.2 section 7's defect, and
  // the baseline here found it before any mutation ran.
  always_comb begin
    own_next = own_q;
    if (grant) own_next[agent] = 1'b1;
    if (recover && (KEEP_DIRECTORY == 0)) own_next = own_next & agents_alive;
  end

  // A line owned by an agent that is no longer alive.
  assign orph       = own_q & ~agents_alive;
  assign owned_by   = own_q;
  assign orphan_now = (orph != 4'd0);
  assign reclaim_now = recover && (KEEP_DIRECTORY == 0) && (orph != 4'd0);
  // SAFETY VIOLATION: recovery completed and a line is still owned by an agent
  // that is gone. Nobody will ever obtain it again.
  assign rec_err = orphan_now && !reclaim_now && recover;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      own_q <= 4'd0; n_recoveries <= 8'd0; n_reclaimed <= 8'd0; n_orphans <= 8'd0;
    end else begin
      own_q <= own_next;
      if (recover) n_recoveries <= n_recoveries + 8'd1;
      if (reclaim_now) n_reclaimed <= n_reclaimed + 8'd1;
      if (rec_err)     n_orphans   <= n_orphans + 8'd1;
    end
  end
endmodule

The measurement. Agents 1 and 2 own lines. Agent 2 departs. A recovery runs:

recovery with agent 2 gone : reclaiming=1 keeping=0

The recovery itself ran identically in both builds — one recovery, counted once, in each. The reclaiming build leaves only agent 1's ownership standing. The keeping build still shows agent 2 owning a line, and every future request for that line will wait for a response from an agent that does not exist.

Both builds detect the orphan. orphan_now is high in both. The keeping build knows, and does nothing, which is the same shape as sections 7 and 10 — the information is present and the action is missing.

The boundary is the honest test. With every agent departed, the reclaiming build empties the directory and the keeping build believes in two owners of lines nobody can reach.

Evidence to demand. For every recovery path, the list of state it touches, checked against the list of state that names an agent. The gap is the finding, and it is found by reading rather than by testing.

What escapes. Lines that become permanently unavailable, one per recovery event, accumulating — so a system that has recovered often enough loses capacity it never gets back and reports no error at any point.

How DV proves it. Grant lines, remove an agent from the live set, recover, and require the directory to contain no entry naming a departed agent.

Telemetry. Orphan count after recovery — must read permanently zero — and reclaims per recovery, which should be non-zero exactly when an agent departed.

Misleading evidence. A recovery that completes quickly and reports success. It did complete. It completed the part it knew about.

Figure 3 — the recovery ran in both paths and counted once in both. Nothing distinguishes them at the recovery itself: same event, same count, same completion. The difference is a single filter by the live agent set, and its absence costs one line per departure, permanently, with no error raised at any point.

15. The Review Assembled

Nine dimensions, one summary — and the same trap 30.1, 30.2 and 30.3 each found at their own level.

// RTL 10 - a coherency review assembled. Nine review dimensions, one summary.
// "The protocol is coherent" is bit 0: a claim, and one sixth of a review.
module coherency_signoff #(parameter int COHERENT_IS_CLAIMED = 0) (
  input  logic clk, rst_n,
  input  logic        review,
  input  logic        protocol_coherent, authority_single, writers_excluded,
  input  logic        acks_conserved, identities_epoched, recovery_reclaims,
  output logic [5:0]  fail_mask,
  output logic [15:0] conditions_met, sound_pct,
  output logic        sound,
  output logic [7:0]  n_reviews, n_sound, n_claimed,
  output logic        coh_err
);
  logic [31:0] s_q;
  logic        truly_sound, claimed;
  assign fail_mask[0] = ~protocol_coherent;
  assign fail_mask[1] = ~authority_single;
  assign fail_mask[2] = ~writers_excluded;
  assign fail_mask[3] = ~acks_conserved;
  assign fail_mask[4] = ~identities_epoched;
  assign fail_mask[5] = ~recovery_reclaims;
  assign conditions_met = {15'd0, protocol_coherent} + {15'd0, authority_single}
                        + {15'd0, writers_excluded} + {15'd0, acks_conserved}
                        + {15'd0, identities_epoched} + {15'd0, recovery_reclaims};
  assign s_q = ({16'd0, conditions_met} * 32'd100) / 32'd6;
  // No clamp: six one-bit values over six cannot exceed a hundred.
  assign sound_pct = s_q[15:0];
  assign truly_sound = (fail_mask == 6'd0);
  assign claimed = (COHERENT_IS_CLAIMED != 0) ? protocol_coherent : truly_sound;
  assign sound = claimed;
  assign coh_err = review && !truly_sound && claimed;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reviews <= 8'd0; n_sound <= 8'd0; n_claimed <= 8'd0;
    end else if (review) begin
      n_reviews <= n_reviews + 8'd1;
      if (truly_sound) n_sound <= n_sound + 8'd1;
      if (claimed)     n_claimed <= n_claimed + 8'd1;
    end
  end
endmodule

The measurement. Two views of the same protocol:

epochs missing : mask=010000 met=5 sound=83%
the protocol is coherent, and nothing else : mask=111110 met=1 sound=16%

The first line is a real review with one finding open — identities are not epoch-qualified. Five of six conditions met, and the design is one mechanism away.

The second line is what Module 30 exists to prevent. The protocol is claimed coherent. Somebody said so, everybody agreed, and not one of the other five conditions was established. Sixteen percent of a review, reported as a review.

16. Quantitative Reasoning

Every figure here is a teaching parameter or a value derived from one and asserted by the testbench. None is a measurement of a real system, and none is a CXL specification number.

Directory storage, derived. For L tracked lines with A agents, an owner-plus-sharers record costs L × (ceil(log2 A) + 1 + A) bits — the owner index, its valid bit, and the sharer mask. At L=1024 and A=8 that is 1024 × (3 + 1 + 8) = 12,288 bits. A holders-only record costs L × A = 8,192 bits. The owner field is four bits per line, and those four bits are the entire difference between section 6's two builds.

The epoch field wraps. A four-bit epoch admits sixteen rounds, so an acknowledgement stale by exactly sixteen rounds aliases onto the current epoch and is accepted by a correct matcher. The run asserts the wrap. Widening to eight bits costs four flops per tracked round and pushes the alias to 256.

One stale acceptance costs three counts. The run measures it: the count-any build records three counted acknowledgements for one real answer — the stale one, the real one that follows and is then mis-scored as a duplicate, and the explicit duplicate. The qualified build records one. The ratio is not a factor of two; it is a cascade.

Phantom capacity after recovery. One departed agent owning one line, kept in the directory, is one line permanently lost per departure. Over N recovery events with one departure each, N lines are gone, and the run drives the extreme: with every agent departed, the keeping build believes in two owners of lines nobody can reach while the reclaiming build's directory is empty.

The acknowledgement equation at work. Three invalidations sent and two received leaves one outstanding, so the balanced build refuses. The run also drives a round whose invalidations are sent over two cycles — two sends of two is four — because a single-cycle send cannot distinguish an accumulating rule from a replacing one. That distinction was a mutation survivor; section 19 records it.

The starvation arithmetic. With an eight-bit age and a limit of 4, the age reaches the bound in four cycles and saturates at 255 rather than wrapping — the run drives 262 cycles to prove it. A wrapping age reports a small number for a very old transaction, which is 30.2 section 9's truncation defect arriving in a liveness monitor.

The overlap window. Two readers left in place across an exclusive grant is two stale copies live for as long as the writer holds the line. The overlap-cycle counter measures the window in cycles, and the invalidating build's reads zero across the entire run.

The sign-off arithmetic. Six conditions; five met is 5 × 100 / 6 = 83 percent under integer division, and one met is 100 / 6 = 16 percent.

17. Verification Method

Order of work

compile → inspect warnings → legal baseline → reset → boundaries → simultaneous events → abuse and error cases → configuration contrasts → structural gates → PASS → mutation campaign

Every campaign in this chapter ran against a green baseline, and the baseline was re-run after every model and testbench modification before the campaign was re-run.

Independent oracles

chkv prints got against expected, and in this chapter it caught two wrong oracles — both mine, and both made the chapter more accurate. Section 19 records them.

X and Z rejected explicitly

chk(c, …) tests c !== 1'b1, so an X-valued condition fails rather than passing. chkv(got, exp, …) reduces the result and reports an explicit X/Z failure before comparing. This is 30.3 section 6's review item applied to this chapter's own harness.

Pulses are latched, never sampled

Every safety output — auth_err, excl_err, dirty_err, ack_err, id_err, trans_err, conc_err, live_err, rec_err, coh_err — is caught by a continuous always @(posedge clk) monitor into a sticky bit, asserted outside any conditional, in a window containing a clock edge.

Stimulus never lands on the active edge

step_clk is @(posedge clk); #1;. Every stimulus change lands one delta after the edge, never on it.

Both builds are always instantiated

Every model has both its measured and lenient build wired to the same stimulus and contrasted in the same simulation. In eight of the ten, the lenient build detects the violation and declines to act on it — the error outputs, the detection flags and the truth counters are computed identically. That is deliberate: the difference under review is never the information available, always what the design does with it.

Safety, liveness and performance kept apart

Safety — authority is single-valued; no read coexists with a writer; the newest value is never dropped; ownership never moves with acknowledgements outstanding; no stale or duplicate acknowledgement is counted; no conflict is answered mid-transition; no same-line pair runs in parallel; recovery leaves no orphan. None requires an assumption.

Liveness — a stalled request is eventually reported, assuming the limit is non-zero and the clock runs. The model proves the withdrawal: at limit zero the request ages indefinitely and no safety property is violated.

Performance — a four-agent directory, a four-deep pending set, a four-cycle stall bound. These are targets. A design that misses one is slow, not incoherent.

18. Assertions

The testbenches carry 432 checks — 221 across the first five models and 211 across the last five.

Every output of every model is asserted as a value, in both builds. The output-listing gate reports zero unasserted output nets across the ten models — after closing 21 of them, which section 19 records.

Every simulator-derived value printed to the reader is asserted. The displayed-value gate scans 41 printed references and reports zero unasserted derived values. One printed name is a testbench-driven input and is reported apart.

Reset is verified with live state: with a line owned, with a round in flight, with reviews recorded, and with a request outstanding.

Simultaneous events are driven: an exclusive grant with a sharer addition, a fill with an eviction, a round start with an acknowledgement, a start with a finish, and — the one that mattered — a grant with a recovery. Section 19 records the RTL defect that last case found.

Abuse cases are driven and asserted to be no-ops or refusals: a write with no owner, a write from an agent that never took the line, a modify of an invalid line, an evict of an invalid line, an acknowledgement with nothing outstanding, a response with no request pending, a conflict against an invalid line, a single requester where a pair is expected, neither requester asking, a finish with nothing active, and a recovery with every agent alive.

Boundaries are driven at the edge and one step past it: an epoch at its wrap point, an age at saturation, a starvation limit of zero, a timeout limit of zero, zero invalidations to send, line 0 against line 0 and line 15 against line 15, a clean eviction, and every agent departing at once.

Configuration contrasts are explicit. Every model instantiates both builds and asserts the observable differs.

19. Baseline Defects Found Before Mutation

RTL defect 1 — a simultaneous grant and recovery lost the grant

Symptom. With a grant and a recovery driven in the same cycle, the ownership vector read 0 where it should have read 8. The check that caught it was the simultaneous-events case, which is the last thing the stimulus drives.

Root cause. The ownership vector was written by two separate statements inside one clocked block — a bit-set for the grant, and a full-vector reclaim for the recovery. Both are correct alone. When both fire, the second is later in source order and the whole-vector assignment discards the bit-set entirely.

Fix. One assignment, computed from both events in an always_comb that applies the grant first and then filters by the live set.

Why it matters. This is 30.2 section 7's defect — the same shape, two chapters later, written by somebody who had just finished writing that chapter. The failure mode here is worse than a miscount: a line granted during a recovery window is silently never granted, and the requester waits forever for a response to a transaction the directory has no record of.

RTL defects 2 and 3 — found in the final adversarial review

Defect 2 — a reader joining in the same cycle as an exclusive grant survived it. The read set was written by two independent statements: an invalidation under the grant, and a join under the reader mask. The join came last, so a reader arriving in the grant cycle overwrote the invalidation and stayed live — producing, in the build that is supposed to be correct, exactly the defect section 7 exists to show.

Fix. One assignment, with the invalidation applied last so it also catches a reader that joins in the grant cycle, and the priority written down.

Defect 3 — a send in the cycle a transfer closed the round was discarded. The round counters were written by two independent statements and the transfer's clear came last. A set of invalidations issued in that cycle — opening the next round — was thrown away, so the next transfer saw a balanced equation it had never earned. That is section 9's escape, reached through the accounting.

Fix. One assignment for each counter, with the priority written down: the transfer closes the round and clears both; a send in that cycle opens the next round and survives the clear; an acknowledgement in that cycle answers the round that just closed and is dropped.

Verification. Both simultaneous cases are now driven and asserted, and three mutations covering the priorities are killed.

How it was found. Not by the stimulus, not by the campaign, and not by any of the structural gates. It was found by a static sweep of every model in the batch for a register written by two independent top-level statements — the exact shape this batch teaches — run as part of the final adversarial review. Five of the thirty models in the batch had it, and in every one the simultaneous same-target case was undriven and the priority unwritten.

The general lesson. A bit-set and a bit-clear on the same vector look independent because they usually name different indices. They stop being independent the moment the two indices are equal, and nothing in the source says whether that can happen. The rule from 30.2 section 7 — one assignment computed from all events, or a written priority — applies to indexed writes exactly as it does to whole registers.

Testbench defects — none

Wrong oracles — two, both mine

One — the duplicate count in the lenient build. I expected one; it is two. The lenient build had cleared a peer's pending bit with the stale acknowledgement, so the legitimate current-epoch answer that followed also looked like a duplicate to it. Accepting one stale answer manufactures a second fault, which is a better lesson than the one I had written down and is now section 10's headline.

Two — the quiet monitor's report count. I expected zero at the genuine-deadlock step. It is one: the fabric had gone quiet by then, so the quiet monitor does fire. It missed the busy stall and catches the idle one. Incomplete, not useless — and section 13 now says so because the run said so.

Both were caught because chkv prints got against expected. A bare equality would have reported a design failure in both cases, and the natural repair would have been to change a correct design.

Coverage gaps found by the structural gates, before any mutation ran

Compiler-warning findings

Under -Wall the ten models produce no truncation, select-width, signedness, cast, multiplication-width, shift-width or loop-width warnings. The only warning is a missing timescale on models containing no delay constructs at all — inspected and recorded as benign rather than silenced. The absence is a checked result, not an assumption.

Simulator constraints

Icarus Verilog 13.0 rejects ref task arguments, carried forward from 29.5, 30.1, 30.2 and 30.3.

20. Mutation Testing

98 mutations attempted. 2 withdrawn as equivalent. 96 non-equivalent mutations injected, 96 killed. Zero unexplained survivors.

By model:

Nine survivors across the two first runs, every one classified before anything was changed.

Four stimulus gaps of one family

Three of the four are the same shape: a structure that was only ever populated once, so no update rule could be distinguished from any other.

A structure populated exactly once cannot distinguish assignment from accumulation, and every one of these mutations changes only that. It is a gap worth looking for by inspection: if a structure is only ever written in one cycle of the whole run, its update rule is untested.

Three missing checkers

The dirty bit after an eviction. The case was driven — a dirty line was evicted — and only valid_q was asserted afterwards. The mutation left the dirty bit standing and nothing looked.

The grant counter around a single requester. The single-requester abuse case was driven and the counter was never asserted around it.

The retry counter at the deadlock step. A live request against a quiet fabric was driven — that is the deadlock case — and the retry counter was not asserted there. The mutation made retries follow liveness instead of activity, and the two quantities are equal in every other cycle of the run.

All three had the state and lacked the assertion, which is the most common survivor class in this batch and the cheapest to fix.

Two equivalent mutants — a dominated guard the tooling did not see

Both survivors in the transient-state model were equivalent for the same structural reason, and both point at the same thing: !transient_now beside st_q == OWNED is a guard that can never be false. transient_now is (st_q == PENDING) in the three-state build and a constant zero in the two-state one, so it cannot be true while the state is OWNED. The term is documentation, not logic.

Withdrawn. Not counted as kills.

domcheck reported zero dominated guards on this chapter. It looks for a clamp or guard dominated by an enclosing condition inside one statement; this domination runs between a continuous assignment's term and a state comparison beside it, which it does not model.

This is the fourth distinct way a structural tool in this batch has reported a confident zero on something it could not read — after a changed assertion idiom in 29.5, a changed net name in 30.1, a changed counter suffix in 30.2. The value of these tools is now known to be "a hit is real", not "a zero is clean", and that is a weaker guarantee than the one they appear to offer.

The guards are kept. A reviewer reading the OWNED arm should see the intent without deriving the domination, and the cost is nothing. What is not acceptable is counting the two mutations as kills.

Equivalent mutants across the batch

Three chapters, three equivalent mutants, three different reasons:

None of the three could be settled by running more tests, and none should have been "fixed" by adding an assertion. Each required a proof, and the proof is the deliverable.

Survivor classification comes before any fix

Mutation testing is invalid unless the unmutated baseline passes first, and a higher kill count is stronger evidence only if the baseline it was measured against was green.

21. Synthesis And Implementation Reality

The owner field is the cheapest mechanism in this chapter. For eight agents it is three bits plus a valid bit per line, against a sharer mask of eight. Four bits per line buys single-valued authority outright, and nothing else in section 6 changes.

The invalidation that accompanies an exclusive grant costs a vector clear, which is free in a register file and a multi-cycle operation in a large directory RAM. That cost is the usual reason the lingering build exists — somebody made the grant single-cycle by deferring the clear, and deferring it is exactly the defect.

The write-back path costs a buffer and a queue slot, and its real cost is the ordering constraint: the line may not be reused until the write-back is accepted. A design that invalidates first and writes back second is faster and has a window in which the newest value exists nowhere.

The acknowledgement counters are two counters and a comparator per outstanding round. For a single-round-at-a-time controller that is two eight-bit counters. The comparator sits outside the datapath, so it costs area rather than timing, which makes it one of the few coherency self-checks worth leaving in production silicon.

The epoch field costs E flops per round context. Four bits gives sixteen rounds of separation and eight gives 256. The alias window is the design decision, and it should be compared against the maximum lifetime of a response in the fabric — an acknowledgement that can outlive sixteen rounds needs a wider epoch, not a faster fabric.

Transient states cost encodings, and encodings cost nothing until they cost a bit. A protocol with four steady states and four transient ones needs three bits rather than two. The default arm question from 30.2 section 6 returns here, larger: more encodings means more undefined ones.

The line comparator is as wide as the line address. For a 4-bit line index it is four XORs and an OR; for a real address it is the tag width. It is on the arbitration path, which is the argument people use for comparing something cheaper — and comparing something cheaper is section 12's defect.

The recovery filter is one AND per agent bit. For an eight-agent directory that is eight gates per line, applied once per recovery. It is the cheapest item in this chapter and the one most often absent, because recovery paths are written last.

No area, frequency or power figures appear in this chapter, because none was measured.

22. Silicon Observability

Six counters here must read permanently zero — unowned writes, overlap cycles, early transfers, stale counted, same-line parallel grants, and orphans after recovery. Each costs almost nothing, never fires in a correct design, and captures a safety escape that would otherwise present as corruption or unavailability far from its cause.

The pattern to read on the stale pair: a high detected count with a zero counted count is a healthy design in a busy fabric. The same detected count with a non-zero counted count is a different chip.

Write-backs against dirty evictions is the pair that catches section 8. Their difference is the number of times the newest value was dropped, and a design with the defect reports zero write-backs rather than a mismatch — so the review is "are these two numbers equal", not "is this counter zero".

Orphans after recovery is the one to keep if only one survives area review. It is a popcount of the directory ANDed against the inverse of the live set, it is evaluable at any moment, and it catches a failure that produces no error and no hang — only a line that quietly stops being available.

23. DebugLabs

Lab 1 — Two agents write one line and the directory shows one entry

Symptom. Memory corruption traced to two agents writing the same line. Every inspection of the directory shows the line held.

Evidence. The directory is a bitmask of holders. Two bits are set. Nothing names an owner.

Hypothesis. The structure cannot answer which holder is authoritative.

Investigation. Trace both writes. Both were permitted, and both were permitted correctly by the rule the design implements: the writer is in the holder set.

Root cause. A set of holders is not an ownership record. It answers who has a copy, not whose copy is newest.

Fix. An owner index plus a valid bit beside the sharer mask, and a write rule that reads the owner.

Prevention. Add a second holder and have it write. A test that only writes from the agent that requested the line cannot find this.

Silicon observability. An unowned-write counter that must read permanently zero.

Lab 2 — A reader returns stale data and the single-writer assertion passes

Symptom. An agent reads a value that another agent overwrote some time ago. No error anywhere.

Evidence. The single-writer assertion has never fired. Exactly one agent holds the line for writing.

Hypothesis. The right invariant is holding and a different one is not.

Investigation. Inspect the read set at the moment of the exclusive grant. Two readers are still present.

Root cause. The grant did not invalidate the readers. Single writer holds; exclusion does not.

Fix. Invalidate the read copies as part of the grant, and add an overlap assertion.

Prevention. Establish readers first, then grant exclusive, then read from a former reader. The natural test order — grant on an unheld line — cannot find this.

Silicon observability. Writer-reader overlap cycles. Permanently zero.

Lab 3 — A value written by the program is not in memory

Symptom. A program writes a value, the line is evicted under capacity pressure, and a later read returns the value from before the write.

Evidence. The eviction completed. The line is invalid. The tags are consistent. Nothing is corrupt.

Hypothesis. The eviction dropped the newest data.

Investigation. Compare the write-back count against the dirty-eviction count. The first is zero.

Root cause. The eviction path invalidates and does not write back. The structure is perfectly consistent and the data is gone.

Fix. Write back before invalidating, and assert the two counts are equal.

Prevention. Fill, modify, evict, then read memory. Asserting that the line went invalid proves the eviction ran, not that it preserved anything.

Silicon observability. Write-backs against dirty evictions. The failing design reports zero write-backs, not a mismatch.

Lab 4 — An exclusive grant completes while a copy is still live

Symptom. An agent granted exclusive access finds its writes disagreeing with another agent's reads for a short window after every transfer.

Evidence. Transfer latency is excellent. The invalidation count and the acknowledgement count differ.

Hypothesis. The transfer is not waiting for the acknowledgements.

Investigation. Sample the outstanding count at the moment of transfer. It is non-zero on a fraction of transfers proportional to load.

Root cause. The transfer fires on the request rather than on the balance.

Fix. Gate the transfer on sent == received, and clear both counters together at the end of the round.

Prevention. Send N invalidations, acknowledge N−1, request the transfer, require a refusal — and then acknowledge the last one and require the transfer to proceed.

Silicon observability. Acknowledgements outstanding at transfer. Permanently zero.

Lab 5 — An invalidation round completes and a copy was never dropped

Symptom. The same failure as Lab 4, on a design whose acknowledgement equation is implemented correctly and passes review.

Evidence. The equation balanced at the transfer. One peer's copy was still live.

Hypothesis. The equation was balanced by an acknowledgement from a previous round.

Investigation. Stamp acknowledgements with an epoch. The balancing answer carries the previous one.

Root cause. Acknowledgements are counted on identity alone. A retry created a second round, and the first round's late answer satisfied the second.

Fix. An epoch advanced by every round, and a counting rule requiring epoch, identity and still-pending.

Prevention. Start a round, start another, then deliver an acknowledgement stamped with the first. Then watch what happens to the real answer when it arrives — it will be mis-scored as a duplicate, which is the second symptom.

Silicon observability. Stale detected against stale counted. The second is the escape.

Lab 6 — Two agents both believe a transfer succeeded

Symptom. Two agents each report exclusive ownership of one line, after a burst of contention.

Evidence. Both transfers were answered. Both answers were consistent with the state each agent's controller was in.

Hypothesis. One of them answered from a state it had not yet reached.

Investigation. The controller has no encoding for "requested, not yet granted". It marks the line owned on the request.

Root cause. A missing transient state. A conflict arriving between request and response is answered on the strength of an ownership that has not been granted.

Fix. An explicit transient state that refuses conflicts and is exited only by its response.

Prevention. Hold the response and drive conflicts into the window — for more than one cycle. A transient state is exited by its response, not by time, and a test that spends one clock there cannot tell the difference.

Silicon observability. Conflicts refused while transient, as a rate. A design that has never refused one has either never been contended or has no transient state.

Lab 7 — Excellent parallelism and an occasional corrupted line

Symptom. Rare corruption on hot lines, under contention, with very good aggregate throughput.

Evidence. The arbiter's parallel-grant rate is high. Corruption correlates with lines that two agents touch.

Hypothesis. Two requests for one line are being granted together.

Investigation. Read the ordering decision. It compares the operation fields, not the line address.

Root cause. Two requests for one line carrying different operations are granted in parallel, so nothing decided which happened first.

Fix. Compare the line address.

Prevention. Two requests, same line, different operations. The identical-operation case passes in the broken design, and identical operations are what a simple stress test generates.

Silicon observability. Same-line parallel grants. Permanently zero, while parallel grants overall stay high.

Lab 8 — A fabric hangs under load and the hang detector is silent

Symptom. A hang reproduces under sustained load. The hang detector never fires, and it fires correctly in a bring-up test where the fabric is idle.

Evidence. During the hang the fabric is extremely busy. Retries are firing continuously.

Hypothesis. The detector is looking for deadlock and this is livelock.

Investigation. Instrument three separate conditions: no activity, activity without completion, and per-agent progress. The second is true throughout.

Root cause. The monitor triggers on absence of activity. Livelock is the opposite of absence of activity.

Fix. Age the oldest outstanding request and report on the age, independently of fabric activity. Keep the quiet detector — it catches the idle failure the new one catches too, and it is not wrong, it is incomplete.

Prevention. Drive all three failures separately. A single hang test finds one of three.

Silicon observability. Oldest-request age as a distribution, and retries-per-transaction as a distribution. Retries as a total cannot distinguish a thousand retries over a thousand transactions from a thousand on one.

24. The Review, As A Working Checklist

Every row is a question with a wrong answer that sounds fine. "The directory tracks it", "the readers get invalidated", "the transfer waits", "the tag is unique", "there are three states", "the watchdog covers it", "recovery clears everything" — each of those ends a review, and each is in this chapter as a defect.

25. How This Appears In Real Engineering

The holders-only directory is a storage optimisation that became a protocol. A bitmask is smaller and simpler and answers the question the first version of the design needed, and the owner field is the thing that gets dropped in the area review.

The lingering reader comes from making the grant fast. Deferring the invalidation shortens the grant path, the deferral is supposed to be resolved before any read, and under contention it is not.

The dropped write-back comes from the eviction path being written for clean lines first. The dirty case is added later, and the ordering between write-back and invalidation is decided by whichever is easier to insert.

Early transfer is a latency optimisation with a plausible argument behind it. Waiting for the slowest peer sets the transfer latency, and somebody measures the improvement from not waiting and does not measure what it costs.

Identity-only counting survives because it works until the first retry. Environments that never model retry never exercise identity reuse across rounds, and retry modelling is usually the last thing added.

Missing transient states come from the protocol diagram. The diagram shows the steady states because that is what a diagram is for, and the RTL is written from the diagram.

Comparing the wrong field in the ordering decision is a timing fix. The line comparator was on the critical path, something cheaper was substituted, and the substitution was correct for the traffic in the test suite.

Quiet-only hang detection comes from bring-up. During bring-up the fabric is idle when it hangs, the detector works perfectly, and it is never revisited.

Recovery leaving the directory intact is the commonest of all, because recovery paths are written last, tested least, and reviewed by whoever is left.

26. Common Misconceptions

"Coherence and consistency are the same thing." Coherence is about one line: is this the newest value? Consistency is about ordering across different locations. A coherent system can have a weak consistency model by design; an incoherent one is always broken.

"The directory tracks who has the line." That is a different question from who has the newest value, and the difference only appears when somebody writes.

"There is one writer, so it is correct." Single writer and writer-reader exclusion are two invariants. A design can satisfy the first and violate the second, and the violation is quieter.

"The eviction completed successfully." It did. The structure is consistent and the data is gone. Ask what memory holds, not what the tags hold.

"The transfer waited for the acknowledgements." For how many? A design that transfers on the first acknowledgement also waited.

"The tag is unique." Within a round, yes. Across rounds, no — and a retry is exactly the event that creates a second round.

"One stale acknowledgement costs one acknowledgement." It costs three: the stale one, the real one that follows and is mis-scored as a duplicate, and every count derived from both.

"The protocol has three states." Three steady states. Ask about the transient ones, and whether they are in the RTL, the diagram, both, or neither.

"A transient state lasts one cycle." It lasts until its response arrives. A test that supplies the response immediately never occupies it, which is why the missing second cycle was a mutation survivor here.

"We serialise conflicting requests." On what comparison? An ordering decision that reads any field other than the line address is a finding.

"The hang detector covers it." Which of the three? Deadlock, livelock and starvation need three answers, and a detector that watches for quiet finds the one that a loaded machine does not produce.

"Recovery cleared everything." It cleared what its branch assigns. The directory names agents, and recovery changes which agents exist — the intersection is the finding.

"Every aggregate metric is healthy." That is the signature of starvation, not evidence against it.

27. Interview And Design-Review Questions

Coherence, consistency and authority

1. State the difference between coherence and memory consistency. Coherence is about a single location: is this the newest value? Consistency is about the order in which operations across different locations become visible.

2. Can a system be coherent and have a weak consistency model? Yes, and that is a documented design decision. The reverse — a strict consistency model over an incoherent fabric — is always a bug.

3. Why can a set of holders not answer the coherency question? It records who has a copy. The question is whose copy is newest, and the set carries no field that answers it.

4. What does adding an owner field cost? For eight agents, three bits plus a valid bit per line — against a sharer mask of eight. Four bits buys single-valued authority outright.

5. "The first bit set is the owner." What is wrong with that? It is an ordering imposed by the reader on a structure that does not carry one. Two different readers can disagree.

6. A directory always shows exactly one holder in test. What does that prove? That the test never created a second holder.

Exclusion and ownership of data

7. Name the two invariants that "one writer" is usually collapsed into. Single writer — at most one agent may write. Exclusion — while an agent may write, no other may read.

8. Give a state that satisfies the first and violates the second. One writer with two read copies left live across the grant.

9. Which of the two is quieter in the field? The exclusion violation. It is not a write-write race; it is a reader holding a value that is no longer current, and no error is raised.

10. Who owes the write-back on a modified line? Whoever holds the newest form of it, before dropping it.

11. Why is a dropped write-back hard to find? Nothing is inconsistent. The eviction completed, the tags are clean, and memory returns a plausible value that happens to be the old one.

12. What ordering does an eviction of a dirty line require? Write back, then invalidate. The reverse has a window in which the newest value exists nowhere.

13. Which two counters catch it, and why not one? Write-backs and dirty evictions. The failing design reports zero write-backs, so the review is "are these equal", not "is this zero".

Acknowledgements and identity

14. What permits an ownership transfer? Invalidations sent equalling acknowledgements received, checked before the transfer.

15. Three of three acknowledgements for a line with no sharers — what should the mechanism do? Transfer immediately. Zero invalidations balance trivially, and a mechanism that cannot tell "nothing to wait for" from "not waiting" stalls every uncontended transfer.

16. Why is an early transfer faster? Because it skipped the wait. The latency improvement is real and it is the cost of the invariant.

17. What does an acknowledgement's identity tell you, and what does it not? Which request it answers. Not which round.

18. Name the event that makes identity reuse across rounds possible. A retry, a recovery, or a second invalidation of the same line — anything that starts a new round while answers to the old one are still in flight.

19. How many counts does one accepted stale acknowledgement cost? Three: the stale one, the real one that follows and is mis-scored as a duplicate, and the accuracy of every figure derived from both.

20. Which two of the four stale and duplicate counters must read zero? The counted ones. Detected is a fabric property.

21. A four-bit epoch. When does a stale acknowledgement alias onto the current round? At exactly sixteen rounds. The width should be compared against the maximum lifetime of a response in the fabric.

Transients, ordering and progress

22. Why does a line need a state between invalid and owned? Because a request has been issued and its response has not arrived, and a conflict in that window must be refused rather than answered from a state the line is about to leave.

23. What exits a transient state? Its response. Not time, and not another request.

24. A test spends one cycle in the transient state and everything passes. What is untested? Whether the state is exited by its response or by the clock. Both look the same for one cycle.

25. What must the ordering decision compare? The line address. Anything else is a finding.

26. Two requests for one line carrying identical operations. Why is that the wrong test? Because an operation-comparing design serialises them correctly, and identical operations are what a simple stress test generates.

27. Should different-line requests be serialised? No. That is throughput given away for nothing, and it is the argument for having the comparison at all.

28. Distinguish deadlock, livelock and starvation in one sentence each. Deadlock: nothing moves. Livelock: everything moves and nothing completes. Starvation: the system progresses and one agent never does.

29. Are any of the three safety failures? None. All three are liveness failures, which is exactly why safety assertions do not find them.

30. A hang detector fires in bring-up and never in the field. What is the likely cause? It triggers on absence of activity, and the field failure is livelock.

31. Why is retries-per-transaction better telemetry than total retries? A thousand retries over a thousand transactions is congestion. A thousand on one is livelock. The total is identical.

32. What is the only evidence of a liveness failure? The continued presence of something old. There is no event to count, so the telemetry is an age distribution.

Recovery, review and campaign

33. What must recovery do to a coherency directory? Filter it by the set of agents that still exist.

34. What is an orphaned line? A line owned by an agent that is gone. No error is raised; the line simply stops being obtainable.

35. Why does this defect accumulate? One line per departure, permanently, with the system continuing to run and report success.

36. What does it cost to fix? One AND per agent bit, applied once per recovery. It is the cheapest item in the chapter and the most often absent.

37. Which six counters in this chapter must read permanently zero? Unowned writes, overlap cycles, early transfers, stale counted, same-line parallel grants, and orphans after recovery.

38. A simultaneous grant and recovery lost the grant. What was the RTL defect? Two separate statements assigning one vector — a bit-set and a full-vector reclaim — where the later one in source order discards the earlier.

39. Why is that worse here than a miscount? A line granted in a recovery window is silently never granted, and the requester waits forever for a response to a transaction the directory has no record of.

40. Three structures were only ever populated once and three mutations survived. What is the general lesson? A structure written in exactly one cycle of a whole run has an untested update rule: assignment and accumulation are indistinguishable.

41. Give three distinct reasons a mutant can be equivalent. A language rule; a reachable-state invariant; a guard term dominated by a condition beside it. This batch produced one of each.

42. A structural checking tool reports zero. What must you confirm? That it read its input. Four distinct times in this batch a tool reported a confident zero on something it could not parse.

43. Why keep a guard that can never be false? It documents intent and costs nothing. What is not acceptable is counting the mutation that removes it as a kill.

44. What single condition invalidates a mutation campaign? A failing baseline.

45. Why is that error hard to notice? The number that comes back is higher.

46. If you could keep three counters from this whole chapter, which? Orphans after recovery, the write-back against dirty-eviction pair, and stale counted. The first catches a failure with no error and no hang, the second catches silent data loss, and the third catches the mechanism that defeats a correct acknowledgement equation.

28. Exercises

1 — Coherency review. You are handed a directory described as "a valid bit and a presence mask per line". Write the review finding: name the invariant at risk, the field that is missing, the evidence you would demand, the failure that escapes, and the telemetry that would expose it after tapeout.

2 — Quantitative. A directory tracks 4,096 lines across 16 agents. Compute the storage for a holders-only record and for an owner-plus-sharers record, express the owner field as a percentage of the total, and argue whether you would spend it.

3 — RTL implementation. Extend the acknowledgement model with a second concurrent round. State what must be replicated, what must not be, which new simultaneous case appears, and what the conservation equation becomes.

4 — Checker design. Write the continuous assertion that catches a reader left live across an exclusive grant. State explicitly why it must be evaluated every cycle rather than at the end of the test, and what its expected value is on an uncontended line.

5 — Mutation classification. A mutation removes && !transient_now from a guard that is already conditioned on state == OWNED, and survives. Give the separating question, classify the survivor, state what you would change, and say what you would write down.

6 — Waveform diagnosis. Using Figure 2, state what the two pending rows show at cycle 6, why the counted row never rises, and what will happen when the peer's real answer to the current round arrives. Then name the cycle at which the damage becomes visible and explain why it is not the cycle at which it was caused.

7 — Architecture reasoning. A design proposes transferring ownership after a fixed delay rather than on acknowledgement balance, arguing that the delay exceeds the worst-case acknowledgement latency. Write the review response: state what must be true for the argument to hold, what makes it false in practice, and what you would require instead.

8 — Coverage planning. Define a functional coverage model for acknowledgement identity that would find the count-any defect without anybody suspecting it. Specify the bins, the cross, identify the bin the failing design can still hit, and the bin it cannot.

29. Summary

Coherence is about one line and consistency is about ordering across locations. They are different properties with different mechanisms, and merging them in a review loses one of them.

Who has authority over the newest value now? A structure that records a set of holders cannot answer that, and the difference only appears when somebody writes.

Single writer and writer-reader exclusion are two invariants, and a design that satisfies the first while leaving readers live fails the quieter one.

A modified line exists in exactly one place, and an eviction that drops it corrupts nothing, breaks no structure, and loses the data.

Ownership moves only when the acknowledgements balance — an equation, checked before the transfer, not a delay chosen to exceed the worst case.

An acknowledgement's identity says which request, not which round. One accepted stale answer costs three counts, because the real answer that follows is then mis-scored as a duplicate.

A line in transition must refuse conflicts, and a transient state is exited by its response rather than by time.

Coherency for a line is decided at one place, and the ordering decision must compare the line address and nothing else.

Deadlock, livelock and starvation are three liveness failures and need three answers; a monitor that watches for quiet finds the one a loaded machine does not produce.

Recovery must reclaim every line owned by an agent that is gone, or the system loses a line per departure, permanently, with no error at any point.

Six conditions, and "the protocol is coherent" is one of them. A real review with one finding open is 83 percent. A claim and nothing else is 16.