AV-Check

Overview

AV-Check (Architectural Variable Check) is the core cross-level comparison operation in tandem simulation. It verifies that the architectural variables observed in an instruction-level execution model (ILEM), derived from an Instruction-Level Abstraction (ILA), match the corresponding architectural variables in an RTL execution model (RTEM) generated from a Verilog RTL design [4baa007f]. The check is applied during cross-level execution and is used to detect bugs in the RTL implementation by catching state divergences between the high-level and low-level models.

Purpose and Semantics

In tandem simulation, the ILEM and RTEM are combined into a cross-level execution model (CLEM) that runs instruction-by-instruction. At designated synchronization points, AV-Check ensures that the ILAVs (Instruction-Level Architectural Variables) and the corresponding RTAVs (RTL Architectural Variables) are equivalent [4baa007f]. Any deviation between the two sets of variables is treated as a potential bug, which can then be analyzed with nearby instructions to aid debugging.

The mapping that defines which ILAV corresponds to which RTAV is captured in the AV map, a component of the refinement map used in the ILA verification methodology [a5c566e5, d558de67].

Invocation Scenarios

AV-Check can be invoked at different points in the simulation flow, depending on the chosen tandem simulation scenario:

Scenario 1: Check at every instruction

The AV-Check is performed at the end of every instruction, after the instruction's state updates have been applied in both the ILEM and the RTEM [d558de67]. This is the most thorough form of checking.

Scenario 2: Check at checkpoints

The AV-Check is performed only at predefined points, such as every P instructions or at specific instruction indices [d558de67]. The methodology supports three types of checkpoints, configured via the checkpoint map [a5c566e5]:

1. Checkpoint period (P): invokes checking for every P instructions.
2. Checkpoint sequence ([t1, t2, ...]): invokes checking at the t_n-th instruction.
3. Checkpoint condition (C): invokes checking when condition C holds.

Scenario 2 is used to reduce the performance overhead of doing AV-Check at every instruction, while still covering important verification points [d558de67].

Scenario 3: Jump-starting implementation simulation

In this scenario, the simulation is jump-started by transferring ILAV values into the RTL model (AV-Swap), bypassing certain sections of RTL simulation. AV-Check is then used at appropriate points after the swap to confirm continued equivalence [d558de67, 4baa007f].

Implementation Mechanism

In the generalized tandem simulation flow, the instruction monitor is responsible for detecting instruction boundaries in the RTEM using the instruction map. Depending on the active scenario, the instruction monitor invokes the AV-Comparator (for Scenarios 1 and 2) to perform the AV-Check, or the AV-Converter (for Scenario 3) to perform AV-Swap and jump-start [a5c566e5]. Both the AV-Comparator and AV-Converter are generated automatically by the tandem tool from the refinement map.

The AV-Comparator is the concrete tool/component that implements the AV-Check logic. According to the refinement map, the tandem generator augments the instruction monitor block to appropriately invoke the AV-Comparator at the configured checkpoints [a5c566e5].

Role in the Tandem Simulation Methodology

AV-Check is the principal correctness signal in tandem simulation. By comparing ILAVs and RTAVs at meaningful synchronization points (end of instruction, periodic checkpoints, or condition-triggered checkpoints), it transforms tandem simulation from a pure co-simulation speedup technique into a verification mechanism: deviations surfaced by AV-Check localize potential bugs to specific instructions, and the nearby instructions can then be examined to diagnose the root cause [4baa007f].

See Also

• Tandem Simulation — the cross-level simulation technique that uses AV-Check as its main verification primitive.
• AV-Comparator — the tool that implements AV-Check, invoked by the instruction monitor.
• AV-Converter — the companion tool used in Scenario 3 for AV-Swap and jump-start.
• Refinement Map — the data structure (containing the AV map and checkpoint map) from which the AV-Check logic is derived.