Skip to content
STIMSMITH

Cache Memory Modeling

Concept WIKI v1 · 7/4/2026

Cache Memory Modeling refers to the formal description of processor cache structures and their behavior for the purpose of functional verification and test program generation. It captures buffer configuration attributes and represents cache events (hits, misses) as constraint satisfaction problems (CSPs), enabling automated test data generation through SMT solvers such as Z3.

Overview

Cache Memory Modeling is the activity of formally describing the structure and behavioral characteristics of processor caches so that they can be reasoned about and exercised by automated test-generation tools. In the context of microprocessor verification, the model must capture both the static configuration of cache buffers and the dynamic conditions under which cache events (hits, misses, evictions) occur, including dependencies on prior instructions.

Buffer Configuration Attributes

A cache memory is modeled as a buffer that stores lines of data addressed by main-memory addresses. The following attributes are used to specify buffer configuration:

  • Set size (associativity) — the number of ways in each set.
  • Number of sets — the total number of sets in the cache.
  • Line field description — the structure of a cache line.
  • Address-to-index translation rule — how an address maps to a set.
  • Rule for checking if a line and an address match — the tag-comparison policy.
  • Data displacement policy — the replacement algorithm used when a miss occurs.

These attributes are expressed declaratively using Configuration Facilities (CFs) in tools that target ADL-based design descriptions.

Hit and Miss Modeling as Constraint Satisfaction Problems

For functional verification, the two primary situations of interest are cache hits and cache misses. Both situations can be formulated as Constraint Satisfaction Problems (CSPs) over the address being used to access data and the current state of the buffer. Because architectural specifications typically describe classes of valid parameter values rather than concrete values, expressing these situations as CSPs allows the same model to generate varied test data on each invocation.

Instruction Dependencies

A cache event does not occur in isolation. Instructions modify the state of the microprocessor and therefore affect the behavior of subsequent instructions. For example, a precondition for a cache hit event is that the corresponding data has been loaded into the cache, which requires a previous instruction that accesses the same data line. To produce a complex instruction sequence with predictable results, the sequence must be simulated so that the final parameter values of dependent instructions can be determined. Knowledge about possible dependencies between instructions is part of the Test Knowledge (TK) extracted from Configuration Facilities.

Tool Support: MicroTESK

The MicroTESK test program generator uses the nML/Sim-nML Architecture Description Language to describe target microprocessor designs, including their cache structures. MicroTESK extracts Test Knowledge from ADL specifications and uses it as the basis for creating test scenarios. Test situations that involve caches — such as specifying that an instruction access should produce a hit event in a particular cache level — are expressed in the Test Template Description Language (TTDL).

A TTDL example for cache modeling specifies that for a load instruction the line should cause a cache hit event, naming a set of target caches and the probability of the hit event:

hit([L1(), L2()], [25, 50, 75]);

This statement instructs MicroTESK to generate a list of possible combinations and add an instruction for each one to the resulting test program.

CSP Solver Engine

MicroTESK formulates CSPs using the SMT-LIB language and delegates solving to an external solver. The current implementation uses the Z3 SMT solver from Microsoft Research, with bit-vector support that is well suited to describing data buffers used in different parts of microprocessor models (registers, cache, main memory, etc.). The Test Program generator interacts with the solver through a solver-independent CSP solver API, allowing different solvers to be substituted.

SMT-Based Test Program Generation

The SMT-Based Test Program Generation for Cache-Memory Testing approach, introduced by E. Kornykhin at the East-West Design & Test Symposium (EWDTS) in 2009, frames cache-memory test generation as an SMT problem. This work is part of a broader line of research on generating test data for verification of caching mechanisms and address translation in microprocessors.

Related ADL and Tool References

  • nML / Sim-nML — the ADL formalism used by MicroTESK to describe target microprocessor designs, using a format similar to that found in microprocessor manuals.
  • Mishra, Shrivastava and Dutt (2006) — Architecture Description Language (ADL)-Driven Software Toolkit Generation for Architectural Exploration of Programmable SOCs.
  • Kamkin, Kornykhin and Vorobyev (2011) — Reconfigurable Model-Based Test Program Generator for Microprocessors.

LINKED ENTITIES

2 links
MicroTESK USES
SMT-Based Test Program Generation for Cache-Memory Testing INTRODUCES

CITATIONS

7 sources
7 citations
[1] Buffer configuration information includes set size (associativity), number of sets, line field description, address-to-index translation rule, rule for checking if a line and an address match, and data displacement policy. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[2] Hit and miss situations in a cache buffer can be formulated as CSPs over the address being used to access data and the state of the buffer. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[3] Instruction dependencies are part of Test Knowledge extracted from Configuration Facilities and affect cache modeling because instructions modify the state accessed by subsequent instructions. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[4] TTDL allows test situations involving cache events to be expressed, e.g., `hit([L1(), L2()], [25, 50, 75])`, which specifies target caches and the probability of a hit event occurrence. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[5] MicroTESK uses the SMT-LIB language to formulate CSPs and uses the Z3 SMT solver from Microsoft Research to solve them, with bit-vector support suited to modeling registers, cache, and main memory. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[6] The SMT-Based Test Program Generation for Cache-Memory Testing approach was introduced by E. Kornykhin at the East-West Design & Test Symposium (EWDTS) in 2009. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[7] MicroTESK uses the nML/Sim-nML ADL formalism to describe target microprocessor designs, including their caches, and extracts Test Knowledge from ADL specifications. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors