ARM Architecture Specification Language (ASL)

Overview

The ARM Architecture Specification Language (ASL) is the machine-readable formal language used inside ARM's published architecture specification to describe the decoding and execution semantics of every instruction in the ARM ISA. It provides a precise, executable account of how an instruction should behave architecturally, and is consumed by analysis tools that need a specification-level source of truth for ARM behavior.

Role in the ARM Architecture Specification

ASL sits alongside the natural-language ARM Architecture Reference Manual and supplies the formal, machine-parseable counterpart. Its purpose in the specification is to:

• Describe the encoding schema of each instruction, including which bit fields are constant and which are mutable encoding symbols.
• Provide the decoding logic that maps a concrete instruction encoding to an internal representation.
• Provide the execution logic that describes the architectural state changes (registers, memory, condition flags) the instruction performs.
• Express constraints over encoding symbols that gate specific behaviors, conditions, or code paths.

ASL code executes based on the concrete values of the instruction's encoding symbols, which means that for any chosen operand values the specification directly determines the expected outcome of running that instruction on conforming hardware.

Structure of an ASL Instruction Description

For each ARM instruction the ASL fragment typically contains:

• Encoding symbols. The non-constant bit fields declared in the encoding diagram (for example, for STR (immediate) the symbols include Rn, Rt, P, U, W, and Imm8). These are the fields that tools are free to mutate when generating instruction encodings.
• Constants. Bit positions whose values are fixed by the encoding (for STR (immediate), bits [31:20] = 111110000100 and bit [7] = 1 are constant).
• Decoding ASL. Statements that interpret the encoding symbols and produce the operands and addressing parameters (such as index, wback, and the selected registers).
• Execution ASL. Statements that describe the architectural side effects of the instruction, conditioned on the decoded values.
• Constraints. Predicates over encoding symbols that restrict which values are legal or that select between alternative code paths in the execution logic (e.g., a constraint requiring Rt to differ from 15 in a given context).

Programmatic Use of ASL

Because ASL is machine-readable, it can be parsed and analyzed rather than only read by humans. Automated test-generation pipelines typically:

1. Parse an instruction's encoding diagram together with its decoding and execution ASL to obtain the set of symbols, constants, and constraints.
2. Apply a syntax-aware mutation strategy that perturbs each encoding symbol using pre-defined rules (e.g., minimum, maximum, and random values for immediate fields) to produce syntactically valid encodings.
3. Apply a semantics-aware strategy that solves the constraints in the ASL together with their negations, so that values which steer execution down different ASL paths are explicitly covered.

Symbolic Execution over ASL

The Examiner system, presented at ASPLOS '22, is described as the first tool to implement a symbolic execution engine targeted at ASL. This engine:

• Treats the encoding symbols of an instruction as symbolic variables.
• Interprets the decoding and execution ASL under those symbolic values.
• Solves each ASL constraint and its negation with a constraint solver to obtain concrete symbol values that drive the instruction down distinct execution branches.
• Uses the resulting concrete encodings as representative test cases for differential testing.

Applying this approach, Examiner generated 2,774,649 representative instruction streams and performed differential testing across four ARM real devices spanning ARMv5, ARMv6, ARMv7, and ARMv8 against three emulators, locating large numbers of inconsistent instruction streams whose root causes were traced to undefined behavior in the ARM manual and to bugs in the emulators themselves.

Significance

ASL is the linchpin that makes large-scale, specification-driven testing of ARM emulators possible. By providing an executable, machine-parsable description of instruction semantics, it removes the need to manually translate the ARM manual into test oracles and instead lets a tool derive expected behavior directly from the architecture specification.