Architecture Description Language
ConceptAn Architecture Description Language (ADL) is a formal notation used to capture a processor or other computational architecture so that downstream artifacts—compilers, simulators, assemblers, synthesizable HDL/RTL reference models, design-space exploration tools, test-program generators, and formal-verification property suites—can be generated or driven from a single source. The evidence covers classical processor ADLs such as EXPRESSION ADL, nML, and Sim-nML; ADL-driven functional test-program generators such as MA2TG and the MicroTESK framework; the industrial test-program generators Genesys-Pro and RAVEN; recent processor description languages including VADL/OpenVADL; and extensions of the ADL concept to non-classical domains such as QADL for quantum software.
First seen 5/26/2026
Last seen 7/4/2026
Evidence 19 chunks
Wiki v7
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]
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
13 connectionsLISA is an ADL tool for automatic generation of simulators and compilers for processors.
MicroTESK uses ADL descriptions to configure the test program generator for target microprocessors.
EXPRESSION is an ADL used for microprocessor specifications.
EXPRESSION is a language for architecture exploration and serves as an ADL.
Minimally Invasive Generation of RISC-V Instruction Set Simulators from Formal ISA Models ← mentions 90% 1e
The paper mentions ADLs as related prior work
ISDL is an architecture description language for processor design.
MIMOLA is an architecture description language for processor design.
LISA is an architecture description language for processor design.
nML is an architecture description language for processor design.
MA2TG uses ADL specification to simplify microprocessor architecture modeling.
Sim-nML is an ADL supported by MicroTESK for instruction-level specifications.
The paper mentions ADL-based approaches and their limitations compared to the proposed method.
Facile is an ADL-based tool for automatic generation of processor tools.
LINKED ENTITIES
7 linksMicroTESK USES Extracted graph relationship
EXPRESSION ADL EXAMPLE_OF EXPRESSION ADL is repeatedly cited across the evidence as a representative ADL used for toolkit generation, validation, and test-program generation.
Sim-nML EXAMPLE_OF Sim-nML is named in the MicroTESK evidence as one of the ADLs supported for instruction-level microprocessor specification.
nML EXAMPLE_OF nML is named in the MicroTESK evidence as one of the ADLs supported for instruction-level microprocessor specification and is also listed among academic ADLs.
MA2TG USED_BY MA2TG is described in the evidence as an ADL-driven test-program generator that takes ADL specifications as input.
Genesys-Pro REFERENCED_TOOL Genesys-Pro is cited in the MicroTESK paper as an industrial model-based TPG tool that uses high-level building blocks and constraint solving.
Raven REFERENCED_TOOL RAVEN is cited in the MicroTESK paper as a Random Architecture Verification Engine that produces random and user-directed test programs.
CITATIONS
34 sources34 citations — click to expand
[1] An ADL is used to capture the architecture of programmable embedded systems and to drive software-toolkit generation and design-space exploration. MicroTESK: An Extendable Framework for
[2] In test-program-generation frameworks an ADL is processed by a translator to build a design model and a coverage model; test templates in a TDL drive test-program generation. MicroTESK: An Extendable Framework for
[3] MicroTESK uses architecture specifications in ADLs together with configuration files (CFs) for subsystems that are difficult to describe in ADLs, summarized as TPs = AS + CFs; ADLs are commonly used in functional simulation. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[4] Processor-oriented ADLs are inputs for validation flows that capture the system architect's knowledge about pipelined architecture behavior for a top-down validation approach. MicroTESK: An Extendable Framework for
[5] Model-based TPG can be expressed as TPs = TTs + TK + ISM, combining test templates with the testing knowledge and instruction-set model extracted from an architecture model. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[6] Genesys-Pro (IBM Research Lab) and RAVEN (Obsidian Software Inc., acquired by ARM) are industrial model-based TPG tools; Genesys-Pro is reported to be difficult to extend for memory-device changes and RAVEN exposes a C++ Generator Construction Set (GCS) API for custom designs. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[7] Random generation is the basis of RAVEN, which combines randomization with information about common microprocessor faults and can be extended by including custom modules. MicroTESK: An Extendable Framework for
[8] Combinatorial generation enumerates short instruction sequences (2–5 instructions) to cover test situations for individual instructions and inter-instruction dependencies; the first MicroTESK version (ISPRAS) supported hierarchical decomposition into iterators and combinators and constructed branch instructions via control-flow graph enumeration with bounded depth-first exploration. MicroTESK: An Extendable Framework for
[9] Template-based generation uses test templates with constraints on operand values, which are turned into concrete test programs by solving those constraints; templates can be hand-written or generated automatically. MicroTESK: An Extendable Framework for
[10] Mishra–Dutt graph-based functional test generation 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; Koo–Mishra improve time and space for counterexample generation using SAT-based bounded model checking. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[11] Instruction-level ADLs describe the programmer's view of a microprocessor while microarchitectural descriptions capture its internal structure; TPG methods and tools mostly use instruction-level models, with only a few using microarchitectural (model-based) descriptions. MicroTESK: An Extendable Framework for
[12] Academic ADLs include ISDL, MIMOLA, LISA, EXPRESSION, and nML; industrial examples include ARC, Axys, RADL, Target, Tensilica, and MDES. MicroTESK: An Extendable Framework for
[13] VADL enables concise formal specification of processor architectures, separates ISA from microarchitecture, and from a single specification can generate assemblers, compilers, linkers, simulators, synthesizable HDL specifications, test cases, and documentation; OpenVADL is the open-source implementation motivated by the original VADL's restricted copyright. The Vienna Architecture Description Language
[14] EXPRESSION ADL can generate a synthesizable RTL description used as a golden reference model for equivalence checking, demonstrated on a RISC DLX architecture. MicroTESK: An Extendable Framework for
[15] EXPRESSION ADL supports software-toolkit generation and design-space exploration across DSP, VLIW, EPIC, and superscalar processors. MicroTESK: An Extendable Framework for
[16] EXPRESSION ADL models a processor as a graph of components—units, storages, ports, and connections—distinguishes pipeline edges from data-transfer edges, organizes behavior into operation groups, and records opcode-to-functional-unit mapping in a mapping section used by a decoder. MicroTESK: An Extendable Framework for
[17] In EXPRESSION ADL, behavior is organized into operation groups, and the mapping section records how opcodes map to functional units, supporting decoder-based instruction routing. MicroTESK: An Extendable Framework for
[18] The Mishra–Dutt directed TPG approach translates EXPRESSION specifications into SMV descriptions and uses a fault model covering registers, individual operations, pipeline paths, and operation interactions; it does not scale on complex designs and is paired with hand-written template-based test generation targeting pipeline hazards. MicroTESK: An Extendable Framework for
[19] ADL-driven validation can use a synthesizable HDL/RTL model generated from an ADL specification as a golden reference model for equivalence checking, complementary to industrial flows such as Formality, FormalPro, eCheck, Affirma, and Conformal. MicroTESK: An Extendable Framework for
[20] Formal-verification work treats an architecture description as the starting point for automatically generating a complete property suite for processors; user-defined mapping functions connect abstract architectural concepts (pipeline stages, stall/cancel signals) to the RTL implementation. This is implemented in the tool FISACO and was demonstrated on an industrial automotive control processor using OneSpin 360 MV. MicroTESK: An Extendable Framework for
[21] Languages such as Facile and LISA supported automatic generation of simulators, assemblers, or compilers, but formal verification was not yet part of those ADL tool chains. MicroTESK: An Extendable Framework for
[22] MicroTESK is an extendable TPG framework whose modeling framework is built around ADL specifications, with a translator producing a design model and a coverage model consumed by the testing framework together with TDL templates. MicroTESK: An Extendable Framework for
[23] The MicroTESK pipeline has four stages (ADL design description and configuration creation; translation into ISM/TK; test-template creation; test-program generation), and the architectural model representation is independent of any particular ADL so adding a new ADL only affects the translator. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[24] MicroTESK's translator is organized into a front-end plus two back-ends—a model generator producing an executable design model and a coverage extractor producing an instruction coverage model—backed by a modeling library split into design and coverage libraries. MicroTESK: An Extendable Framework for
[25] The MicroTESK modeling framework's core describes registers (fixed-size bit vectors), memory (array of machine words), and instructions (atomic operations over registers and memory), with extensions for memory management (cache hierarchy, address translation) and pipelining (interconnection between pipeline stages, control-flow transfers), each with its own extension points. MicroTESK: An Extendable Framework for
[26] MicroTESK supports nML and Sim-nML for instruction-level microprocessor specification; Sim-nML allows the UNPREDICTABLE function to indicate undefined behavior, supports automatic coverage-model extraction from control/data-flow analysis, allows grouping of instructions for template use, and can predict test-program execution results from the specification. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[27] Analysis of the MIPS ADD instruction specification yields three condition classes for test generation: sign-extension constraints making the result UNPREDICTABLE, two's-complement overflow requiring the destination register not to be modified and IntegerOverflow to be raised, and normal execution placing the sign-extended 32-bit result into the destination register. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[28] Because ADLs like Sim-nML are not suitable for describing the MMU and PCU, MicroTESK augments the ADL description with configuration files (CFs); caches and TLBs are represented as buffers of sets of lines (each line a structure of bit-vector fields) with attributes such as associativity, number of sets, line fields, and replacement behavior. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
[29] MA2TG is a specification-driven, constraint-solving-based test-program generator that takes an ADL specification, produces random test programs and instruction sequences satisfying a constraints file, reduces verification time, and was demonstrated on the DLX processor. MA2TG: A Functional Test Program Generator for Microprocessor Verification
[30] MA2TG situates itself within a line of constraint-satisfaction and pseudo-random techniques including AVPGEN, IBM PowerPC test-program generation, the Automaton multiprocessor verification environment, IBM RISC System/6000 dynamic biased pseudo-random generation, BNF-based automatic test program generation, and graph-based functional test generation for pipelined processors; it uses the EXPRESSION ADL as a representative ADL. MA2TG: A Functional Test Program Generator for Microprocessor Verification
[31] Classical ADLs focus more on microarchitectural details such as pipelining and caching, making them difficult to integrate with existing simulators and vendor-supplied components; they are primarily used to generate new simulators rather than to integrate into existing ones. MicroTESK: An Extendable Framework for
[32] Sail is a domain-specific language for ISA semantics from which formal descriptions can be generated in C, OCaml, Coq, Isabelle, and HOL4; Sail has been used to model RISC-V, ARM-v8, and MIPS ISAs. Its completeness—including address translation and instruction decoding—makes it generate standalone ISA simulators rather than integrating into existing RISC-V simulators. MicroTESK: An Extendable Framework for
[33] QADL is a Quantum Architecture Description Language, a prototype specification language and environment for quantum-software architecture inspired by classical ADLs; it provides a graphical interface for quantum-software components, a parser for syntactic correctness, and an execution environment integrated with IBM Qiskit; it was initially evaluated with Quantum Teleportation and Grover's Search. QADL: Prototype of Quantum Architecture Description Language
[34] An alternative to EXPRESSION-style and template-driven approaches is to formally specify a microprocessor as an operation state machine (OSM). MicroTESK: An Extendable Framework for