Cache Coherence Verification

Concept

Cache coherence verification is the discipline of validating that a processor design correctly maintains consistency across its cache hierarchy and memory subsystem, ensuring all memory accesses observe a coherent view of shared data. It is exercised both as a first-class class of verification events in hardware-accelerated co-simulation frameworks (e.g., DiffTest-H covering 32 event types on XiangShan) and as the dedicated target of unit-level cache verification frameworks (e.g., TL-Test, which checks TileLink protocol behavior and coherence directly on the cache design).

First seen 6/6/2026

Last seen 6/6/2026

Evidence 3 chunks

Wiki v2

WIKI

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.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

2 connections

DiffTest-H ← uses 90% 1e

DiffTest-H covers cache coherence as one of its verification event types.

TL-Test ← implements 98% 1e

TL-Test supports TileLink protocol and cache coherence checking as a cache verification framework.

LINKED ENTITIES

1 links

TL-Test IMPLEMENTS Extracted graph relationship

CITATIONS

9 sources

9 citations — click to expand

[1] DiffTest-H covers 32 types of verification events, including instructions, cache coherence, TLB, vectorization, and virtualization. DiffTest-H: Toward Semantic-Aware Communication in Hardware-Accelerated Processor Verification (MICRO '25)

[2] Verification events are organized into six representative categories (Control Flow, Register Updates, Memory Access, Memory Hierarchy, RISC-V Extensions, …) with the Memory Hierarchy category containing six representative event types such as cache refill operations and L1/L2 TLB operations. DiffTest-H: Toward Semantic-Aware Communication in Hardware-Accelerated Processor Verification (MICRO '25)

[3] The three semantic properties (Structural Semantics, Order Semantics, Behavioral Semantics) of verification events can be exploited to optimize communication while preserving debuggability. DiffTest-H: Toward Semantic-Aware Communication in Hardware-Accelerated Processor Verification (MICRO '25)

[4] Hardware–software communication is a point-to-point interaction that can be modeled by the LogGP model, and over 98% of co-simulation time is consumed by communication overhead in unoptimized setups. DiffTest-H: Toward Semantic-Aware Communication in Hardware-Accelerated Processor Verification (MICRO '25)

[5] DiffTest-H achieves 478 KHz on Palladium and 7.8 MHz on FPGA, 80× and 78× over baseline DiffTest, 273× and 1945× over 16-thread Verilator, and reduces communication overhead by 99.84% on the emulator. DiffTest-H: Toward Semantic-Aware Communication in Hardware-Accelerated Processor Verification (MICRO '25)

[6] DiffTest-H uncovered over 151 complex bugs in XiangShan that required up to 2 months to identify with Verilator but were detected within 11 hours on Palladium; all bugs were fixed across 19 pull requests with more than 780 lines of code change. DiffTest-H: Toward Semantic-Aware Communication in Hardware-Accelerated Processor Verification (MICRO '25)

[7] TL-Test is a Unit Level Verification Framework for the cache system that supports the TileLink protocol and cache coherence check, can generate testcases or constrained-random tests quickly, and supports converting real cache access traces into a testbench via tl-trace mode for fast reproduction of functional bugs and analysis of performance problems. XiangShan ASPLOS '25 Tutorial — Function Verification (TL-Test section)

[8] An injected cache coherence bug that incorrectly shifts the Grant Data on the L2→L1 path (d.data := data << 8 instead of d.data := data) is detected by TL-Test at address 0x4000, and is analyzed via TL-Log / chiselDB queries over the effective address to identify the wrong transaction and cycle number. XiangShan ASPLOS '25 Tutorial — Function Verification (TL-Test section)

[9] In the DiffTest-H co-simulation workflow, deterministic events (DEs) such as ordinary instruction commits are stepped and compared by the REF independently, while non-deterministic events (NDEs) such as external interrupts and MMIO accesses are synchronized from the DUT to the REF at precise instructions; any mismatch aborts co-simulation. DiffTest-H: Toward Semantic-Aware Communication in Hardware-Accelerated Processor Verification (MICRO '25)