ARM Architecture Specification Language (ASL)

Concept

The ARM Architecture Specification Language (ASL) is ARM's machine-readable formal notation that expresses the encoding, decoding, and execution semantics of ARM instructions. Because it is executable and parsable, it enables automated tools (notably the Examiner symbolic-execution engine) to derive ground-truth instruction behavior and to drive differential testing between ARM emulators and real devices.

First seen 6/7/2026

Last seen 6/7/2026

Evidence 3 chunks

Wiki v1

WIKI

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:

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

2 connections

Examiner ← uses 100% 2e

Examiner parses and symbolically executes ARM ASL code to derive test cases.

Symbolic Execution ← implements 100% 2e

The paper implements the first symbolic execution engine for ARM ASL to generate test cases.

LINKED ENTITIES

2 links

Examiner USES Extracted graph relationship

Symbolic Execution IMPLEMENTS Extracted graph relationship

CITATIONS

7 sources

7 citations — click to expand

[1] ASL is the machine-readable specification language in which ARM expresses the decoding and execution semantics of its instructions. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[2] Each ARM instruction's ASL description includes an encoding schema with constant fields and mutable encoding symbols (e.g., STR immediate uses constants 111110000100 in [31:20] and 1 in [7:7], and symbols Rn, Rt, P, U, W, Imm8). Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[3] ASL code executes based on the concrete values of the instruction's encoding symbols. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[4] ASL contains constraints over encoding symbols (e.g., Rt == 15) that gate specific behaviors or execution paths, which must be satisfied for an instruction to be legal in a given context. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[5] Examiner is the first tool to implement a symbolic execution engine for ASL, using it to extract symbols, constants, and constraints and to solve those constraints and their negations to cover different execution paths. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[6] Using its ASL symbolic execution engine, Examiner generated 2,774,649 representative instruction streams and conducted differential testing against ARM real devices across ARMv5, ARMv6, ARMv7, and ARMv8. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[7] The arXiv version of the work also reports generating 2,774,649 instruction streams and locating 155,642 inconsistent streams (covering 30% of instruction encodings and 47.8% of instructions) when testing against QEMU, with undefined ARM manual behavior and QEMU bugs identified as major causes. Automatically Locating ARM Instructions Deviation between Real Devices and CPU Emulators