AV-Check

Concept

AV-Check (Architectural Variable Check) is a cross-level comparison operation used in tandem simulation to verify equivalence between the instruction-level architectural variables (ILAVs) of an Instruction-Level Abstraction (ILA) model and the corresponding RTL architectural variables (RTAVs) of an RTL implementation. Any deviation between the two indicates a potential bug in the RTL implementation.

First seen 6/6/2026

Last seen 6/6/2026

Evidence 3 chunks

Wiki v1

WIKI

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.

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

Tandem Simulation ← uses 97% 1e

Tandem simulation checks architectural variables at instruction boundaries

AV-Comparator ← implements 97% 1e

AV-Comparator implements AV checking

LINKED ENTITIES

2 links

Tandem Simulation USES Extracted graph relationship

AV-Comparator IMPLEMENTS Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[1] AV-Check compares ILAVs and RTAVs at the end of each instruction in tandem simulation, and any deviation is a potential bug. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models

[2] In Scenario 1, AV-Check is applied at the end of every instruction; in Scenario 2, AV-Check is applied at predefined points (every P instructions, at a sequence of instruction indices, or when a condition holds), which reduces the per-instruction comparison overhead. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models

[3] The tandem tool generates the instruction monitor, AV-Comparator, and AV-Converter from the refinement map, and the instruction monitor invokes the AV-Comparator (for AV-Check in Scenarios 1-2) or the AV-Converter (for AV-Swap/jump-start in Scenario 3), with correspondence between ILAVs and RTAVs given by the AV map. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models

[4] The checkpoint map defines three types of AV-Check invocations: checkpoint period (P, every P instructions), checkpoint sequence ([t1, t2, ...], at the t_n-th instruction), and checkpoint condition (C, when C holds), and the tandem generator augments the instruction monitor to invoke the AV-Comparator at these checkpoints. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models

[5] Scenario 3 (jump-starting implementation simulation) uses AV-Swap to leave warm-up phases to the ILEM only, and AV-Check is used afterwards to confirm continued equivalence between ILAVs and RTAVs. Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models