Cache Coherence Verification

Overview

Cache coherence verification is the discipline of checking that a processor implementation correctly enforces its cache coherence protocol, so that loads, stores, refills, and invalidations across the cache hierarchy produce an architecturally consistent view of memory. It is pursued at two complementary levels in the XiangShan ecosystem: (1) as a verification event class within a full-processor hardware-accelerated co-simulation (DiffTest-H), and (2) as a dedicated target of a unit-level cache verification framework (TL-Test) that exercises the cache subsystem in isolation.

Cache Coherence as a Verification Event in Co-Simulation

In the DiffTest-H framework, verification events are organized into six representative categories spanning the architectural surface of an out-of-order RISC-V processor:

Cache coherence events fall under the Memory Hierarchy category, one of the six representative event types. Across the full DiffTest-H framework, 32 distinct verification event types are covered, including instructions, cache coherence, TLB, vectorization, and virtualization.

Role in Co-Simulation Verification

During co-simulation:

1. The DUT emits verification events — including cache coherence events such as refill transactions and protocol messages — to the REF.
2. Deterministic events (DEs) such as ordinary instruction commits are stepped and compared by the REF independently.
3. Non-deterministic events (NDEs) such as external interrupts and MMIO accesses are synchronized from the DUT to the REF at precise instructions and then compared.
4. On any mismatch between the DUT's emitted state (including cache coherence state) and the REF's expected state, the co-simulation is aborted.

The hardware–software communication that carries cache coherence events, like all verification events, is a point-to-point interaction that can be modeled by the LogGP model and dominates the co-simulation time when not optimized — over 98% of co-simulation time is consumed by communication overhead in unoptimized setups.

Three Semantic Properties Used in Optimization

Verification events, including cache coherence events, carry three key semantic properties that frameworks exploit to optimize communication while preserving debuggability:

1. Structural Semantics — the length and data structure of each event. Cache coherence events have variable-length payloads, so tight packing (allocating space according to length) eliminates bubble padding that fixed-width schemes incur.
2. Order Semantics — the specific checking order of events. Decoupling communication from checking order via order tags allows cache coherence events to be fused and reordered at the software side, even when interleaved with NDEs such as external interrupts.
3. Behavioral Semantics — the architectural behavior checked, which localizes errors to specific microarchitectural components (e.g., a particular coherence state, directory, or snoop port).

Significance in Bug Detection

In DiffTest-H's evaluation on XiangShan — a 6-wide out-of-order RISC-V processor — the framework achieves simulation speeds of 478 KHz on the Cadence Palladium emulator and 7.8 MHz on the Xilinx VU19P FPGA, representing 80× and 78× speedups over the baseline DiffTest, 273× and 1945× faster than 16-thread Verilator, and 7.8× faster than the prior state-of-the-art on the FPGA. DiffTest-H reduces communication overhead by 99.84% on the emulator.

Over 151 complex bugs in XiangShan were uncovered that required up to 2 months to identify with Verilator-based simulation but were detected within 11 hours by DiffTest-H on Palladium. All of these bugs have been confirmed and fixed by XiangShan developers, totaling more than 780 lines of code change across 19 pull requests. Cache coherence bugs are a notable class within these, given that the memory-hierarchy event category (which subsumes coherence events) is one of the six representative categories the framework explicitly models.

Unit-Level Cache Verification with TL-Test

While DiffTest-H verifies cache coherence in the context of full-processor co-simulation, the XiangShan project also provides a dedicated unit-level framework for exercising cache coherence directly on the cache design.

TL-Test is a Unit Level Verification Framework for the cache system. As an infrastructure for cache verification, it:

• Supports the TileLink protocol and cache coherence check.
• Can generate testcases or run constrained-random tests quickly to exercise the cache.
• Supports converting real cache access traces into a testbench via its tl-trace mode, so that a trace dumped from the whole XS-Core can be replayed against the cache system alone as a trace-driven model.
• Uses tl-trace mode for fast reproduction of functional bugs and analysis of performance problems.

A typical TL-Test workflow (as documented in the XiangShan ASPLOS '25 tutorial):

1. Run the pre-compiled TL-Test, which generates a constrained-random testcase and flags mismatches. For example, an injected bug in the GrantBuffer of the CoupledL2 (wrongly shifting the Grant Data on the L2→L1 path, d.data := data << 8 instead of d.data := data) is detected at address 0x4000.
2. Analyze the failure by querying the TL-Log / chiselDB for all transactions on the effective address. The TL-Log pinpoints the wrong transaction and the precise cycle number, enabling quick root-cause analysis.

This complements DiffTest-H: TL-Test isolates cache coherence failures at the unit level with reproducible trace-driven or constrained-random stimuli, while DiffTest-H catches coherence violations that only manifest in full-processor execution.

Related Frameworks

• DiffTest-H — A semantic-aware, hardware-accelerated co-simulation framework that uses cache coherence verification (and 31 other event types) to validate the XiangShan RISC-V processor. It introduces three optimizations: Batch (packing), Squash (fusion with decoupled checking order), and Replay (preserving instruction-level debuggability).
• TL-Test — A unit-level TileLink/cache coherence verification framework that performs constrained-random and trace-driven (tl-trace) testing of the cache subsystem in isolation, and produces TL-Log traces for debugging.