Architecture Description Language Wiki

Overview

An Architecture Description Language (ADL) is a language used to capture an architecture specification so that downstream design, simulation, compilation, exploration, or validation artifacts can be generated from it. In a language-driven design-space exploration flow for programmable embedded systems, the processor, coprocessor, and memory subsystem are captured using an ADL; the ADL specification is then used to generate a software toolkit including a compiler, simulator, and assembler, and to provide architectural-quality feedback to the designer. [C1]

In test-program-generation frameworks for microprocessors, an ADL serves as the input format for a translator that builds a design model and a coverage model of the microprocessor under test; test templates written in a separate template description language (TDL) then use those models to drive test-program generation. [C2]

The MicroTESK line of work explicitly motivates using ADLs for test-program generation by noting that ADLs are "commonly used in the area of functional simulation," and that an architecture specification (AS) in an ADL can be used by a tool to automatically build a microprocessor's instruction-set model (ISM) and testing knowledge (TK); ADL-based specification together with lightweight configuration files (CFs) for subsystems that are hard to express in ADLs is summarized by the formula TPs = AS + CFs. [C3]

Processor-oriented ADLs are also discussed as inputs for validation flows. In one ADL-driven microprocessor validation methodology, the system architect's knowledge about the behavior of a pipelined architecture is captured through ADL constructs, enabling a top-down approach to architecture validation. [C4]

Test program generation context

The model-based approach to test program generation (TPG) decomposes the generation problem into three inputs—test templates (TTs), testing knowledge (TK), and an instruction-set model (ISM)—and summarizes the overall goal as TPs = TTs + TK + ISM, where TPs are test programs produced by combining TTs with the TK and ISM extracted from an architecture model. [C5]

The cited industrial implementations of model-based TPG are Genesys-Pro (IBM Research Lab), which uses high-level building blocks to build an architecture model and formulates a constraint satisfaction problem (CSP) for each instruction of a test template, and RAVEN (Random Architecture Verification Engine; developed by Obsidian Software Inc., later acquired by ARM), which produces fully random, semi-random, or user-directed test programs and exposes a C++ Generator Construction Set (GCS) API for custom designs. The MicroTESK paper notes as a known weakness of Genesys-Pro that modeling instructions affecting memory devices is difficult, making significant memory-subsystem modifications costly. [C6]

Three families of test-program generation approaches appear across the cited literature:

Random generation, which produces complex but unsystematic test programs and is the basis of tools such as RAVEN, which combines randomization with information about common microprocessor faults. [C7]
Combinatorial generation, based on the observation that many bugs are triggered by short instruction sequences (typically 2–5 instructions); the first version of MicroTESK from ISPRAS followed this approach, supporting hierarchical decomposition of a test program generator into iterators and combinators and constructing branch instructions by enumerating control-flow graphs with bounded depth-first exploration. [C8]
Template-based generation, in which test templates are abstract representations of test programs with constraints on possible operand values; templates can be hand-written or automatically generated and are then turned into concrete test programs by solving the constraints. [C9]

The MicroTESK paper additionally surveys academic ADL-based approaches to TPG, including the Mishra–Dutt graph-based functional test generation that uses the EXPRESSION ADL to build a graph-based coverage model and constructs tests as counterexamples for the negation of target test situations via model checking, and the Koo–Mishra SAT-based bounded model checking (BMC) technique that improves time and space for counterexample generation over ordinary model checking. [C10]

ADL-driven test program generation via SMV model checking

The Mishra–Dutt approach specifies the processor architecture in an ADL (EXPRESSION ADL) and verifies the correctness of the ADL specification itself; the verification engineers then write properties that the architecture should satisfy, and the processor model is generated from the architecture specification. Both the processor model and the properties are described using the SMV (Symbolic Model Verifier) language, and the SMV model checker produces counterexamples (instruction sequences) for the negations of the target properties. These counterexamples are converted into complete tests—instruction sequence followed by expected results—using a cycle-accurate structural simulator that is itself generated automatically from the ADL specification. [C11]

The DLX processor is used as the case study for this ADL→SMV flow. The EXPRESSION ADL specification of DLX captures its pipeline and data-transfer paths, structural components (units, storages, ports, connections), behavioral description of the instruction set, and the mapping between structure and behavior (including hazards, stalls, interrupts, and exceptions). [C12]

From the ADL specification, the SMV description of the DLX architecture is generated automatically using a library of generic architectural components; the cited DLX SMV description totals 354 lines of code built from pipeline- and cycle-accurate library components. A typical building block is a simplified instruction-fetch unit described in SMV as a module with input/output ports (e.g., PC, InstMemory, operation) and initial/next relations. [C13]

Properties are written for each category of testcases considered in the flow—pipeline flow (operation timing, hazards, stalls, exceptions), feedback paths, branch prediction, execution style, and memory controller (store-to-load forwarding, TLB miss)—and the methodology iterates: when the coverage report from the simulator-driven tests shows that coverage is insufficient, more properties are added until the requirement is met. [C14]

For coverage estimation, the ADL-based methodology proposes a functional coverage metric tied directly to the specification rather than to code/toggle/fault coverage, allowing verification engineers to define exactly which device functionality is monitored. [C15]

Instruction-level vs. microarchitectural models

The test-program-generation literature distinguishes between instruction-level descriptions and microarchitectural descriptions. Instruction-level ADLs describe the programmer's view of a microprocessor—how to write programs for it—while microarchitectural descriptions capture the internal structure of the microprocessor—the computer engineer's point of view. Test-program generation methods and tools typically use instruction-level models, but only a few use microarchitectural models; the latter are called model-based. [C16]

Generated artifacts and design-space exploration

The cited literature identifies ADL-driven software-toolkit generation and design-space exploration as a substantial research area for processor-based embedded systems. Academic examples named in the evidence include ISDL, MIMOLA, LISA, EXPRESSION, and nML; the same passage also lists industrial examples such as ARC, Axys, RADL, Target, Tensilica, and MDES. [C17]

The Vienna Architecture Description Language (VADL) is a recent processor description language that enables concise formal specification of processor architectures. A distinctive feature of VADL is the separation of the instruction set architecture (ISA) specification from the microarchitecture (MiA) specification, allowing different ISAs to be combined with different MiAs. A single VADL processor specification can be used to automatically generate assemblers, compilers, linkers, functional instruction-set simulators, cycle-accurate instruction-set simulators, synthesizable hardware-description-language specifications, test cases, and documentation. The original VADL implementation had a restricted copyright, motivating the open-source OpenVADL implementation. [C18]

EXPRESSION ADL

EXPRESSION ADL is used in the cited validation work to capture both the structure and behavior of a processor. From the EXPRESSION ADL specification, the methodology generates a synthesizable RTL description of the architecture and uses that generated RTL as a golden reference model for equivalence checking against an implementation. The approach was demonstrated on a RISC DLX architecture. [C19]

EXPRESSION ADL is described as supporting automatic software-toolkit generation and design-space exploration across a wide range of processors and memory subsystems, including DSP, VLIW, EPIC, and superscalar processors. [C20]

The language captures three related aspects of a programmable architecture: structure, behavior, and the mapping between structure and behavior. Structurally, a processor is modeled as a graph whose nodes are components and whose edges represent connectivity. The evidence names four component types—units such as ALUs, storages such as register files, ports, and connections such as buses—and distinguishes pipeline edges from data-transfer edges. A pipeline path is a path from a root node (e.g., Fetch) to a leaf node (e.g., WriteBack) through units and pipeline edges, and denotes an execution flow in the pipeline taken by an operation (e.g., ⟨IF, ID, DIV, MEM, WB⟩). A data-transfer path is a path from a unit to a storage or vice versa through storages and data-transfer edges (e.g., ⟨MEM, MEMORY⟩). Each component carries attributes such as latches, ports, connections, opcodes, timing, and capacity. [C21]

In EXPRESSION ADL, behavior is organized into operation groups, each containing operations with common characteristics. The mapping section records how opcodes map to functional units; this information can be used by a decoder to extract opcode and operand information and decide where an instruction should be sent in the pipeline. [C22]

In the Mishra–Dutt directed TPG approach, detailed EXPRESSION specifications are translated into SMV descriptions, and a fault model covering registers, individual operations, pipeline paths, and interactions between operations is used to drive test generation. The cited authors note that this technique does not scale well on complex microprocessor designs and propose combining it with hand-written template-based generation that targets pipeline hazards, using a graph model extracted from the specification. [C23]

Validation and formal verification

A recurring motivation for ADL-driven validation is the lack of a golden reference model in processor validation. In the EXPRESSION-based methodology, a synthesizable HDL/RTL model is generated from the ADL specification and used as the golden reference model for equivalence checking against the original RTL design; the technique is described as complementary to traditional industrial equivalence-checking flows such as Formality, FormalPro, eCheck, Affirma, and Conformal. [C24]

Formal-verification work also treats an architecture description as the starting point for automatically generating a complete property suite for processors. In that approach, the user defines mapping functions that connect abstract architectural concepts to the RTL implementation, including pipeline stages, stall signals, cancel signals, and similar implementation objects. The property-generation approach is implemented in the tool FISACO and was demonstrated on an industrial control processor used in embedded automotive systems, with OneSpin 360 MV used as the verification engine. [C25]

The same formal-verification source notes a limitation of then-common ADL tool chains: languages such as Facile and LISA supported automatic generation of simulators, assemblers, or compilers, but formal verification of the design functionality was not yet part of that tool chain. [C26]

MicroTESK and Sim-nML / nML as an ADL-driven testing tool chain

MicroTESK is an extendable framework for test-program generation whose modeling framework is built around formal specifications written in an ADL. MicroTESK divides the framework into a modeling framework and a testing framework: the modeling framework processes ADL specifications through a translator to produce a design model and a coverage model, while the testing framework consumes those models, together with test templates written in a TDL, to produce test programs. [C27]

The MicroTESK pipeline has four stages, each operating on data produced by the previous stage: (1) creation of a design description in an ADL and configuration of the design subsystems, performed by a modeling engineer; (2) translation of the design description and configuration into the architectural model (ISM and TK) by a translator that uses unified building blocks from a model library; (3) creation of test templates, either automatically by a TT generator or manually by a verification engineer; (4) generation of test programs by processing templates, solving constraint-satisfaction problems for test situations, and assembling the result into an assembler program. Because the architectural model representation is independent of any particular ADL, adding support for a new ADL only affects the translator. [C28]

Within MicroTESK, the translator is organized into a front-end plus two back-ends—a model generator that constructs an executable design model and a coverage extractor that builds a coverage model for the microprocessor instructions—and is supported by a modeling library split into design and coverage libraries. [C29]

The core of the MicroTESK modeling framework describes registers (as variables storing fixed-size bit vectors), memory (as an array of machine words), and instructions (as atomic operations over registers and memory). More detailed specifications are provided by model extensions, including standard extensions for memory management (cache hierarchy, address translation mechanisms) and pipelining (interconnection between pipeline stages, control-flow transfers); each such extension has its own extension points for further customization (e.g., cache replacement strategy or pipeline-stage behavior). [C30]

At the time of the cited MicroTESK paper, the framework supported two ADLs at the instruction level: nML, which describes a microprocessor at the instruction-set level hiding unnecessary low-level details and is flexible and easy to use, and Sim-nML, which allows instructions to use the predefined function UNPREDICTABLE to indicate situations where the design's behavior is undefined; analysis of control and data flow in instruction specifications supports automatic extraction of a coverage model, instructions can be grouped to provide information useful inside test templates, and the framework is able to predict the result of test-program execution from the specification. [C31]

As a concrete example, the MIPS ADD instruction ADD rd, rs, rt can be specified in nML as an ALU operation; analysis of such specifications yields three classes of conditions that the test generator must reason about: (1) sign-extension constraints on the 32-bit operands rs and rt (otherwise the result is UNPREDICTABLE and should be avoided in tests), (2) 32-bit two's-complement overflow (in which case the destination register rd must not be modified and the IntegerOverflow exception must be raised), and (3) normal execution (sign-extended 32-bit result placed into rd). The constraint-solver engine computes exact operand values for each case. [C32]

Because ADLs such as Sim-nML are not well suited to describing subsystems such as the memory management unit (MMU) or the pipeline control unit (PCU), MicroTESK augments the ADL description with lightweight configuration files (CFs) for those subsystems. For caches and translation look-aside buffers (TLBs), a buffer is represented as an array of sets of lines, where each line is a structure comprising several bit-vector fields; buffer configuration specifies attributes such as set size (associativity), number of sets, line fields, and replacement behavior on misses. [C33]

MA2TG: ADL-driven constraint-based functional test generation

MA2TG (Microprocessor Architecture Automatic Test Program Generator) is a specification-driven, constraint-solving-based test-program generator for advanced microprocessors. It accepts the microprocessor model in the form of an ADL specification, simplifying architecture modeling and easing the adoption of architecture modifications, and can produce both random test programs and sequences of instructions that satisfy a user-specified constraints file. The reported methodology reduces the number of test programs required for microprocessor verification and the associated verification time, and was applied to the DLX processor as a demonstration. [C34]

The MA2TG work situates itself within a broader line of constraint-satisfaction and pseudo-random test-generation techniques—including AVPGEN, IBM's PowerPC test-program generation, the Automaton coverage-based multiprocessor verification environment, dynamic biased pseudo-random generation for the IBM RISC System/6000, BNF-based automatic test program generation for compatible-microprocessor verification, and graph-based functional test program generation for pipelined processors—and uses the EXPRESSION ADL as a representative ADL for modeling. [C35]

Microarchitectural focus and simulator generation

Recent work contrasting ADLs with formal ISA models states that classical ADLs focus more on microarchitectural details such as pipelining and caching. Because of that focus, the source says they can be difficult to integrate with existing simulators and vendor-supplied components, and are therefore primarily used to generate new simulators rather than to integrate into existing ones. [C36]

Related formal ISA modeling: Sail

Sail is described in the cited RISC-V generation work as a domain-specific language for ISA semantics. From a Sail model of an ISA, formal descriptions can be generated in programming and theorem-proving languages such as C, OCaml, Coq, Isabelle, and HOL4, and Sail has been used to model RISC-V, ARM-v8, and MIPS ISAs. The same source notes that Sail's completeness adds complexity, including modeling of address translation and instruction decoding, and that Sail therefore generates a standalone ISA simulator rather than integrating easily into an existing RISC-V simulator. [C37]

Extensions beyond classical processor ADLs

The ADL concept has also been applied outside conventional processor-design flows. QADL, the Quantum Architecture Description Language, is presented as a prototype specification language and environment for quantum-software architecture. It is inspired by classical ADLs and provides a graphical interface for quantum-software components, a parser for syntactical correctness, and an execution environment integrated with IBM Qiskit; an initial evaluation used quantum algorithms such as Quantum Teleportation and Grover's Search. [C38]

Operation-state-machine formulation

Beyond EXPRESSION-style and template-driven approaches, the cited literature describes a microprocessor specified as an operation state machine (OSM); this formal model is one of the alternatives discussed for ADL-based test-program generation. [C39]