AV Map

Definition

An AV Map (Architectural Variable Map) is a mapping structure that defines the correspondence between ILAVs (Instruction-Level Abstraction Architectural Variables) in a high-level ILA model and RTAVs (RTL Architectural Variables) in the corresponding RTL implementation. It forms one of the main fields of the broader refinement map used to support cross-level verification via tandem simulation.

The AV map answers the question "what to check" — i.e., which state variables on the ILA side correspond to which state variables on the RTL side, and therefore must be compared for equivalence during simulation.

Role within the Refinement Map

The AV map is a constituent part of the Refinement Map, which is used in formal verification of processors and accelerators. The refinement map's two primary fields are:

1. AV map — defines the mapping from ILAVs to their corresponding RTAVs (e.g., RTAV1 in the ILA model corresponds to ILAV1, and the two are checked for equivalence).
2. Instruction map — defines the time or condition when each instruction starts and finishes in the RTL implementation, indicating the correspondence points at which RTAVs should be checked against ILAVs.

Together, these two fields specify the key information needed for verification: what to check and when to check it.

Use in Tandem Simulation

In the generalized tandem simulation flow, the AV map is consumed by the tandem tool to generate two key blocks:

• AV-Comparator — used in Scenarios 1 and 2 of tandem simulation, invoked by the instruction monitor to check AVs for equivalence at instruction boundaries.
• AV-Converter — used in Scenario 3, responsible for swapping AVs and performing jump-start operations.

Both of these generated blocks are based on the AV map, which provides the correspondence between ILAVs and RTAVs. The instruction monitor detects instruction boundaries (when an instruction starts or finishes) in the RTEM and invokes the AV-Comparator or AV-Converter as appropriate, relying on the AV map to identify which variable pairs must be handled.

Example

In the AES-ILA / AES-RTL refinement map (derived from earlier ILA refinement work), the AV map entries specify, for instance, that the RTL signal top.aes_key_reg_out from the AES-Block implementation corresponds to the ILA variable key in the AES-ILA model. The set_key instruction row further indicates that the corresponding instruction starts when the decode function is true and finishes after executing one RTL cycle — and the AV map identifies that during this interval, the key ILAV and the corresponding RTAV are the variables to be compared.

Relation to Other Concepts

• The AV Map is a part of the Refinement Map in the tandem simulation framework.
• The Tandem Simulation technique relies on the AV map (together with the instruction map) to drive the AV-Comparator and AV-Converter blocks that enforce ILA–RTL equivalence.