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
In modern processor and system design flows, instruction set simulators play an important role in pre-silicon software development, enabling the simulation of software before the target system is manufactured or even the design is finished. With increasing system complexity, simulation performance in terms of executed instructions per second has become an important factor, so ISS are typically based on the ISA and implemented in high-level languages such as C++. For such an ISS, the ISA has to be reimplemented manually. [C1]
A common way to avoid the manual coding of high-performance simulators is the use of architecture description languages (ADL), which can then be compiled into an ISS. Examples of such ADLs named in the cited sources are Facile and LISA. [C1] [C2]
Microarchitectural Focus vs. Formal ISA Models
The evidence contrasts classical ADLs with formal ISA modeling approaches. Compared to formal ISA models, classical ADLs focus more on microarchitectural details such as pipelining or caching. For this reason, it is challenging to integrate them with existing simulators and vendor-supplied components. Therefore, these languages are primarily used to generate new simulators rather than to aim for integration with existing ones. [C5]
Sail: A DSL for ISA Semantics
Sail is described in the cited RISC-V generation work as a domain-specific language (DSL) developed to describe ISA semantics. From a Sail model of an ISA, formal descriptions in different programming and theorem-proving languages can be generated, including C, OCaml, Coq, Isabelle, and HOL4. Sail has been used in prior work to model the RISC-V, ARM-v8, and MIPS ISAs, among others. [C6]
The source notes that this versatility comes at a price: the generated models are not as concise or convenient to work with as native ones. Moreover, Sail focuses on completeness and therefore goes beyond the description of instruction semantics, also including formalization of additional ISA details such as address-translation algorithms and instruction decoding. This contributes to the complexity of Sail and makes it difficult to integrate it into an existing RISC-V simulator, so Sail instead generates a new standalone ISA simulator. [C6]
Broader Generated Artifacts: VADL
The Vienna Architecture Description Language (VADL) is a processor description language (PDL) that enables the concise formal specification of processor architectures. From a single VADL processor specification, the VADL system can automatically generate:
- assemblers
- compilers
- linkers
- functional instruction set simulators
- cycle-accurate instruction set simulators
- synthesizable specifications in a hardware description language
- test cases
- documentation [C3]
A distinctive feature of VADL is the separation of the ISA specification from the microarchitecture (MiA) specification. This segregation is intended to allow different ISAs to be combined with different MiAs, and the VADL MiA specification operates at a higher level of abstraction than in some existing processor description languages. [C3]
Because the original VADL implementation has a restricted copyright, an open-source implementation called OpenVADL was started. [C3]
Extension to Quantum Software: QADL
The Quantum Architecture Description Language (QADL) extends the ADL idea to quantum software (QSW). QADL provides:
- a graphical interface to specify and design QSW components
- a parser for syntactical correctness
- an execution environment by integrating QADL with IBM Qiskit
The initial evaluation is based on usability assessments by a team of quantum physicists and software engineers using algorithms such as Quantum Teleportation and Grover's Search. [C4]
Limitation: Reimplementation of Processor Semantics
Although ADL-based approaches can generate an ISS from an architectural description, the cited work notes a limitation: the processor semantics still have to be reimplemented in the ADL. Because of that reimplementation step, the functional equivalence between the generated ISS and the processor design still remains to be demonstrated. [C1]
Contrast with Property-Suite-Based Generation
The cited paper contrasts ADL-based ISS generation with an approach that reuses a complete formal property suite from processor verification to generate an ISS. In that alternative approach, the property suite is treated as a functionally equivalent model after formal verification, and the generated simulator is described as compliant with the ISA used for verification and, by construction, with the design. The source notes that this methodology generally offers the highest quality of verification. [C1] [C2]
Integration with Formal Verification
The Kühne FMCAD paper proposes generating a complete property suite from an architecture description of the processor. The user defines mapping functions that capture how abstract concepts are mapped to the register transfer level (RTL) implementation, referring to pipeline stages, stall and cancel signals, and similar objects familiar to design and verification engineers. The automatic generation of properties is implemented in the tool FISACO, demonstrated on an industrial control processor from the automotive domain, and the verification engine used is the OneSpin 360 MV tool. The estimated verification productivity was reported to have doubled. [C7]
The same source states that a complementary extension would be the use of an existing ADL such as LISA, facilitating the integration of formal methods into the tool chain for processor design. The paper argues that 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. [C7] [C8]
Design-Flow Implications
The cited sources state that an ISS can be generated early once the ISA has been formally captured, and that later verification ensures correspondence between the generated ISS and the design. They also state that using a revised formal property suite can adapt the ISS with little additional effort when design or specification changes occur late in the flow. [C1] [C2]