Coherency Verification

25.1 asked what a passing suite proves about a protocol. This chapter asks the same question about coherency, and the answer is worse, because a coherency bug is not a property of one transaction. It is a property of two caches at the same instant, and almost every checker ever written looks at one.

The single-writer invariant is the clearest case. Two caches holding a line modified is the definition of broken — and a checker scoped to the requesting cache cannot see the second one, reports nothing, and passes. Section 5.

1. The Engineering Problem — The Bug Is In The Pair

A checker scoped to one cache cannot see a second writer. Two caches modified at once is the invariant broken, and a requester-scoped check reports zero violations of three. Section 5.

A read must be checked against the owning copy, not memory. A dirty line whose cache holds version 14 against a memory holding 10 is correct hardware and a failing check. Section 6.

A snoop filter that over-reports costs cycles; one that under-reports loses a copy. Seven false hits is 140 wasted cycles; one false miss is a coherency bug, and only one of the two is a correctness question. Section 7.

A checker that samples at transaction boundaries sees two states of six. It reports nothing missing, because it never looked between them. Section 8.

And the space a coherency bug lives in is a cross product. Four states across two caches is sixteen pairs, not four states — and a coverage report counting states closes at 100% with a quarter of the space untouched. Section 12.

This chapter against 25.1, stated precisely. That one owns whether a rule was checked at all. This one owns whether the check was wide enough to see the bug — which is why every model here is about the scope of an observation, and why section 14's weak definition is a green regression dashboard.

2. The One-Sentence Model

Coherency is verified when the single-writer invariant is checked across every cache, reads are checked against the owning copy, the snoop filter names every holder, the checker can see the states between transactions, and the cross-cache state space is closed — and "the coherency tests pass" is none of those five.

3. What This Chapter Owns

Deferred:

4. Teaching-Model Boundary

Every model is a small synchronous block isolating one scope decision. A real coherency environment is a reference model, a set of monitors, a snoop-filter mirror, a transaction matcher and a coverage database, and none of that is reproduced. What is reproduced is the arithmetic each scope decision implies, and the shape of the mistake when the scope is drawn too narrow.

Three simplifications are worth stating. Section 5 uses a four-bit occupancy mask where a real design has a directory with sharers, owners and pending states. Section 8 treats sampling as evenly spread, which a real monitor is not. Section 13 prices triage at a flat hours-per-disagreement, which is highly variable. In each case the conclusion is the same and the model is abbreviated.

Each model is built twice — a correct build and a broken build selected by a parameter. Every broken build here is a check drawn at the wrong scope: one cache instead of all, memory instead of the owner, a filter assumed exact, boundaries instead of the interior, states instead of pairs, atomic instead of overlapping. None of them is a coding error, which is why each one survives review: they are all defensible descriptions of a smaller problem.

Figure 1 — The same hardware, two scopes, two verdicts. The narrow checker is not wrong about cache 0; it is answering a question that cannot detect the bug, and it is the question most environments actually ask.

5. RTL 1 — The Single-Writer Invariant Is Not A Per-Cache Property

// RTL 1 - the single-writer invariant. At most one cache may hold a line
// modified; a checker that only inspects the requester cannot see the second.
module single_writer #(parameter int CHECK_REQUESTER_ONLY = 0) (
  input  logic clk, rst_n,
  input  logic        check,
  input  logic [3:0]  modified_mask,   // one bit per cache, 1 = holds it M
  input  logic [1:0]  requester,
  output logic [2:0]  writers, others_writing,
  output logic        invariant_holds, violation,
  output logic [7:0]  n_checks, n_violations,
  output logic        missed_violation_err
);
  logic [2:0] popc;
  logic       req_is_writer;
  assign popc = {2'd0, modified_mask[0]} + {2'd0, modified_mask[1]}
              + {2'd0, modified_mask[2]} + {2'd0, modified_mask[3]};
  assign writers = popc;
  assign req_is_writer = modified_mask[requester];
  // A checker scoped to the requester sees at most its own copy.
  assign others_writing = (CHECK_REQUESTER_ONLY != 0)
                          ? 3'd0 : (writers - {2'd0, req_is_writer});
  assign violation = (CHECK_REQUESTER_ONLY != 0)
                     ? 1'b0 : (writers > 3'd1);
  assign invariant_holds = !violation;
  // Two caches modified at once, reported as holding.
  assign missed_violation_err = check && (writers > 3'd1) && !violation;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_checks <= 8'd0; n_violations <= 8'd0;
    end else if (check) begin
      n_checks <= n_checks + 8'd1;
      if (violation) n_violations <= n_violations + 8'd1;
    end
  end
endmodule

Six checks. Four caches.

Four violations across the caches; none within one.

The invariant is a statement about the set, not about a member of it. "At most one cache holds this line modified" cannot be evaluated from inside one cache, because the quantity it constrains — how many caches — is not visible there. The requester-scoped build reports zero violations of four and is not wrong about anything it looked at.

Row three is why the narrow check cannot be patched. Two caches are modified and neither of them is the requester, so even a check that also inspected the requester's peers-in-passing would miss it. The scope has to be the whole set or the invariant is not being checked.

Row five separates the two ways a narrow check fails. Here the requester is one of the two writers, so the narrow checker has the evidence in front of it — one modified copy — and still cannot conclude anything, because one modified copy is exactly what a correct exclusive write looks like. The bug is not in what it saw; it is in what it could not see alongside it.

6. RTL 2 — A Read Is Checked Against The Owner, Not Memory

// RTL 2 - the data-value invariant. A read must return the most recent write,
// which lives in the owning cache and not necessarily in memory.
module data_value #(parameter int COMPARE_TO_MEMORY = 0) (
  input  logic clk, rst_n,
  input  logic        read_it,
  input  logic [15:0] memory_version, cache_version,
  input  logic        line_is_dirty,
  output logic [15:0] expected_version, observed_version, staleness,
  output logic        value_ok,
  output logic [7:0]  n_reads, n_stale,
  output logic        stale_reference_err
);
  // The newest copy is the dirty cache's, when there is one.
  assign expected_version = (COMPARE_TO_MEMORY != 0) ? memory_version
                          : (line_is_dirty ? cache_version : memory_version);
  assign observed_version = line_is_dirty ? cache_version : memory_version;
  assign staleness = (observed_version > expected_version)
                     ? (observed_version - expected_version)
                     : (expected_version - observed_version);
  assign value_ok = (staleness == 16'd0);
  // A dirty line checked against memory, which cannot be current.
  assign stale_reference_err = read_it && line_is_dirty
                               && (cache_version != memory_version)
                               && (expected_version == memory_version);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reads <= 8'd0; n_stale <= 8'd0;
    end else if (read_it) begin
      n_reads <= n_reads + 8'd1;
      if (!value_ok) n_stale <= n_stale + 8'd1;
    end
  end
endmodule

Five reads.

None stale against the owning copy; three against memory.

A reference model that reads memory is checking the wrong thing. In a write-back protocol the newest value is in whichever cache holds the line dirty, and memory is by definition behind. Row one is correct hardware failing a check — and the failure looks exactly like a data-corruption bug, which is how it consumes a week.

Row three is the row that makes the defect survive. Cache and memory happen to hold the same version, both references agree, and the test passes for the wrong reason. A regression made mostly of clean lines and freshly written-back ones will be green for months.

Row four is the direction people forget. A dirty cache copy behind memory is not a coherency state that should exist — but a checker computing observed − expected without an absolute value underflows and reports a staleness of 65,530 rather than 6. The invariant is a difference; differences have two directions.

7. RTL 3 — A Snoop Filter's Recall Is A Correctness Property

// RTL 3 - snoop filter precision and recall. An imprecise filter costs snoops;
// an incomplete one loses a copy, and only one of those is a correctness bug.
module snoop_filter #(parameter int ASSUME_EXACT = 0) (
  input  logic clk, rst_n,
  input  logic        lookup,
  input  logic [15:0] caches_holding, filter_says, snoop_cost_cycles,
  output logic [15:0] false_hits, false_misses, wasted_cycles,
  output logic        sound, precise,
  output logic [7:0]  n_lookups, n_unsound,
  output logic        recall_ignored_err
);
  // Over-reporting costs snoops; under-reporting loses a copy.
  assign false_hits = (filter_says > caches_holding)
                      ? (filter_says - caches_holding) : 16'd0;
  assign false_misses = (ASSUME_EXACT != 0) ? 16'd0
                      : ((caches_holding > filter_says)
                         ? (caches_holding - filter_says) : 16'd0);
  assign wasted_cycles = false_hits * snoop_cost_cycles;
  assign sound = (false_misses == 16'd0);
  assign precise = (false_hits == 16'd0);
  // A cache holding the line that the filter did not name.
  assign recall_ignored_err = lookup && (caches_holding > filter_says)
                              && (false_misses == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_lookups <= 8'd0; n_unsound <= 8'd0;
    end else if (lookup) begin
      n_lookups <= n_lookups + 8'd1;
      if (!sound) n_unsound <= n_unsound + 8'd1;
    end
  end
endmodule

Five lookups. Twenty cycles per snoop.

One unsound when recall is modelled; none when the filter is assumed exact.

Precision and recall fail in completely different currencies. A filter that names caches which do not hold the line sends snoops nobody needs — pure cycles, measurable, and never a wrong answer. A filter that fails to name a cache that does hold the line leaves a stale copy in the machine, which is a coherency violation with no upper bound on its consequences.

Row four is the design that is always correct and sometimes unusable. Naming all eight caches on every lookup is perfectly sound — the filter degenerates into a broadcast — and costs 140 cycles a lookup. That is the safe direction to be wrong in, and knowing which direction is safe is the point of separating the two numbers.

Row two is the one the exact-filter assumption erases. The environment mirrors the filter's own answer instead of tracking who actually holds the line, so the mirror and the filter agree by construction and the missing cache is invisible to both. A checker built from the DUT's own bookkeeping cannot audit that bookkeeping.

8. RTL 4 — A Checker That Samples At Boundaries Sees Two States Of Six

// RTL 4 - the observation window. A checker that samples only at transaction
// boundaries cannot see the states the line passes through in between, and
// reports nothing missing because it never looked.
module observation_window #(parameter int SAMPLE_AT_BOUNDARIES = 0) (
  input  logic clk, rst_n,
  input  logic        observe,
  input  logic [15:0] transaction_cycles, transient_cycles, sample_period,
  input  logic [15:0] states_visited,
  output logic [15:0] samples, seen_states, missed_states, blind_cycles,
  output logic        transient_visible,
  output logic [7:0]  n_observations, n_blind,
  output logic        window_ignored_err
);
  logic [31:0] s_q, c_q;
  // Boundary sampling looks twice: before and after. Periodic sampling looks
  // as often as the period allows.
  assign s_q = (SAMPLE_AT_BOUNDARIES != 0) ? 32'd2
             : ((sample_period == 16'd0) ? 32'd0
                : ({16'd0, transaction_cycles} / {16'd0, sample_period}));
  assign samples = (s_q > 32'd65535) ? 16'hFFFF : s_q[15:0];
  assign seen_states = (samples > states_visited) ? states_visited : samples;
  // A checker that never looks between boundaries reports nothing missing.
  assign missed_states = (SAMPLE_AT_BOUNDARIES != 0) ? 16'd0
                       : (states_visited - seen_states);
  assign blind_cycles = (transaction_cycles > samples)
                        ? (transaction_cycles - samples) : 16'd0;
  // A transient of length L spread over N samples is certainly caught when
  // L * N covers the transaction.
  assign c_q = {16'd0, transient_cycles} * {16'd0, samples};
  assign transient_visible = (c_q >= {16'd0, transaction_cycles})
                             && (samples != 16'd0);
  // States the line passed through that the checker did not see, reported as
  // nothing missing.
  assign window_ignored_err = observe && (states_visited > seen_states)
                              && (missed_states == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_observations <= 8'd0; n_blind <= 8'd0;
    end else if (observe) begin
      n_observations <= n_observations + 8'd1;
      if (!transient_visible) n_blind <= n_blind + 8'd1;
    end
  end
endmodule

Eight observations. A 100-cycle transaction visiting six states unless stated.

Five blind with periodic sampling; seven of eight with boundary sampling.

The defect is not that the boundary checker sees less; it is that it reports nothing missing. Row one is the whole chapter in a line: the periodic sampler sees six states of six, the boundary sampler sees two — and reports zero missed, because "missed" is computed from what it looked for. A coverage number derived from a monitor's own observations cannot measure the monitor.

Rows four and five are the sampling rule, and it is an inequality. A transient of length L is certainly caught when L times the number of samples covers the transaction: ten cycles across ten samples is exactly enough and nine is not. That converts a monitor's sampling period directly into the shortest state it can guarantee to see.

Row six is the exemption. A transaction that only ever visits two states is fully observed by boundary sampling, both models agree, and neither reports an error. The boundary technique is not wrong in general — it is wrong in proportion to how much happens between the boundaries, which is a property of the protocol rather than of the monitor.

9. RTL 5 — A Bias Switch Costs The Flush It Requires

// RTL 5 - bias transitions. Moving a line between host bias and device bias
// requires the other side's copies to be flushed first, and the flush costs.
module bias_transition #(parameter int FLUSH_IS_FREE = 0) (
  input  logic clk, rst_n,
  input  logic        transition,
  input  logic [15:0] dirty_lines, flush_cycles_per_line, switch_overhead,
  input  logic [15:0] budget_cycles,
  output logic [15:0] flush_cost, total_cost, headroom,
  output logic        within_budget, safe_to_switch,
  output logic [7:0]  n_transitions, n_over,
  output logic        unflushed_err
);
  logic [31:0] f_q, t_q;
  assign f_q = (FLUSH_IS_FREE != 0) ? 32'd0
             : ({16'd0, dirty_lines} * {16'd0, flush_cycles_per_line});
  assign flush_cost = (f_q > 32'd65535) ? 16'hFFFF : f_q[15:0];
  assign t_q = {16'd0, flush_cost} + {16'd0, switch_overhead};
  assign total_cost = (t_q > 32'd65535) ? 16'hFFFF : t_q[15:0];
  assign headroom = (budget_cycles > total_cost) ? (budget_cycles - total_cost) : 16'd0;
  assign within_budget = (total_cost <= budget_cycles);
  // A switch is safe only once the other side holds nothing dirty.
  assign safe_to_switch = (FLUSH_IS_FREE != 0) ? 1'b1 : (flush_cost != 16'd0)
                          || (dirty_lines == 16'd0);
  // Dirty lines on the far side, and a switch costed at nothing.
  assign unflushed_err = transition && (dirty_lines != 16'd0)
                         && (flush_cost == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_transitions <= 8'd0; n_over <= 8'd0;
    end else if (transition) begin
      n_transitions <= n_transitions + 8'd1;
      if (!within_budget) n_over <= n_over + 8'd1;
    end
  end
endmodule

Four transitions. A 50-cycle switch overhead against a 200-cycle budget unless stated.

One over budget when the flush is charged; none when it is not.

A bias switch is a flush with a rename on the end. Moving a line from device bias to host bias means every dirty copy on the device side has to be written back first, and sixty-four lines at four cycles each is 256 cycles against a switch overhead of fifty. The overhead is the part that gets estimated; the flush is the part that dominates.

Row four separates a cheap switch from an unsafe one. No measured per-line flush cost produces a total of fifty — the same number the free-flush model reports in row one — but here safe_to_switch goes low, because dirty lines exist and nothing was charged for moving them. Two ways of reaching the same total, one of which is a correctness failure.

10. RTL 6 — Coherency Coverage Counts Pairs, Not States

// RTL 6 - what coherency coverage has to count. A bug lives in a pair of
// states across two caches, so counting states in one cache counts the wrong
// space.
module pair_coverage #(parameter int COUNT_STATES_ONLY = 0) (
  input  logic clk, rst_n,
  input  logic        measure,
  input  logic [15:0] states, caches, pairs_seen,
  output logic [15:0] space, seen, covered_pct, remaining,
  output logic        closed,
  output logic [7:0]  n_measures, n_open,
  output logic        space_understated_err
);
  logic [31:0] sp_q, pc_q;
  // The space a coherency bug lives in is the cross product, not the states.
  assign sp_q = (COUNT_STATES_ONLY != 0) ? {16'd0, states}
              : ({16'd0, states} * {16'd0, states});
  assign space = (sp_q > 32'd65535) ? 16'hFFFF : sp_q[15:0];
  assign seen = (pairs_seen > space) ? space : pairs_seen;
  assign pc_q = (space == 16'd0) ? 32'd0
              : (({16'd0, seen} * 32'd100) / {16'd0, space});
  assign covered_pct = (pc_q > 32'd65535) ? 16'hFFFF : pc_q[15:0];
  assign remaining = space - seen;
  assign closed = (remaining == 16'd0);
  // A cross-cache space reported as a per-cache one.
  assign space_understated_err = measure && (caches > 16'd1)
                                 && (states > 16'd1) && (space == states);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_measures <= 8'd0; n_open <= 8'd0;
    end else if (measure) begin
      n_measures <= n_measures + 8'd1;
      if (!closed) n_open <= n_open + 8'd1;
    end
  end
endmodule

Six measurements. Four states across two caches unless stated.

Two open against the cross product; none against the states alone.

A coherency bug is a relationship, so the coverage space is a product. Four states in one cache is four bins; four states across two caches is sixteen pairs, and the bug in section 5 lives in exactly one of them — modified against modified. A per-cache coverage model closes at 100% with twelve of sixteen pairs seen, and the four it never touched include the one that matters.

Row one is the arithmetic of the false confidence. Twelve of sixteen is 75% and reads as work remaining; four of four is 100% and reads as done. The two reports describe the same regression and differ only in what they were asked to count.

Row four is the exemption that keeps the check honest. With a single cache there is no cross-cache space to understate, so the error stays low even though the per-cache model still reports a smaller number. The defect is counting states where pairs are needed, not counting states at all.

11. RTL 7 — The Race Window Has A Width And A Run Count

// RTL 7 - the race window. A snoop and a request that cross are the coherency
// bug that a directed test never writes, and the window has a width.
module race_window #(parameter int ASSUME_ATOMIC = 0) (
  input  logic clk, rst_n,
  input  logic        evaluate,
  input  logic [15:0] request_latency, snoop_latency, runs, hit_rate_ppm,
  output logic [15:0] window_cycles, expected_hits, runs_needed,
  output logic        window_exercised,
  output logic [7:0]  n_evals, n_unexercised,
  output logic        atomicity_assumed_err
);
  logic [31:0] w_q, h_q, r_q;
  // Two operations overlap for as long as the slower one outlives the faster.
  assign w_q = (ASSUME_ATOMIC != 0) ? 32'd0
             : ((request_latency > snoop_latency)
                ? ({16'd0, request_latency} - {16'd0, snoop_latency})
                : ({16'd0, snoop_latency} - {16'd0, request_latency}));
  assign window_cycles = (w_q > 32'd65535) ? 16'hFFFF : w_q[15:0];
  assign h_q = ({16'd0, runs} * {16'd0, hit_rate_ppm}) / 32'd1000000;
  assign expected_hits = (h_q > 32'd65535) ? 16'hFFFF : h_q[15:0];
  assign r_q = (hit_rate_ppm == 16'd0) ? 32'd0
             : (32'd1000000 / {16'd0, hit_rate_ppm});
  assign runs_needed = (r_q > 32'd65535) ? 16'hFFFF : r_q[15:0];
  assign window_exercised = (expected_hits > 16'd0);
  // Two operations that overlap, modelled as if they could not.
  assign atomicity_assumed_err = evaluate && (request_latency != snoop_latency)
                                 && (window_cycles == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_evals <= 8'd0; n_unexercised <= 8'd0;
    end else if (evaluate) begin
      n_evals <= n_evals + 8'd1;
      if (!window_exercised) n_unexercised <= n_unexercised + 8'd1;
    end
  end
endmodule

Six evaluations. A 500-parts-per-million window unless stated.

Two windows never exercised — the same two in both models, because the run count does not depend on the model.

A coherency race is two operations whose lifetimes overlap. A forty-cycle request against a twelve-cycle snoop leaves twenty-eight cycles in which both are live and the ordering between them is decided by something nobody wrote down. The atomic model reports a window of zero and every race question below it becomes unaskable.

Row five is the number to take to a regression plan. A window hit at 500 ppm needs two thousand runs to be expected once — so a thousand-run nightly is not "lightly covered", it is structurally incapable of hitting it, and the report will say so with a coverage bin at zero and no failures. Expected hits is the honest metric; runs is not.

Row six is the worst of the six and the easiest to ship. The window is still twenty-eight cycles wide — the race is real and reachable — and its rate was never characterised, so there is no run count to aim for. The model reports the width and admits it cannot say how often. A hazard with no measured rate is not a hazard that was ruled out.

12. RTL 8 — The Reference Model Runs Behind The DUT

// RTL 8 - the reference model lags. A checker compares the DUT against a model
// that is some number of transactions behind, and the gap is where bugs hide.
module model_lag #(parameter int ASSUME_IN_STEP = 0) (
  input  logic clk, rst_n,
  input  logic        compare,
  input  logic [15:0] dut_txn, model_txn, txn_rate, detect_budget,
  output logic [15:0] lag_txns, lag_cycles, headroom,
  output logic        detected_in_time, in_step,
  output logic [7:0]  n_compares, n_late,
  output logic        lag_ignored_err
);
  logic [31:0] c_q;
  assign lag_txns = (ASSUME_IN_STEP != 0) ? 16'd0
                  : ((dut_txn > model_txn) ? (dut_txn - model_txn) : 16'd0);
  assign c_q = (txn_rate == 16'd0) ? 32'd0
             : (({16'd0, lag_txns} * 32'd1000) / {16'd0, txn_rate});
  assign lag_cycles = (c_q > 32'd65535) ? 16'hFFFF : c_q[15:0];
  assign headroom = (detect_budget > lag_cycles) ? (detect_budget - lag_cycles) : 16'd0;
  assign detected_in_time = (lag_cycles <= detect_budget);
  assign in_step = (lag_txns == 16'd0);
  // A model behind the DUT, reported as level with it.
  assign lag_ignored_err = compare && (dut_txn > model_txn) && (lag_txns == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_compares <= 8'd0; n_late <= 8'd0;
    end else if (compare) begin
      n_compares <= n_compares + 8'd1;
      if (!detected_in_time) n_late <= n_late + 8'd1;
    end
  end
endmodule

Five comparisons. A hundred transactions per thousand cycles, a 500-cycle detection budget.

One late when the lag is measured; none when it is assumed away.

A reference model that runs behind the DUT detects bugs late, and lateness has a cost. A hundred transactions of lag at a hundred transactions per thousand cycles is a thousand cycles between the corruption happening and the checker noticing — and everything the DUT did in those thousand cycles is now part of the failure signature.

Row four is the failure mode that looks like success. With no measured transaction rate the lag in cycles computes to zero, detected_in_time goes high, and the environment reports timely detection. The lag in transactions is still a hundred — the model states both numbers rather than collapsing them, which is what lets the report be read correctly.

Row five is a floor that matters. A model running ahead of the DUT — a real thing when the model is predictive — gives a negative difference, and a checker computing it without a floor wraps to 65,436 transactions of lag and fails a healthy environment.

13. RTL 9 — A Golden Model Is Paid For On Every Regression

// RTL 9 - what a coherency checker costs. A golden model is built once, run
// on every test, and debugged when it disagrees - and only the first is a
// number anyone estimates.
module checker_cost #(parameter int BUILD_COST_ONLY = 0) (
  input  logic clk, rst_n,
  input  logic        budget,
  input  logic [15:0] build_days, runs, run_minutes, disagreements,
  input  logic [15:0] triage_hours_each, budget_days,
  output logic [15:0] run_days, triage_days, total_days, overrun,
  output logic        affordable,
  output logic [7:0]  n_budgets, n_over,
  output logic        run_cost_ignored_err
);
  logic [31:0] r_q, t_q, s_q;
  // A model that runs on every regression is paid for on every regression.
  assign r_q = (BUILD_COST_ONLY != 0) ? 32'd0
             : (({16'd0, runs} * {16'd0, run_minutes}) / 32'd1440);
  assign run_days = (r_q > 32'd65535) ? 16'hFFFF : r_q[15:0];
  assign t_q = (BUILD_COST_ONLY != 0) ? 32'd0
             : (({16'd0, disagreements} * {16'd0, triage_hours_each}) / 32'd8);
  assign triage_days = (t_q > 32'd65535) ? 16'hFFFF : t_q[15:0];
  assign s_q = {16'd0, build_days} + {16'd0, run_days} + {16'd0, triage_days};
  assign total_days = (s_q > 32'd65535) ? 16'hFFFF : s_q[15:0];
  assign overrun = (total_days > budget_days) ? (total_days - budget_days) : 16'd0;
  assign affordable = (total_days <= budget_days);
  // A model that runs and is triaged, costed only as the day it was written.
  assign run_cost_ignored_err = budget && (runs != 16'd0) && (run_minutes != 16'd0)
                                && (total_days == build_days);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_budgets <= 8'd0; n_over <= 8'd0;
    end else if (budget) begin
      n_budgets <= n_budgets + 8'd1;
      if (!affordable) n_over <= n_over + 8'd1;
    end
  end
endmodule

Five budgets. Twenty days to build, 500 runs of 30 minutes, 40 disagreements at 4 hours each.

One over budget when the runs are charged; none when only the build is.

A coherency model is the most expensive checker in the environment and it is estimated as if it were the cheapest. Twenty days to write is the number that appears in a plan. Ten days of machine time and twenty days of triage are not — and together they are 60% of the real cost, all of it arriving after the plan was approved.

Triage is the item nobody budgets and it is the largest. Forty disagreements at four hours each is twenty days, and most disagreements are the model being wrong, not the DUT — a fact that makes them no cheaper to investigate. The number to negotiate is disagreements per thousand runs, and almost nobody measures it.

Row five is a degenerate case both models agree on, and it is worth driving deliberately. Ten runs of five minutes is fifty minutes, which rounds to zero days, so the full model reports the same total as the build-only one and both raise the same flag. A checker that fired only on the broken build here would be reporting the parameter rather than the cost.

Figure 3 — The plan is complete, correct and thirty days short. Triage is the largest single item and the only one with no natural unit — which is why it is the one that gets left out.

14. RTL 10 — Coherency Sign-Off Assembled

// RTL 10 - coherency verification assembled. Everything that must hold before
// "the coherency tests pass" is a coherency claim rather than a test result.
module coherency_signoff #(parameter int TESTS_PASS = 0) (
  input  logic clk, rst_n,
  input  logic       evaluate,
  input  logic       tests_pass,        // the coherency suite is green
  input  logic       writer_checked,    // single-writer checked across caches
  input  logic       values_checked,    // reads checked against the owning copy
  input  logic       filter_sound,      // the snoop filter names every holder
  input  logic       window_covered,    // the checker can see transient states
  input  logic       pairs_covered,     // the cross-cache state space is closed
  output logic       verified,
  output logic [5:0] fail_mask,
  output logic [7:0] n_eval, n_verified,
  output logic       false_signoff_err
);
  assign fail_mask[0] = ~tests_pass;
  assign fail_mask[1] = ~writer_checked;
  assign fail_mask[2] = ~values_checked;
  assign fail_mask[3] = ~filter_sound;
  assign fail_mask[4] = ~window_covered;
  assign fail_mask[5] = ~pairs_covered;
  // The tests-pass build is what a regression dashboard reports.
  assign verified = (TESTS_PASS != 0) ? tests_pass : (fail_mask == 6'd0);
  assign false_signoff_err = evaluate && verified && (fail_mask != 6'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_eval <= 8'd0; n_verified <= 8'd0;
    end else if (evaluate) begin
      n_eval <= n_eval + 8'd1;
      if (verified) n_verified <= n_verified + 8'd1;
    end
  end
endmodule

Seven configurations.

One verified under the full model; six under the dashboard.

Every one of the five middle rows is a green dashboard on a machine with a coherency bug in it. None of them is a flaky test, an ignored assertion or a disabled check — the suite genuinely passes, because each failure is a question the suite was never shaped to ask.

The asymmetry is what makes the dashboard dangerous. Row seven is the one it catches, and it catches it correctly: a coherency test that fails is real evidence of a real bug. The dashboard is never wrong when it complains, which is exactly why nobody questions it when it is silent. Its failures are all false negatives.

These six are not 25.1's six. That chapter's properties are about whether a rule was checked; these are about whether the check could see the violation. A suite can be complete by 25.1's standard and fail all five of these, because every rule has a checker and every checker is scoped to one cache.

Figure 4 — The scope questions come first because they are the ones that make a check incapable of failing; the coverage questions come last because they only make it unlikely to. Every exit above is a green regression.

15. Quantitative Reasoning

Single writer. Two caches modified at once is the invariant broken; a requester-scoped check reports zero violations of four.

Value reference. A dirty line at version 14 against a memory at 10 fails a memory-referenced check with a staleness of 4, and a check without an absolute value reports 65,530 in the other direction.

Filter recall. Seven false hits is 140 wasted cycles and always sound; one false miss is a lost copy and a coherency bug.

Observation window. A 100-cycle transaction visiting six states is six seen at a 10-cycle period and two at the boundaries — with four missed and zero reported missing.

The sampling rule. A transient of ten cycles across ten samples is exactly caught; nine is not.

Bias switches. Sixty-four dirty lines at four cycles each is 256 cycles against a fifty-cycle switch overhead — 306 against a 200-cycle budget.

Pair coverage. Four states across two caches is sixteen pairs; twelve seen is 75% against a per-cache report of 100%.

Race windows. A forty-cycle request against a twelve-cycle snoop is a 28-cycle window at 500 ppm, needing 2,000 runs to be expected once.

Model lag. A hundred transactions behind at a hundred per thousand cycles is 1,000 cycles of detection latency against a 500-cycle budget.

Checker cost. Twenty days to build attracts ten of machine time and twenty of triage — fifty against a plan of twenty.

The assembled model. Six properties, seven configurations, one verified. The dashboard called six verified.

16. Assertions

Every check is an explicit comparison against an exact value. Icarus Verilog 13.0 has no concurrent assertion support, so each is a procedural comparison against 1'b1, and every one is an equality.

Every computed output is asserted as a value at least once on the build where it is not zero — the rule 24.5 §17 arrived at, and the rule that three of this chapter's four survivors needed. Alongside it: every inclusive threshold at exactly equal, every ceiling on and off its boundary, every floor past it, and both builds asserted on every degenerate case.

Single writer. Six masks cover one writer, two including the requester, two excluding it, all four, and none.

chk(wGw == 3'd2, "two writers");
chk(wGo == 3'd2, "and neither is the requester");

Value reference. The gap is driven in both directions — a cache ahead of memory and a cache behind it — which is what an absolute difference needs.

chk(vBs == 16'd6, "a staleness of six, computed the other way round");

Filter recall. Over-reporting, under-reporting, an exact filter and a broadcast filter are all driven, and the exact case is asserted not to be an ignored miss.

Observation window. The sampling inequality is driven at exactly enough and one cycle short, and a two-state transaction is asserted as not an error in either build.

chk(oGv == 1'b1, "and ten cycles across ten samples is exactly enough");
chk(oGv == 1'b0, "nine cycles across ten samples is not");

Bias switches. A cost exactly at the budget is constructed from 32 lines and a 72-cycle overhead, and headroom is asserted as a value in two cases — one where it is zero and one where it is 150.

Pair coverage. A count larger than the space is asserted to clamp, and both the one-cache and one-state exemptions are asserted quiet in both builds.

Race windows. Exactly the number of runs the window needs is driven, and the uncharacterised-rate case asserts that the window is still 28 cycles wide — the hazard exists and was never hit.

Model lag. A lag exactly at the budget is constructed from 50 transactions, and a model ahead of the DUT is asserted to floor rather than wrap.

Checker cost. A budget exactly equal to the cost is driven, and the rounds-to-zero regression is asserted to raise the same flag in both builds.

The assembled model. Every fail mask is asserted as an exact six-bit value, and each of the six bits is driven false alone so no two can be swapped without a test noticing.

Totals: 301 checks across two testbenches, 160 on the front five models and 141 on the back five, all passing on the unmutated sources.

17. Mutation Testing

Eighty-five mutations were injected one at a time. 85 injected, 85 killed, after four survivors.

Three of the four survivors were the same defect, and it is the one 24.5 named. headroom in section 9, safe_to_switch in section 9, and headroom in section 12 were each computed, driven, and never asserted as a value — observed only through a neighbouring flag. Inverting the comparison inside each one changed nothing any test looked at. Four lines fixed all three, none of them new stimulus.

That rule was written down one chapter ago and it did not prevent the defect. It caught it — at mutation time, which is where it is cheap — but the drafting habit has not formed. The corrective is mechanical rather than attentional: after writing a model, list its outputs and check each one appears in an equality somewhere. Section 18 states it as a step rather than a principle.

The fourth survivor was a guard reachable only at a degenerate input. transient_visible ends in && (samples != 0), which is dominated by the coverage inequality for every non-zero transaction — transient × 0 cannot reach a positive length. At a transaction of zero cycles it is the only thing standing between the model and claiming visibility of nothing, so the guard is live and the case was simply undriven. Adding it killed the mutation and produced §8 row eight, where the boundary sampler claims its two looks covered a transaction that never ran.

18. Verification Strategy

What a testbench for a scope-of-observation model must cover.

List every output and confirm it appears in an equality. Three of four survivors here, and the same class in three of five chapters of the previous batch. Do this as a step after writing each model, not as a principle held while writing it — the principle has now failed twice.

Drive both directions of every difference. §6's staleness is an absolute value, and a testbench that only ever puts the cache ahead of memory never executes half of it. A difference has two signs and a subtraction has one.

Drive the degenerate input a guard exists for. §8's zero-sample guard is unreachable for every real transaction and load-bearing for a transaction of zero cycles. A guard that looks dominated may be guarding the boundary of the domain rather than the arithmetic.

The cases where the narrow scope is right. A single exclusive writer. A clean line. An exact filter. A two-state transaction. A single cache. A single-state protocol. Equal latencies. A model in step. Eight exemptions across nine models, each one a real configuration in which the broken build is correct — and each one the reason the narrow scope survives review.

Separate the claim from the count. §8's seen_states and missed_states are different outputs because they are different facts: what a monitor saw and what it says it missed, and the whole defect lives in the second one being derived from the first.

Counters as a second signature. Ten models, ten pairs of totals, differing in nine. The tenth is §11's n_unexercised, which is deliberately equal in both builds — the run count is a property of the regression, not of the model, so a difference there would be manufactured.

What a real coherency environment needs that these models do not have. A directory with sharers and owners rather than §5's occupancy mask, a non-uniform sampling model for §8, and a measured disagreement rate for §13. All three are abbreviations that preserve the conclusion, and section 26 exercises 1, 4 and 9 are where they come back.

19. Synthesis and Implementation Reality

§5's cross-cache check is a monitor with no home. It needs visibility into every cache's state at the same instant, which no single interface carries — so it is built either from a directory mirror or from a union of per-cache monitors with a common time base. The common time base is the hard part, and it is why the requester-scoped version gets written instead.

§6's owning-copy reference is a write-back model, not a memory model. It has to track which cache holds each line dirty, which means it is a coherency model in its own right — the checker for the protocol is as complex as the protocol, which is §13's cost and the reason it is underestimated.

§7's filter mirror must be independent of the filter. A mirror built by observing the filter's own allocations agrees with it by construction and can only catch implementation slips, not policy errors. An independent mirror is built from the transactions, and it is roughly the same size as the filter.

§8's periodic sampling costs simulation time. Sampling every cycle in a large environment is a substantial slowdown, which is exactly the pressure that produces boundary sampling. The right compromise is stated as a number: sample at the period the shortest state of interest requires, and record what that period was.

§11's race windows are reached by randomisation, not by direction. A directed test constructs the overlap once; a constrained-random regression reaches it at a rate. Both are needed — the directed test proves it is reachable, and the rate says whether the regression will keep reaching it.

§12's model lag is a design choice in the environment. A model that runs in lockstep is slow and detects immediately; one that runs behind is fast and detects late. The budget is a detection-latency requirement, and almost no environment states one.

20. Silicon Observability

"Filter entries evicted while a cache still holds the line" is the entry worth building first. It is the only counter here that fires before a coherency bug rather than after one — an unsound filter is a latent fault, and the eviction that creates it is observable at the moment it happens. Every other counter on this list describes a machine that already has the problem.

21. Debug Lab

Symptom. A CXL type-2 accelerator has been in regression for four months. The coherency suite is green on every run. Then, on a customer workload: a tensor comes back with sixteen bytes wrong, once every few hours, always at a page boundary, and never reproducible in simulation.

Step 1 — what does green mean here? The coherency environment has a checker for every CXL.cache rule and a coverage model at 100%. Section 14's question rather than section 14's answer: which of the six properties does that establish? The audit takes an afternoon and finds five of them unestablished.

Step 2 — the scope of the invariant checker. The single-writer check is written inside the cache agent monitor and evaluates this_cache.state == M against the snoop response it just sent. Section 5. It cannot see a second cache, and the environment has four. Zero violations of however many occurred.

Step 3 — the reference model's reference. Reads are checked against a memory image the environment maintains. Section 6. For clean lines this is correct, and the regression is mostly clean lines. For a line held dirty in another cache it compares against a stale value — and it has been passing because the two agree far more often than not.

Step 4 — the coverage number. 100% is per-cache: four states, four bins, all hit. Section 10. Across two caches the space is sixteen pairs, and the database has eleven. The five never seen include modified against modified, which is the pair the symptom is made of.

Step 5 — why simulation never hit it. The overlap between an incoming snoop and an outstanding write is 28 cycles at a rate the environment has never characterised. Section 11. At 500 ppm the nightly's thousand runs expect zero hits; the customer's machine runs the equivalent of millions.

Step 6 — the page boundary. Not a coherency property at all — it is where the accelerator's bias switches, and the switch is costed at its fifty-cycle overhead with the flush of sixty-four dirty lines uncounted. Section 9. The switch completes before the flush does, which is how two caches come to hold the line modified in the first place.

The finding. One hardware bug — a bias switch that does not wait for its flush — and five independent reasons the environment could not have found it. The invariant checker was scoped to one cache, the value checker referenced memory, the coverage model counted states, the regression was too short to hit the window, and the flush cost was never modelled.

The fix. In the RTL, gate the bias switch on flush completion. In the environment: move the single-writer check to a directory-scoped monitor, re-reference the value checker to the owning copy, re-key the coverage model on cache pairs, and characterise the overlap rate so the regression length can be argued rather than assumed. The first change fixes the machine; the other four are why it took four months.

What made this hard. The suite was not neglected. Every rule had a checker, every checker passed, and the coverage report said 100% — and each of those three statements was true at a scope that could not contain the bug.

22. Design Review

1. What scope does the single-writer check evaluate over, and where does it get simultaneous state from? A monitor inside one agent cannot check a property of the set. Sections 5 and 19.

2. What does the value checker compare against when the line is dirty in another cache? Memory is behind by definition. Section 6.

3. Is the snoop-filter mirror built from the filter or from the transactions? A mirror built from the filter agrees with it by construction. Sections 7 and 19.

4. What is the monitor's sampling period, and what is the shortest state of interest? Ten cycles across ten samples is exactly enough; nine is not. Section 8.

5. What does the environment report as "missed", and is it derived from what the monitor saw? A coverage number derived from a monitor cannot measure that monitor. Section 8.

6. Is the coverage model keyed on states or on pairs? Sixteen pairs against four bins. Section 10.

7. What are the race windows, how wide, and at what measured rate? A 28-cycle window at 500 ppm needs 2,000 runs to be expected once. Section 11.

8. How far behind the DUT does the reference model run, and what is the detection-latency budget? Almost no environment states one. Section 12.

9. What is the model's disagreement rate per thousand runs? It is the largest cost item and the least measured. Section 13.

10. Which of the six properties does a green coherency regression establish? Section 14 exists because the answer is the last one only.

23. How This Appears In Real Engineering

A verification engineer writes checkers where the signals are, and the signals are inside an agent. Every narrow scope in this chapter is what you get by building the checker at the natural place — which is why the fix is architectural rather than a matter of care.

A verification lead owns the question in section 14 and usually answers it with a coverage percentage. The percentage is a fact about a database whose keys somebody chose, and section 10 is what happens when the keys are per-cache.

An architect owns the invariants and rarely sees how they are checked. The gap between "at most one cache holds this modified" and the SystemVerilog that allegedly checks it is where this chapter lives, and closing it is a review rather than a tool.

A silicon debug engineer meets all of this after tape-out, with the counters of section 20 or without them. The eviction counter in particular cannot be added later, and it is the only one that fires before the corruption.

24. Common Misconceptions

"Every rule has a checker, so the protocol is checked." 25.1's standard, met in full, and all five of this chapter's scope failures survive it. A checker for the right rule at the wrong scope is a checker that cannot fail.

"Coverage is at 100%." Of a space somebody chose. Four states across two caches is sixteen pairs; a per-cache model closes at 100% with a quarter of the space untouched (section 10), and the untouched quarter is where the bug is.

"The reference model compares against memory, which is the truth." Memory is the truth for clean lines and stale by construction for dirty ones (section 6). The reference has to follow ownership, which makes it a coherency model rather than a memory image.

"The monitor didn't report anything missing." It reported what it looked for. Boundary sampling sees two states of six and reports zero missed (section 8) — the claim is derived from the observation, so it cannot contradict it.

"An imprecise snoop filter is a performance issue." Imprecision is. Incompleteness is a coherency bug (section 7), and the two are different numbers that a single "filter accuracy" metric hides.

"We run a million random cycles a night." Against a 28-cycle window at 500 ppm, the metric that matters is expected hits, not cycles (section 11) — and a thousand runs expect zero.

25. Interview Reasoning

"How would you check that at most one cache holds a line modified?" The answer has to name a scope before it names a mechanism. A check inside a cache agent cannot evaluate a property of the set, whatever it is written in — the candidate who reaches for a directory-scoped monitor or a union of monitors on a common time base has understood the question, and the one who reaches for an SVA property has answered §25.3's.

"Your coherency coverage is at 100% and you found a coherency bug in silicon. What went wrong?" Section 10. The space was keyed on states in one cache rather than pairs across two, so 100% describes a quarter of the real space. A good follow-up to ask back: what would the number have been on the right keys? — 75%, which reads as work remaining.

"The reference model and the DUT disagree. Which is wrong?" Usually the model — and that is the trap. Most disagreements being model bugs is exactly why they are expensive (section 13), not why they can be dismissed. Twenty of the model's fifty days are this.

"How long should the regression be?" Not a length — a rate. A window at 500 ppm needs 2,000 runs to be expected once (section 11), so the honest answer is a question: what is the measured rate of the narrowest window? A candidate who names a cycle count has not been asked for one.

"What does a green coherency dashboard tell you?" That no coherency test failed. Section 14's six properties are the distinction between an observation and a claim, and it is the same distinction 25.1 is built on, moved from rules to scopes.

26. Exercises

1. Replace the occupancy mask with a directory. §5 uses four bits. Model sharers, an owner and a pending state, then state the single-writer invariant over it and find the transient during which it is legally violated.

2. Build the value checker properly. Write the ownership tracking §6 needs, and count how much of a coherency model it turns out to be. Compare against §13's build estimate.

3. Price filter soundness. At 20 cycles a snoop, compute the wasted cycles for filters at 1, 2, 4 and 8 false hits per lookup, and the expected cost of one false miss. State why the units cannot be compared.

4. Make the sampling model non-uniform. §8 assumes samples are evenly spread. Redo the visibility inequality for samples clustered at transaction start, and find the transient length that is caught under one model and missed under the other.

5. Turn a sampling period into a requirement. Given a shortest state of interest of 8 cycles in a 100-cycle transaction, compute the maximum sampling period and the simulation slowdown it implies at 1, 10 and 100 monitored lines.

6. Close the pair space. For 4 states and 2 caches, list the sixteen pairs and mark which are legal, which are illegal, and which are transiently legal. How many bins should the coverage model actually have?

7. Size a regression from a rate. For windows at 500, 50 and 5 ppm, compute the runs needed for an expected hit and for 95% confidence of at least one. Which of the three is affordable nightly?

8. Budget detection latency. §12 uses 500 cycles. Derive a budget from a debug argument — how much DUT activity after a corruption is still tractable to read — and state the model lag it permits.

9. Measure the disagreement rate. §13 assumes 40 disagreements. Propose how to measure it in the first month and what to do when it comes back at 400.

10. Add the seventh property. Propose one none of §14's six implies, name its section, and construct the configuration where the six hold and it fails. A property that cannot fail alone is not a seventh property.

27. Summary

The single-writer invariant is a property of the set, not of a cache. A requester-scoped check reports zero violations of four, and it is not wrong about anything it looked at.

A read is checked against the owning copy or against nothing. A dirty line at version 14 against a memory at 10 fails a correct read — and passes for months, because clean lines and written-back lines agree.

A snoop filter fails in two currencies. Seven false hits is 140 wasted cycles; one false miss is a lost copy, and a single accuracy metric hides which one happened.

A checker that samples at boundaries sees two states of six and reports nothing missing. The claim is derived from the observation, so it cannot contradict it — which is the sharpest form of this chapter's problem.

Ten cycles across ten samples is exactly enough and nine is not. That converts a sampling period into the shortest state a monitor can guarantee to see, which is a requirement rather than a setting.

A bias switch costs its flush. Sixty-four dirty lines at four cycles each is 256 cycles against a fifty-cycle overhead — and a switch that completes before its flush is how two caches come to hold a line modified.

Coherency coverage counts pairs. Four states across two caches is sixteen, and twelve seen is 75% against a per-cache report of 100% — with modified-against-modified among the four never touched.

A race window has a width and a rate. Twenty-eight cycles at 500 ppm needs 2,000 runs to be expected once, so a thousand-run nightly is not lightly covering it; it is structurally unable to reach it.

A reference model runs behind, and lateness is unbudgeted. A hundred transactions of lag is a thousand cycles of DUT activity between the corruption and the detection.

And the model costs fifty days against a plan of twenty — ten of machine time, twenty of triage, most of it after the plan was approved.

Three of four mutation survivors were outputs never asserted as a value — the rule 24.5 wrote down one chapter ago. It caught them, cheaply, at mutation time; it did not prevent them. §18 now states it as a step to perform rather than a principle to hold.

"The coherency tests pass" is one property of six. The dashboard called six of seven configurations verified when one was — and §21 is an accelerator four months green, with one hardware bug and five independent reasons the environment could not have found it.

25.3 — CXL Assertions takes the checks this chapter kept describing and writes them. Every scope argument here becomes a question about what an assertion can sample and when: a property is only as wide as the signals in scope at the clock it is written on.