Architecture Description Language

Concept

An Architecture Description Language (ADL) is a dedicated language for the formal specification of processor and system architectures, used in particular to capture instruction set architectures (ISAs) and to automatically generate design artifacts such as instruction set simulators (ISS), assemblers, compilers, and linkers. Examples named in the cited sources include LISA and Facile; the ADL concept has been extended by broader processor description languages such as the Vienna Architecture Description Language (VADL) and by the Quantum Architecture Description Language (QADL), while a separate domain-specific language called Sail focuses on ISA semantics. A known limitation of ADL-based ISS generation is that processor semantics must still be reimplemented in the ADL, so functional equivalence to the design still has to be demonstrated, which has motivated property-suite-based alternatives and tighter integration with formal verification.

First seen 5/26/2026

Last seen 6/9/2026

Evidence 5 chunks

Wiki v3

WIKI

Overview

An Architecture Description Language (ADL) is a dedicated language for the formal specification of processor and system architectures. In processor and system design flows, ADLs are used to describe instruction set architectures (ISAs) and to support the automatic generation of design artifacts such as instruction set simulators (ISS), assemblers, compilers, and linkers. [C1] [C2] The ADL idea has also been generalized to broader processor description languages, exemplified by the Vienna Architecture Description Language (VADL), and more recently to quantum software systems, as in the Quantum Architecture Description Language (QADL). [C3] [C4]

Role in Instruction Set Simulation

READ FULL ARTICLE →

NEIGHBORHOOD

2 nodes · 1 edges

graph · Architecture Description Language · depth=1

RELATIONSHIPS

4 connections

LISA ← implements 95% 4e

LISA is an ADL tool for automatic generation of simulators and compilers for processors.

Generating an Efficient Instruction Set Simulator from a Complete Property Suite ← mentions 90% 1e

The paper mentions ADL-based approaches and their limitations compared to the proposed method.

Facile ← implements 80% 1e

Facile is an ADL-based tool for automatic generation of processor tools.

Minimally Invasive Generation of RISC-V Instruction Set Simulators from Formal ISA Models ← mentions 90% 1e

The paper mentions ADLs as related prior work

LINKED ENTITIES

7 links

Minimally Invasive Generation of RISC-V Instruction Set Simulators from Formal ISA Models MENTIONS Extracted graph relationship

LISA EXAMPLE_OF LISA is named in both the Kühne paper and the property-suite ISS paper as an example of an ADL for describing ISAs, and is also mentioned as a candidate for integrating formal methods into the processor design tool chain.

Facile EXAMPLE_OF Facile is named in both the Kühne paper and the property-suite ISS paper as an example of an ADL for high-performance processor simulators.

Sail CONTRASTS_WITH Sail is described in the RISC-V paper as a DSL for ISA semantics that contrasts with classical ADLs: it focuses on completeness (instruction decoding, address translation) rather than microarchitectural detail, and generates a new standalone ISS.

FISACO INTEGRATES FISACO is described in the Kühne paper as the tool that implements the automatic generation of a complete property suite from an architecture description and that is proposed to be combined with an existing ADL like LISA.

OneSpin 360 MV USES OneSpin 360 MV is named in the Kühne paper as the driving verification engine for the FISACO property-suite generation approach.

OpenVADL IMPLEMENTS OpenVADL is described in the public VADL context as the open-source implementation of VADL, started because the original VADL implementation has a restricted copyright.

CITATIONS

9 sources

9 citations — click to expand

[1] Instruction set simulators play an important role in pre-silicon software development; a common way to avoid the manual coding of high-performance simulators is to use ADLs that compile into an ISS, with Facile and LISA named as examples. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[2] ADL-based ISS generation still requires the reimplementation of the processor semantics in the ADL, so the functional equivalence of the ISS and the design still remains to be demonstrated. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[3] A complete formal property suite from processor verification can be reused to automatically generate an ISS that, by construction, complies with the ISA used for verification and with the design; this methodology is described as offering the highest quality of verification. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[4] VADL is a processor description language that enables concise formal specification of processor architectures and automatic generation of assemblers, compilers, linkers, functional and cycle-accurate ISS, synthesizable HDL specifications, test cases, and documentation; it separates ISA from microarchitecture and is the basis of the open-source OpenVADL implementation. The Vienna Architecture Description Language

[5] QADL extends the ADL concept to quantum software, providing a graphical interface for designing QSW components, a parser for syntactical correctness, and an execution environment integrated with IBM Qiskit, with initial evaluation using Quantum Teleportation and Grover's Search. QADL: Prototype of Quantum Architecture Description Language

[6] Compared to formal ISA models, classical ADLs focus more on microarchitectural details such as pipelining or caching, which makes integration with existing simulators and vendor-supplied components challenging; these languages are therefore primarily used to generate new simulators rather than to integrate with existing ones. Minimally Invasive Generation of RISC-V Instruction Set Simulators from Formal ISA Models

[7] Sail is a DSL for ISA semantics; from a Sail model, formal descriptions in C, OCaml, Coq, Isabelle, and HOL4 can be generated; Sail has been used to model the RISC-V, ARM-v8, and MIPS ISAs; it focuses on completeness including address-translation algorithms and instruction decoding, which makes integration into an existing RISC-V simulator difficult, so Sail generates a new standalone ISA simulator. Minimally Invasive Generation of RISC-V Instruction Set Simulators from Formal ISA Models

[8] The Kühne paper proposes automatic generation of a complete property suite from an architecture description via mapping functions that capture how abstract concepts are mapped to the RTL implementation (pipeline stages, stall and cancel signals); the approach is implemented in FISACO, uses the OneSpin 360 MV verification engine, and was demonstrated on an industrial automotive control processor with reported doubled verification productivity. Automated Formal Verification of Processors

[9] A complementary extension of the property-suite approach would be the use of an existing ADL such as LISA to integrate formal methods into the processor-design tool chain; generating both a complete property suite and an efficient ISS from a common architecture description would ensure that the generated ISS complies with the verified RTL code. Automated Formal Verification of Processors