Skip to content
STIMSMITH

Checkpoint Map

Concept WIKI v1 · 6/6/2026

A checkpoint map is an optional field of the ILA refinement map, introduced to support tandem simulation. It specifies when the AV-Comparator should be invoked by defining checkpoint periods, sequences, or conditions during instruction-level execution of the RTL executable model (RTEM).

Checkpoint Map

A checkpoint map is an optional field of the ILA refinement map that specifies when the architectural variables (AVs) of the instruction-level architecture (ILA) model should be compared against the corresponding RTL architectural variables (RTAVs) of the RTL executable model (RTEM) during tandem simulation.

Origin and Context

The checkpoint map is one of two optional fields added to the original ILA refinement map (introduced in formal verification work for processors and accelerators) to support the generalized tandem simulation methodology. As stated in the source: "(iv) Checkpoint map and (v) 'cold start' map: are not part of the original ILA refinement map [8] and have been added as part of this work to support tandem simulation."

Position Within the Refinement Map

The refinement map defines two main fields — the AV map (specifying what to check, i.e., the correspondence between ILAVs and RTAVs) and the instruction map (specifying instruction start/finish boundaries in the RTL implementation). It additionally supports three optional fields: the interface map, the checkpoint map, and the "cold start" map.

Three Types of Checkpoints

The methodology augments the refinement map with the checkpoint map to support the following three types of checkpoints, used in Scenario 2 of tandem simulation (periodic checking of AVs):

  1. Checkpoint period (P) — invokes checking for every P instructions.
  2. Checkpoint sequence ([t1, t2, ...]) — invokes checking at the n-th instruction, where the instruction index belongs to the supplied sequence (e.g., checking at instruction t1, t2, and so on).
  3. Checkpoint condition (C) — invokes checking when a Boolean condition C holds (e.g., (commit == 1)).

Role in the Tandem Simulation Flow

According to the refinement map and checkpoint map, the tandem generator automatically augments the instruction monitor block (one of the auxiliary blocks in the tandem simulation flow) to invoke the AV-Comparator at the appropriate moments. The instruction monitor uses the instruction map to detect instruction start/finish boundaries in the RTEM, while the checkpoint map determines the additional points at which AV comparison should be triggered.

See Also

  • Refinement Map — the parent structure that contains the checkpoint map as one of its optional fields.
  • Tandem Simulation — the simulation technique that consumes the checkpoint map to drive periodic AV comparisons.

CITATIONS

4 sources
4 citations
[1] The checkpoint map is an optional field (iv) of the ILA refinement map, added as part of this work to support tandem simulation, and is not part of the original ILA refinement map [8]. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models
[2] The checkpoint map supports three types of checkpoints: Checkpoint period (P) invoking checking every P instructions, Checkpoint sequence ([t1, t2, ...]) invoking checking at the tn-th instruction, and Checkpoint condition (C) invoking checking when condition C holds. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models
[3] According to the refinement map, the tandem generator augments the instruction monitor block to appropriately invoke the AV-Comparator at the checkpoints defined by the checkpoint map. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models
[4] The refinement map defines two main fields (AV map and instruction map) specifying what to check and when to check, with the checkpoint map providing an additional mechanism for periodic checking in Scenario 2. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models