Overview

The ADL-driven Validation Framework is a methodology introduced in A Methodology for Validation of Microprocessors using Equivalence Checking (MTV'03). It shifts the notion of "golden" design from the manually written RTL to an automatically synthesized HDL model derived from a formal Architecture Description Language (ADL) specification. By treating the ADL specification as the authoritative description of the processor and using equivalence checking between the synthesized HDL and the RTL implementation, the framework validates that the manually coded RTL design faithfully reflects the architectural intent.

Motivation

Existing formal verification approaches for microprocessors typically:

• Compare a pipelined implementation against a sequential (ISA) specification model, or
• Derive the sequential model from the implementation itself.

These techniques attempt to formally verify the implementation but do not guarantee that the original RTL design is itself golden. Industrial equivalence checkers (e.g., Formality, FormalPro, eCheck, Affirma, Conformal) are traditionally used to compare an RTL design with a modified design (gate-level or revised RTL), assuming the original RTL is golden.

The ADL-driven validation framework is complementary to these approaches: it ensures that the original RTL design is golden.

Framework Workflow

The framework, illustrated in Figure 3 of the source paper, proceeds as follows:

1. Architecture Specification — System architects produce the architecture specification document.
2. Logic Design — Logic designers implement the modules to generate the RTL design.
3. ADL Specification — The first step of the framework is to specify the architecture in the EXPRESSION ADL. The ADL specification itself is validated to ensure the architecture is well-formed.
4. HDL Generation — A synthesizable hardware model (HDL) is automatically generated from the ADL specification.
5. Equivalence Checking — The generated HDL reference model and the manually written RTL design are fed into an equivalence checker. The result is reported as Equivalent or Not Equivalent (with manual feedback when mismatches occur).

This approach reduces the validation problem to checking equivalence of two terms in a logic with equality and uninterpreted function symbols, which is tractable even for complex microarchitectures.

Role of the EXPRESSION ADL

The EXPRESSION ADL captures the structure, behavior, and mapping (between structure and behavior) of a programmable architecture:

• Structure — Viewed as a graph with components as nodes and connectivity as edges.
  • Four component types: units (e.g., ALUs), storages (e.g., register files), ports, and connections (e.g., buses).
  • Two edge types: pipeline edges (instruction transfer between units via pipeline latches) and data transfer edges (data transfer, typically between units and storages or between two storages).
  • Each component carries a list of attributes (e.g., a functional unit has information about latches, ports, connections, opcodes, timing, and capacity).
• Behavior — Organized into operation groups; each group contains a set of operations sharing common characteristics.
• Mapping — Captures how opcodes are mapped to functional units, enabling the decoder to direct instructions through the pipeline.

HDL Generation Pipeline

The synthesizable HDL generator consumes the ADL specification in two main stages:

Decoder

• Extracts opcode, operands, and other information from the input instruction using the instruction format described in the ADL.
• Uses the mapping section of the ADL to perform/initiate necessary functions (e.g., operand read) and decide where (which pipeline latch) to send the instruction.

Datapath

The datapath implementation consists of two parts:

1. Compose each component in the structure using the ADL's functional and parameter information.
2. Instantiate components (fetch, decode, ALU, LdSt, writeback, branch, caches, register files, memories, etc.) and establish connectivity using the appropriate number of pipeline latches, ports, and connections.

For example, to compose an execution unit, the generator instantiates all of its opcode functionalities using the ADL's component description.

Case Study

The paper presents a case study in which the framework is used to validate the DLX architecture via the generated reference model.

Relationship to Other Techniques

• Equivalence Checking — Used as the formal comparison engine between the synthesized HDL reference model and the RTL implementation.
• EXPRESSION ADL — Serves as both the input specification language and the source of the golden reference model.
• Golden Reference Model — The ADL-driven framework produces the golden reference model by automatically synthesizing HDL from the ADL, rather than relying on a hand-written RTL as the golden source.

Limitations and Context

• The framework depends on first validating the ADL specification itself for well-formedness.
• When the equivalence checker reports a mismatch, manual feedback is used to determine whether the discrepancy lies in the RTL implementation or in the ADL specification.
• The technique is presented as complementary to (not a replacement for) sequential-vs-pipelined verification approaches such as unpipelining, Abstract State Machines, controlled token nets, and compositional model checking.