AMBA CHI · Module 10 · Cache State Management
Common State Bugs
This module built the CHI cache states and tables; this chapter studies how they break. Real coherence state machines fail in a few recurring ways: illegal transitions (a move the table never allowed, like silently upgrading a shared line to writable), lost dirty data (a dirty line released with no writeback and no forward), stale sharers (a write that misses a forgotten holder), ownership drift (the directory and a cache disagreeing on the owner), and incomplete tables (a combination nobody defined). The insight: every one violates a state-machine invariant, and each is caught by an assertion bound to the design. Directed tests pass and the bug ships; the assertion fires when the corner case occurs. Representative model, not the specification.
Advanced16 min readAMBA CHIState BugsAssertionsInvariantsVerification
Module 10 · Chapter 10.7 · Cache State Management
Project thread — 10.1–10.6 built the state machine. This chapter closes the module by cataloguing how it breaks, and how assertions catch it. Module 11 turns to the interconnect.
1. Learning Outcomes
By the end of this chapter you should be able to:
- Name the recurring families of CHI cache-state bugs.
- Match each bug family to the invariant it violates.
- Recognize illegal transitions, lost dirty data, stale sharers, ownership drift, incomplete tables.
- Explain why assertions (invariant checks) catch what directed tests miss.
- Diagnose a corner-case coherence violation that slipped past directed testing.
- Implement a representative invariant monitor in SystemVerilog, Verilog-2001, and VHDL.
2. Why Should I Learn This?
A coherence state machine is small — five states, a handful of events — but its bugs are among the most feared in a chip, because they are silent, rare, and catastrophic: a stale read or a lost write, deep in a corner case, that no functional test happened to hit. This chapter is the module's payoff: it gathers the mistakes you have seen chapter by chapter into a single catalogue — the things that actually go wrong in real implementations.
The deeper lesson is how to catch them. Every state bug is a violated invariant — a rule the state machine must always obey, broken in some overlooked case. Directed tests check the cases you thought of; assertions check the invariant on every case, thought of or not. So the way to ship a correct coherence machine is not more directed tests but the right invariant checks, bound to fire the instant a rule breaks. Learning the bug families and their invariants is learning what to assert.
3. Key Terms
4. Previous Chapter Connection
Every chapter of this module ended with a bug: 10.1 conflated the two axes (evicting SD as clean); 10.2 left a table entry missing; 10.3 let the directory drift from the owner; 10.4 under-counted the sharer set; 10.5 released dirty data to nowhere; 10.6 read a cell's state but not its action.
This chapter collects them. Each was a specific failure; together they form a taxonomy — a short list of families that recur across implementations. And they share a structure: each violates an invariant of the state machine, and each is caught by the corresponding assertion. So 10.7 is both a checklist of what to hunt and an argument for how to hunt it — bind an invariant check for every rule, and the whole family becomes catchable rather than shippable.
5. Core Concept — every state bug violates an invariant
The recurring CHI state bugs are few, and each breaks a specific invariant of the state machine.
- Illegal transition. A move not in the table — the classic being a silent SC → UD (writing a shared line without upgrading). Invariant broken: only legal transitions occur.
- Lost dirty data. A dirty line released with no writeback and no forward (Chapter 10.5), or a cell read for its state but not its action (Chapter 10.6). Invariant: the latest value is conserved.
- Stale sharer. A write that misses a holder — an under-counted sharer set (Chapter 10.4) or a skipped snoop (Chapter 8.2). Invariant: a write invalidates every holder.
- Ownership drift. The directory and a cache disagree on the owner (Chapter 10.3), or a transfer leaves two or zero owners (Chapter 9.6). Invariant: exactly one owner, consistently recorded.
- Incomplete table. A missing (state, event) entry (Chapter 10.2). Invariant: the table is total.
The synthesis:
The common CHI state bugs are a short taxonomy — illegal transition, lost dirty data, stale sharer, ownership drift, incomplete table — and each violates one invariant: legal transitions only, value conserved, every holder invalidated, one owner consistently recorded, total table. Because each bug is a broken invariant, each is caught by an assertion on that invariant — which fires on every case, not just the ones a directed test happened to try.
6. Engineering Mental Model — smoke detectors, not a fire drill
Two ways to guard a building against fire.
- A fire drill rehearses specific scenarios — "a fire starts in the kitchen at 2pm." Useful, but it only covers the scenarios you script. A fire in the basement at 3am, unrehearsed, goes undetected.
- Smoke detectors watch a condition — smoke, anywhere, anytime. They do not care where or when the fire starts; they fire on the property, not the scenario.
- Directed tests are fire drills: they check the cases you imagined. Assertions are smoke detectors: they watch an invariant and fire the moment it is violated, in a corner case no drill rehearsed.
A coherence state machine, like a building, has too many possible scenarios to drill them all. You protect it by wiring detectors on the invariants — one per rule the machine must always obey — so a violation anywhere trips an alarm. The bug families are the fires; the assertions are the detectors.
7. Engineering Diagram — a legal move and an illegal one
Read the two paths: the legal route is SC → UC → UD (upgrade, then write); the illegal shortcut is SC → UD directly, skipping the upgrade that would invalidate the other sharers. The illegal move looks harmless — the line becomes writable — but it leaves stale readers. An assertion that only legal transitions occur fires on it.
8. The Bug Families and Their Invariants
The catalogue, each family paired with its invariant and the assertion that catches it.
| Bug family | Invariant violated | Caught by |
|---|---|---|
| Illegal transition | only legal transitions occur | an assertion on the legal-move set |
| Lost dirty data | the latest value is conserved | a dirty-release routing check |
| Stale sharer | a write invalidates every holder | a set-vs-snoop coverage check |
| Ownership drift | one owner, consistently recorded | a directory/state consistency check |
| Incomplete table | the table is total | a (state, event) coverage check |
The rule to carry: a small taxonomy covers most cache-state bugs, and each maps to a one-line invariant and a matching assertion. This is what makes coherence verification tractable — not enumerating scenarios, but enumerating invariants, and asserting each. The families recur because the invariants are few; assert them all and the families have nowhere to hide.
9. Assertions Catch What Directed Tests Miss
Why the invariant approach beats more directed tests deserves its own statement.
- Directed tests cover scenarios. They check the specific sequences you wrote — a finite, imagined subset.
- State bugs live in corners. They occur in rare interleavings — a snoop arriving mid-transaction, a specific state under a specific event — that no scenario list is complete for.
- Assertions cover the property. An assertion on an invariant fires whenever the invariant breaks, in any scenario, scripted or not.
- So bind the invariants. For each bug family, bind an assertion on its invariant. A corner case that violates it trips the assertion — in simulation, in formal, in emulation — instead of shipping.
The point to carry:
The reason coherence bugs are so dangerous is that they hide in the combinatorial explosion of interleavings, where directed testing is hopelessly incomplete. The reason they are nonetheless catchable is that they all reduce to a handful of invariants — and an invariant is checkable on every state, every cycle, every interleaving at once. The shift is from testing behaviors to asserting properties: you cannot enumerate the ways a state machine can be exercised, but you can enumerate the rules it must never break. Bind a detector to each rule, and the corner cases that defeat directed tests become the exact cases the assertions were built to catch.
10. Walkthrough — a bug the assertion catches
A coherence machine passes its directed suite; watch an assertion catch what the suite missed.
- Directed tests pass. The suite exercises reads, writes, and evictions in the sequences the team scripted. All green.
- A corner case occurs. In the field, a SnpUnique arrives while a line is in SD — a combination the directed suite never sequenced.
- The table has a hole. The controller has no entry for (SD, SnpUnique) — the incomplete-table bug (Chapter 10.2). The line is not invalidated.
- Without an assertion: nothing notices. A stale sharer survives; a later read returns old data — a silent coherence violation shipped to a customer.
- With the invariant assertion: the totality check — every (state, event) has a legal, applied transition — fires the instant (SD, SnpUnique) is hit, flagging the hole in simulation or formal, long before the field.
The bug was identical in both runs; the difference was the detector. The directed suite could not have covered every interleaving, but the assertion covered the invariant across all of them.
11. RTL / Hardware View — an invariant monitor
A coherence invariant monitor watches the state signals and flags any family's violation. Representative — a bundle of the invariant checks as one monitor.
// Representative cache-state invariant monitor (educational).
// Watches the state machine and flags each bug family's invariant violation.
// all_ok is high only when every invariant holds. In practice these become
// concurrent assertions bound to the design.
module chi_state_invariants (
input logic legal_transition, // the move taken is in the table
input logic dirty_released, // a dirty owner gave up the line this event
input logic dirty_routed, // ...and the value went to memory or a peer
input logic write_occurred, // a write to a shared line completed
input logic all_holders_inv, // ...and every holder was invalidated
input logic owner_consistent, // directory owner == owning cache state
input logic table_entry_defined,// the (state,event) had a defined entry
output logic illegal_transition,
output logic lost_dirty,
output logic stale_sharer,
output logic owner_drift,
output logic incomplete_table,
output logic all_ok
);
assign illegal_transition = !legal_transition;
assign lost_dirty = dirty_released && !dirty_routed; // value went nowhere
assign stale_sharer = write_occurred && !all_holders_inv; // a holder survived
assign owner_drift = !owner_consistent; // records disagree
assign incomplete_table = !table_entry_defined; // missing cell
assign all_ok = !(illegal_transition | lost_dirty | stale_sharer |
owner_drift | incomplete_table);
endmoduleThe same behavior in Verilog-2001:
// Representative cache-state invariant monitor (Verilog-2001).
module chi_state_invariants (
input legal_transition, dirty_released, dirty_routed, write_occurred,
input all_holders_inv, owner_consistent, table_entry_defined,
output illegal_transition, lost_dirty, stale_sharer, owner_drift,
output incomplete_table, all_ok
);
assign illegal_transition = !legal_transition;
assign lost_dirty = dirty_released && !dirty_routed;
assign stale_sharer = write_occurred && !all_holders_inv;
assign owner_drift = !owner_consistent;
assign incomplete_table = !table_entry_defined;
assign all_ok = !(illegal_transition | lost_dirty | stale_sharer |
owner_drift | incomplete_table);
endmoduleAnd in VHDL:
-- Representative cache-state invariant monitor (VHDL).
library ieee;
use ieee.std_logic_1164.all;
entity chi_state_invariants is
port (
legal_transition : in std_logic;
dirty_released : in std_logic;
dirty_routed : in std_logic;
write_occurred : in std_logic;
all_holders_inv : in std_logic;
owner_consistent : in std_logic;
table_entry_defined : in std_logic;
illegal_transition : out std_logic;
lost_dirty : out std_logic;
stale_sharer : out std_logic;
owner_drift : out std_logic;
incomplete_table : out std_logic;
all_ok : out std_logic
);
end entity;
architecture rtl of chi_state_invariants is
signal it, ld, ss, od, ic : std_logic;
begin
it <= not legal_transition;
ld <= dirty_released and (not dirty_routed);
ss <= write_occurred and (not all_holders_inv);
od <= not owner_consistent;
ic <= not table_entry_defined;
illegal_transition <= it;
lost_dirty <= ld;
stale_sharer <= ss;
owner_drift <= od;
incomplete_table <= ic;
all_ok <= not (it or ld or ss or od or ic);
end architecture;All three flag each bug family from its invariant and assert all_ok only when every invariant holds. In practice these become concurrent assertions bound to the real design — smoke detectors on the state machine. The DebugLab shows the cost of shipping without them.
12. Verification View — assert the invariants, not the scenarios
The properties are the invariants themselves, one per bug family.
// Bind to the coherence controller (signals as in chi_state_invariants).
// 1. Only legal transitions occur.
property p_legal_only; @(posedge clk) legal_transition; endproperty
// 2. A dirty release always routes the value (never lost).
property p_value_conserved; @(posedge clk) dirty_released |-> dirty_routed; endproperty
// 3. A write invalidates every holder (no stale sharer).
property p_full_invalidate; @(posedge clk) write_occurred |-> all_holders_inv; endproperty
// 4. The directory and cache agree on the owner (no drift).
property p_owner_consistent;@(posedge clk) owner_consistent; endproperty
// 5. Every (state, event) has a defined entry (total table).
property p_table_total; @(posedge clk) table_entry_defined; endpropertyThe system point, beyond the checks:
The five properties above are, in a real sense, the entire coherence contract of the cache state machine — compressed into invariants an assertion engine can watch continuously. That is the deepest takeaway of the module: the states, transitions, and tables all exist to uphold a handful of rules, and the rules are far fewer than the behaviors that could break them. So verification is won not by out-testing the interleavings — an unwinnable race — but by asserting the invariants that no interleaving may violate. A coherence machine shipped behind these assertions is correct not because every scenario was tried, but because every rule was guarded on every scenario, tried or not.
- What it proves: each invariant holds continuously — legal moves, conserved value, full invalidation, one owner, total table.
- What it does not prove: the invariants are complete — the taxonomy covers the common families, not every conceivable bug.
- Bug signature: any invariant assertion firing — the corresponding bug family, caught.
13. Testbench — the monitor flags each family
Drives a healthy state and each violation, checking the monitor flags them.
module tb_chi_state_invariants;
logic legal_transition, dirty_released, dirty_routed, write_occurred;
logic all_holders_inv, owner_consistent, table_entry_defined;
logic illegal_transition, lost_dirty, stale_sharer, owner_drift, incomplete_table, all_ok;
int errors = 0;
chi_state_invariants dut (.*);
task automatic ok_case();
legal_transition=1; dirty_released=1; dirty_routed=1; write_occurred=1;
all_holders_inv=1; owner_consistent=1; table_entry_defined=1; #1;
if (!all_ok) begin errors++; $display("FAIL healthy case flagged"); end
else $display("PASS healthy: all_ok=1");
endtask
initial begin
ok_case();
// Lost dirty: released but not routed.
dirty_routed = 0; #1;
if (!lost_dirty || all_ok) begin errors++; $display("FAIL lost_dirty not flagged"); end
else $display("PASS lost_dirty flagged");
dirty_routed = 1;
// Stale sharer: wrote but not all invalidated.
all_holders_inv = 0; #1;
if (!stale_sharer || all_ok) begin errors++; $display("FAIL stale_sharer not flagged"); end
else $display("PASS stale_sharer flagged");
all_holders_inv = 1;
// Owner drift.
owner_consistent = 0; #1;
if (!owner_drift || all_ok) begin errors++; $display("FAIL owner_drift not flagged"); end
else $display("PASS owner_drift flagged");
owner_consistent = 1;
// Incomplete table.
table_entry_defined = 0; #1;
if (!incomplete_table || all_ok) begin errors++; $display("FAIL incomplete_table not flagged"); end
else $display("PASS incomplete_table flagged");
if (errors == 0) $display("ALL TESTS PASSED");
else $display("%0d FAILURE(S)", errors);
$finish;
end
endmoduleExpected output:
PASS healthy: all_ok=1
PASS lost_dirty flagged
PASS stale_sharer flagged
PASS owner_drift flagged
PASS incomplete_table flagged
ALL TESTS PASSED14. DebugLab — a corner-case bug that shipped past directed tests
A corner-case bug that shipped past directed tests
CORNER-CASE STATE BUG UNGUARDED BY ASSERTIONS -> SILENT FIELD FAILUREThe design passes every directed test and every regression, ships, and then shows rare, hard-to-reproduce data corruption in the field — a stale read or a lost write that appears under heavy, specific multi-core contention and vanishes when probed.
A corner case hit an unguarded rule:
directed suite: all sequences GREEN
field interleaving: SnpUnique arrives while line is in SD
-> (SD, SnpUnique) undefined in the table (a hole)
-> line not invalidated (illegal/undefined move)
-> stale sharer survives a write -> corruption
NO assertion on totality / legal transitions -> nothing fired
bug reproduced only 1 in millions of cycles under contentionThe rule was broken; no detector was watching that rule.
Verification relied on directed scenarios and had no assertions on the state-machine invariants. From that point any corner case outside the scripted sequences could violate a rule undetected — and one did.
State bugs live in interleavings directed tests cannot enumerate, but they all break invariants an assertion can watch continuously. Testing behaviors is an unwinnable race against the combinatorial explosion of interleavings; the corner case that shipped was simply one the suite never sequenced. Because the bug violated an invariant — a legal, total transition — an assertion on that invariant would have fired on the very first occurrence, in simulation or formal. The failure was not too little testing but the absence of invariant checks, distinct from any single earlier bug (this is the meta-lesson): the families of Chapters 10.1–10.6 are only safe when each is guarded by its assertion.
Bind concurrent assertions on every state-machine invariant — legal transitions only, dirty value conserved, every holder invalidated, one consistent owner, total table — so any corner case that violates a rule fires in verification, not the field. Assert the properties, not the scenarios: the chi_state_invariants flags become SVA assertions on the real controller, watching every state and cycle. A machine guarded by its invariants is correct across interleavings no test could reach.
15. Common Mistakes
- Testing scenarios, not invariants. Assumption: directed tests suffice. Bug: corner-case field failure (the DebugLab). Prevention: assert the invariants.
- Silent illegal transitions. Assumption: an undefined move is harmless. Bug: coherence violation. Prevention: assert legal-only.
- Unrouted dirty releases. Assumption: a state change needs no data. Bug: lost value (Chapter 10.5). Prevention: assert conservation.
- Partial invalidation. Assumption: a subset suffices. Bug: stale sharer (Chapter 10.4). Prevention: assert full invalidation.
- Directory drift. Assumption: one record is enough. Bug: owner drift (Chapter 10.3). Prevention: assert consistency.
- Table holes. Assumption: rare cells can be skipped. Bug: incomplete table (Chapter 10.2). Prevention: assert totality.
16. Engineering Checklist
- Know the families — illegal transition, lost dirty, stale sharer, owner drift, incomplete table.
- Map each bug to the invariant it violates.
- Bind a concurrent assertion on every invariant.
- Assert properties, not scenarios — cover all interleavings.
- Run the assertions in simulation, formal, and emulation.
- Treat any firing assertion as a coherence bug caught before the field.
17. Key Takeaways
- CHI cache-state bugs form a short taxonomy: illegal transition, lost dirty data, stale sharer, ownership drift, incomplete table.
- Each bug violates one invariant of the state machine.
- Assertions on the invariants catch what directed tests miss — every interleaving, not just scripted ones.
- Directed tests cover scenarios; assertions cover properties.
- A machine guarded by its invariants is correct across corner cases no test could reach.
- Assert every rule; the model here is representative.
18. Quick Revision
Common state bugs. CHI cache-state bugs form a short taxonomy, and each violates one invariant: an illegal transition (a move not in the table, like silent SC → UD) breaks legal transitions only; lost dirty data (a dirty release routed nowhere, or a half-read cell) breaks value conservation; a stale sharer (an under-counted set or skipped snoop) breaks a write invalidates every holder; ownership drift (directory and cache disagree, or two/zero owners) breaks one owner, consistently recorded; an incomplete table (a missing cell) breaks totality. The meta-lesson: state bugs hide in interleavings that directed tests cannot enumerate, but every one reduces to a broken invariant an assertion can watch continuously. So the way to ship a correct coherence machine is to bind a concurrent assertion on every invariant — legal moves, conserved value, full invalidation, single consistent owner, total table — so a corner case fires an alarm in verification instead of corrupting data in the field. Assert properties, not scenarios. Representative model; Module 11 turns to the CHI interconnect and its topology.
Coming Next
Chapter 11.1 — Centralised Directory. Module 10 closed the cache state machine; Module 11 turns to the structure that tracks coherence across all of it — the directory. Chapter 11.1 opens with the centralised directory: a single point that records who holds every line, its benefits as a simple source of truth, and the limits — bottleneck and scaling — that push real systems toward the distributed directories the module then explores.