Coherency Verification

Module 17 · Chapter 17.2 · CHI Verification

Project thread — 17.1 checked per-flit legality. 17.2 checks cross-cache coherence invariants; 17.3 builds the scoreboard.

1. Learning Outcomes

By the end of this chapter you should be able to:

• Explain that coherency is a system property — invisible in any single flit or cache.
• State the SWMR invariant — one writer with no other holders, or many readers, never both.
• Describe a coherency monitor that aggregates every cache's per-line state.
• Explain why local transition checks cannot catch a cross-cache violation.
• Diagnose the escaped two-writer violation from a locally-only checker.
• Implement a representative SWMR checker in SystemVerilog, Verilog-2001, and VHDL.

2. Why Should I Learn This?

A design can emit perfectly legal flits and still be incoherent. Protocol verification (Chapter 17.1) proves each flit is well-formed; it cannot prove the caches agree about a line. Coherency is the property that the whole point of CHI exists to provide, and verifying it requires a fundamentally different kind of check — a global one that looks at all the caches together, not one flit at a time.

The invariant that captures coherence is SWMR — single-writer-multiple-reader. For any line: either one cache holds it writable/dirty and no one else holds it, or several caches hold it read-only — but a writer never coexists with another holder. A two-writer state (two caches both able to modify a line) means two cores can diverge — the exact failure coherence prevents. The catch is that no single flit or cache reveals the violation: each cache's local transitions can look legal while the combination is illegal. A checker that only verifies local legality gives a false pass on a real coherence bug. This chapter is the global invariant and why it must be checked across the caches.

3. Key Terms

4. Previous Chapter Connection

This chapter verifies the coherence you built in Modules 9–11. SWMR is the formal statement of the sharing rules from Chapter 10 (states UC/UD/SC/SD) — a writable copy excludes all others; read-only copies may coexist. Where those chapters implemented coherence, this one checks it, from the outside, across the whole system.

It also targets the exact bug class of Chapter 16.1. There, a directory race (concurrent same-line requests) could leave the directory wrong and let two caches end up writable — a coherence violation. This chapter is the verification that catches it — if the checker looks globally. The connection is the lesson: an RTL bug that corrupts a cross-cache invariant is invisible to a checker that only examines one cache or one transaction. Chapter 17.1 was per-flit; this is per-system — and the two together are still not enough without the scoreboard (17.3) and the coverage (17.6) that ensure the checks actually run.

5. Core Concept — check SWMR across all caches

Coherency verification aggregates every cache's per-line state and asserts the SWMR invariant — a violation that no single flit or cache can reveal.

• Coherency is global. Whether a line is coherent depends on all caches holding it — no single flit or cache shows the whole picture.
• SWMR is the invariant. For each line: one writer (writable/dirty) with no other holders, or any number of readers (read-only), but never a writer alongside another holder.
• Aggregate the caches. A coherency monitor tracks, per line, which caches hold it and in what state — a global per-line view assembled from all caches.
• Assert the invariant. For each line, count writers and readers; a violation is writers > 1, or writers ≥ 1 while readers ≥ 1. Local legality does not imply the global invariant holds.

The synthesis:

Coherency verification checks global, cross-cache invariants — chiefly SWMR: per line, one writer alone or many readers, never a writer with another holder. It requires aggregating every cache's per-line state and asserting the invariant across them. A violation is invisible in any single flit or cache — so a checker that verifies only local transitions gives a false pass on a real two-writer coherence bug. The check must be system-wide.

6. Engineering Mental Model — one editable master among copies

Think of a document that a team shares, with a rule about who may edit versus read.

• The rule (SWMR): either one person has the editable master and no one else has a copy, or several people have read-only copies — but never an editor and other holders at once. Two editors could make conflicting changes.
• To check the rule, you must look at everyone's desk at once — who has the editable master, who has read-only copies. You cannot tell from one person's desk whether the rule holds.
• A checker that only asks each person "is your own copy in a legal state?" learns that each copy is individually fine — an editable master is fine, a read-only copy is fine — but never asks "does anyone else also have it?"
• So if two people each hold an editable master (each individually legal), the local checker sees two legal desks and reports all clear — while the document is in a two-editor state that will corrupt it. The violation is in the combination, which no single-desk check sees.

The all-desks view is the global aggregate; SWMR is the rule; the single-desk check is the local-only checker that misses the two-editor violation.

7. Engineering Diagram — the coherency monitor

Every cache feeds the global aggregate; the SWMR check runs on the combined per-line counts. The violation lives in the aggregate, not in any one cache's feed. The DebugLab omits the aggregate — checking each cache's feed in isolation.

8. The SWMR States

The legal and illegal global per-line configurations.

The rule to carry: legality is a property of the counts across all caches, and only two shapes are legal — one writer alone, or readers only. A single cache in any state is locally legal (a writable copy is fine, a read-only copy is fine) — so local checks always pass. The violation appears only when you count across caches: more than one writer, or a writer with any reader. This is why coherency verification must aggregate — the illegal states are combinations of individually-legal cache states.

9. Why Local Checks Miss the Violation

The false pass, made explicit.

• Each cache's transitions are individually legal. A cache moving I → UD (gaining a writable copy) is a legal transition for that cache. So is another cache doing the same.
• A local checker verifies each in isolation. It watches each cache and confirms its state changes follow the protocol's per-cache rules — and they do.
• No component compares the caches. With only local checks, nothing in the environment ever asks "do two caches both hold this line writable?" — the global relationship is never examined.
• So a two-writer state passes. If a directory bug (Chapter 16.1) grants two caches a writable copy, each transition was locally legal, the local checker passes both, and the two-writer coherence violation escapes — a false pass on the most serious bug class there is.

The point to carry:

Coherency verification is the archetype of a compositional correctness property — one that holds of a collection even though it cannot be reduced to a property of each member. SWMR is not "each cache is in a legal state" (that is always true); it is "the caches are in a mutually legal configuration," which is a statement about the relationships between them. A verification environment built only from per-agent checkers is structurally incapable of catching a compositional violation, because no per-agent checker sees more than its own agent — the violation lives in the space between the agents, which only a global observer occupies. This is the single most important architectural decision in a CHI verification environment: there must be a component that sees the whole system and checks the invariants that span it, because the bugs that matter most — the actual coherence violations — are exactly the ones no local checker can see. It also foreshadows the UVM architecture of Chapter 17.7: a bank of per-agent monitors is necessary but not sufficient; a central system-level checker subscribed to all of them is what makes coherence verifiable at all. Local checks find malformed flits; only a global check finds incoherence.

10. Verifying a Line — local-only vs global

A directory bug grants caches c0 and c1 a writable copy of line X.

1. c0: I → UD. Cache c0 gains a writable/dirty copy of X. A locally legal transition. A local checker passes it.
2. c1: I → UD. Cache c1 also gains a writable copy of X (the directory race). Locally legal for c1 in isolation. A local checker passes it too.
3. Local-only checker — false pass. Both transitions were individually legal; nothing compared c0 and c1. The environment reports all clear — while X has two writers. Violation escaped.
4. Global checker — aggregate. The coherency monitor updates the global per-line view: X now has writers = 2 (c0 and c1 both UD).
5. Global checker — SWMR fails. The invariant check sees writers > 1 and flags a violation. The two-writer coherence bug is caught.

The global checker caught what both local checks missed — because it looked at the combination. The DebugLab is steps 1–3.

11. Checker / Monitor View — the SWMR invariant checker

Aggregate per-line writer and reader counts across caches; flag more than one writer or a writer with readers. Representative.

// Representative SWMR coherency checker (educational).
// Aggregate the per-line state of ALL caches. For a line, a WRITER is a cache in a
// writable/dirty state; a READER is a cache in a read-only state. SWMR is violated if
// writers>1, OR a writer coexists with any reader. A per-cache-only checker cannot see
// this -- the violation is in the COMBINATION across caches.
module chi_swmr_check #(parameter NCACHE = 8) (
  input  logic [NCACHE-1:0] holds_writable,  // per cache: holds this line writable/dirty
  input  logic [NCACHE-1:0] holds_readonly,  // per cache: holds this line read-only
  output logic [$clog2(NCACHE+1)-1:0] writers,
  output logic [$clog2(NCACHE+1)-1:0] readers,
  output logic              swmr_violation
);
  always_comb begin
    writers = '0; readers = '0;
    for (int i = 0; i < NCACHE; i++) begin
      writers += holds_writable[i];   // count writers across all caches
      readers += holds_readonly[i];   // count readers across all caches
    end
  end
  // Violation: more than one writer, OR a writer coexisting with any reader.
  assign swmr_violation = (writers > 1) || ((writers >= 1) && (readers >= 1));
endmodule

The same behavior in Verilog-2001:

// Representative SWMR coherency checker (Verilog-2001).
module chi_swmr_check #(parameter NCACHE = 8, parameter CW = 4) (
  input  [NCACHE-1:0] holds_writable, holds_readonly,
  output reg [CW-1:0] writers, readers,
  output              swmr_violation
);
  integer i;
  always @* begin
    writers = {CW{1'b0}}; readers = {CW{1'b0}};
    for (i = 0; i < NCACHE; i = i + 1) begin
      writers = writers + holds_writable[i];
      readers = readers + holds_readonly[i];
    end
  end
  assign swmr_violation = (writers > 1) | ((writers >= 1) & (readers >= 1));
endmodule

And in VHDL:

-- Representative SWMR coherency checker (VHDL).
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
 
entity chi_swmr_check is
  generic ( NCACHE : integer := 8 );
  port (
    holds_writable : in  std_logic_vector(NCACHE-1 downto 0);
    holds_readonly : in  std_logic_vector(NCACHE-1 downto 0);
    writers        : out integer range 0 to NCACHE;
    readers        : out integer range 0 to NCACHE;
    swmr_violation : out std_logic
  );
end entity;
 
architecture rtl of chi_swmr_check is
begin
  process (holds_writable, holds_readonly)
    variable w, r : integer range 0 to NCACHE;
  begin
    w := 0; r := 0;
    for i in 0 to NCACHE-1 loop
      if holds_writable(i) = '1' then w := w + 1; end if;
      if holds_readonly(i) = '1' then r := r + 1; end if;
    end loop;
    writers        <= w;
    readers        <= r;
    if (w > 1) or (w >= 1 and r >= 1) then
      swmr_violation <= '1';
    else
      swmr_violation <= '0';
    end if;
  end process;
end architecture;

All three count writers and readers across all caches and flag swmr_violation on more than one writer or a writer-with-readers — a check possible only with the global aggregate. The DebugLab has no such aggregate; it checks each cache alone.

12. Assertion View — SWMR holds for every line

The properties formalize the invariant: at most one writer, and no writer-with-readers.

// Bind to chi_swmr_check (per line, across the aggregate).
// 1. At most one cache holds any line in a writable/dirty state.
property p_single_writer;
  @(posedge clk) disable iff (!rst_n)
    (writers <= 1);
endproperty
 
// 2. A writer never coexists with any reader (writer XOR readers).
property p_writer_excludes_readers;
  @(posedge clk) disable iff (!rst_n)
    (writers >= 1) |-> (readers == 0);
endproperty
 
// 3. The violation flag fires exactly when SWMR is broken.
property p_violation_iff_broken;
  @(posedge clk) disable iff (!rst_n)
    swmr_violation == ((writers > 1) || ((writers >= 1) && (readers >= 1)));
endproperty

The system point, beyond the checks:

The SWMR checker is a reference invariant that is far simpler than the design that must uphold it — a handful of counts and a comparison, versus the entire distributed machinery of directories, snoops, and trackers from Module 16. That asymmetry is the power of invariant-based verification: you do not re-implement the protocol to check it; you state the property the protocol must maintain, in the simplest terms, and check that property continuously against the running design. A bug anywhere in the vast implementation — a directory race, a lost snoop, a mis-tagged response — that results in two writers will trip this one small check, regardless of how it happened. This is why global invariants are the highest-value checks in a coherence environment: one simple property catches an entire class of complex bugs by their effect rather than their cause. The complementary weakness is that an invariant tells you a violation occurred but not where it came from — so the invariant checker (17.2) pairs with the scoreboard (17.3) and per-flit monitors (17.1) that localize the cause. The invariant is the safety net; the other checks are the diagnosis.

• What it proves: at most one writer per line; a writer excludes readers.
• What it does not prove: the data value is correct — that is the scoreboard (Chapter 17.3).
• Bug signature: an environment with per-cache checks but no global aggregate/SWMR check.

13. Testbench — a two-writer state must be flagged

Sets two caches writable on the same line and checks SWMR fires.

module tb_chi_swmr_check;
  localparam NCACHE = 8, CW = 4;
  logic [NCACHE-1:0] holds_writable, holds_readonly;
  logic [CW-1:0] writers, readers;
  logic swmr_violation;
  int errors = 0;
 
  chi_swmr_check #(.NCACHE(NCACHE)) dut (.*);
 
  initial begin
    // Legal: one writer, no readers.
    holds_writable = 8'b0000_0001; holds_readonly = 8'b0000_0000; #1;
    if (swmr_violation) begin errors++; $display("FAIL single writer flagged"); end
    else $display("PASS single writer legal (w=%0d r=%0d)", writers, readers);
 
    // Legal: several readers, no writer.
    holds_writable = 8'b0000_0000; holds_readonly = 8'b0000_1110; #1;
    if (swmr_violation) begin errors++; $display("FAIL multiple readers flagged"); end
    else $display("PASS multiple readers legal (w=%0d r=%0d)", writers, readers);
 
    // VIOLATION: two caches hold the line writable (the directory-race bug).
    holds_writable = 8'b0000_0011; holds_readonly = 8'b0000_0000; #1;
    if (!swmr_violation) begin errors++; $display("FAIL two writers NOT flagged (escaped!)"); end
    else $display("PASS two writers flagged: w=%0d (SWMR violation)", writers);
 
    // VIOLATION: a writer coexisting with a reader.
    holds_writable = 8'b0000_0001; holds_readonly = 8'b0000_0010; #1;
    if (!swmr_violation) begin errors++; $display("FAIL writer+reader NOT flagged"); end
    else $display("PASS writer+reader flagged (w=%0d r=%0d)", writers, readers);
 
    if (errors == 0) $display("ALL TESTS PASSED");
    else             $display("%0d FAILURE(S)", errors);
    $finish;
  end
endmodule

Expected output:

PASS single writer legal (w=1 r=0)
PASS multiple readers legal (w=0 r=3)
PASS two writers flagged: w=2 (SWMR violation)
PASS writer+reader flagged (w=1 r=1)
ALL TESTS PASSED

14. DebugLab — a coherency checker with no global aggregate

directory race: grants line X writable to BOTH cache 0 and cache 1
cache 0: I -> UD  (locally legal transition)   -> local checker PASSES
cache 1: I -> UD  (locally legal transition)   -> local checker PASSES
environment: per-cache checks only, NO global aggregate, NO SWMR check
  -> nothing ever asks "do c0 and c1 both hold X writable?"
  -> two-writer state (writers = 2) NEVER examined -> false PASS
correct: global aggregate -> writers(X) = 2 -> SWMR violation flagged

15. Common Mistakes

• No global aggregate. Assumption: per-cache checks suffice. Bug: two-writer escapes (the DebugLab). Prevention: aggregate all caches.
• Checking only local transitions. Assumption: legal transitions imply coherence. Bug: illegal combinations pass. Prevention: assert the cross-cache invariant.
• Omitting the writer-with-readers case. Assumption: only two-writers is bad. Bug: writer+reader passes. Prevention: writer XOR readers.
• Trusting a green protocol run. Assumption: legal flits mean coherent. Bug: incoherence unseen. Prevention: coherency is a separate layer.
• No data-value check. Assumption: SWMR is enough. Bug: wrong value with legal states. Prevention: add the scoreboard (Chapter 17.3).
• Per-agent-only environment. Assumption: agents cover it. Bug: cross-agent holes. Prevention: a central checker (Chapter 17.7).

16. Engineering Checklist

• Maintain a global per-line aggregate of every cache's state.
• Assert SWMR — at most one writer, and a writer excludes readers.
• Flag writers > 1 and writer coexisting with any reader.
• Check the invariant continuously, not just at transaction boundaries.
• Pair the invariant with per-flit (17.1) and scoreboard (17.3) checks for diagnosis.
• Ensure a system-level component sees the whole design.

17. Key Takeaways

• Coherency is a system property — invisible in any single flit or cache.
• SWMR: one writer alone, or many readers, never a writer with another holder.
• A coherency monitor aggregates every cache's per-line state.
• Local transition checks cannot catch a cross-cache violation.
• A locally-only checker gives a false pass on a two-writer bug.
• Global invariants catch bug classes by effect; the model here is representative.

18. Quick Revision

Coherency verification. Protocol verification (Chapter 17.1) proves each flit is well-formed but says nothing about whether the caches stay coherent — a system property invisible in any single flit or cache. The central invariant is SWMR (single-writer-multiple-reader): for any line, either one cache holds it writable/dirty with no other holders, or several caches hold it read-only, but a writer never coexists with another holder. Checking it requires a coherency monitor that aggregates every cache's per-line state into a global view and, per line, counts writers and readers, flagging writers > 1 or a writer with any reader. The failure to avoid: a checker that verifies each cache's transitions as locally legal but never the cross-cache invariant. Two caches each going I → UD (the directory-race bug of Chapter 16.1) are individually legal, so local checks pass both — and with no global aggregate, nothing ever compares them, so the two-writer violation escapes as a false pass. SWMR is compositional — a property of the caches' mutual configuration, not each cache alone — so a per-agent-only environment is structurally blind to it; only a global observer sees the space between the agents. A global invariant is the highest-value check: one simple property catches a whole class of complex bugs by their effect. Representative model; 17.3 covers the scoreboard that checks data values.

Coming Next

Chapter 17.3 — CHI Scoreboards. The coherency invariant proves the caches' states are consistent; the scoreboard proves the data values are correct. Chapter 17.3 covers CHI scoreboards — the distributed scoreboard that matches each response to its expected transaction and compares returned data against a reference, and why matching by address instead of the transaction ID mis-correlates responses and hides real data bugs.