ARM Architecture Reference Manual

Overview

The ARM Architecture Reference Manual (ARM ARM) is ARM Limited's official architectural specification document for its processor instruction set architectures. In the current v8 generation it is published as two principal volumes covering the application/profile (v8-A/R) and microcontroller (v8-M) variants of the architecture. The reference manual defines the programmer-visible behaviour of every instruction and is the source of truth against which ARM processors are verified.

Scale and structure of the v8 manuals

The ARM v8-A/R architecture reference manual defines 1,280 instruction encodings and is over 2,500 pages long. The ARM v8-M architecture reference manual defines 384 instruction encodings and is over 600 pages long. The instruction-set-architecture portion of the v7-M specification alone is over 600 pages long, almost half the length of the entire specification. The manuals encode many subtleties: many instruction encodings explicitly disallow using certain registers as sources or destinations, many instructions are conditional, and the manuals are updated regularly with new architectural changes.

Architecture Specification Language (ASL)

The core executable notation inside the ARM Architecture Reference Manual is ARM's Architecture Specification Language (ASL). ASL grew out of the pseudocode used in earlier versions of the architecture reference manuals. At a high level, ASL is:

• indentation-sensitive,
• imperative,
• strongly typed with type inference,
• first-order,
• supporting exceptions, enumerations, arrays, records, but not pointers,
• using unbounded integers with direct support for N-bit bitstrings, and
• allowing functions to be polymorphic in the width of a bitstring.

For example, a memory read returns a value of type bits(8*size) where size is constrained to be 1, 2, 4 or 8.

From ARM ARM to executable Verilog for verification

Manually writing and maintaining a Verilog specification equivalent to the ARM ARM is unattractive given the size, complexity and rate of change of the manuals. Over a five-year period ARM developed tools that automatically transform ARM's official Architecture Reference Manuals into executable specifications of the v8-A/R and v8-M architectures. Before using these specifications for verification they were tested thoroughly, in a manner analogous to Fox and Myreen's testing of an ARM ISA specification, but using ARM's internal architecture conformance testsuite to run billions of instructions probing each instruction's corner cases.

Translating ASL to the synthesizable subset of SystemVerilog accepted by commercial model checkers involves overcoming several limitations of synthesizable Verilog:

1. Verilog integers are finite and bitwidth is part of the type.
2. Combinational Verilog is normally declarative, with no assignments, limited control flow, and few function calls.
3. Synthesizable Verilog does not support unbounded for-loops or while-loops.
4. Synthesizable Verilog does not support exceptions.
5. The width of bitstrings in Verilog must always be a manifest constant, and functions cannot be polymorphic over bitwidth.

ARM addresses these challenges as follows:

1. A global flow-insensitive value-range analysis computes the required width of most integer variables; integers with unknown range are assigned a large but safe bound.
2. Translation uses Verilog's rarely used procedural subset, which covers most of ASL.
3. User-supplied bounds on loops allow all loops to be unrolled.
4. A whole-program transformation adds flags and control flow to make exception-related and return-related control flow explicit.
5. Almost all bitwidth polymorphism is caused by instructions that operate on multiple data widths (such as 8, 16, 32 or 64-bit loads). The translator automatically specialises such instruction encodings into one instruction per data width, then uses constant propagation and a monomorphisation pass that resolves calls whose bitwidth is a manifest constant. Any remaining polymorphism is handled by ad-hoc transforms in the Verilog backend.

Role in ISA-Formal verification

The mechanical translation of the ARM Architecture Reference Manual into Verilog is the key scaling enabler for ISA-Formal, ARM's end-to-end framework for detecting bugs in datapath, pipeline control, and forwarding/stall logic. ISA-Formal partitions the specification on function-call boundaries into parts such as "Instruction Set Architecture (ISA)," "Floating Point," "Exception," and "Address Translation," and only generates Verilog for the ISA part; functions on the interfaces to other partitions are written by hand. The verification task is split into thousands of small properties so that large compute clusters can be used effectively.

Significance

The ARM Architecture Reference Manual is the foundation for ARM's formal verification strategy: it is the single source from which both the architecture specification and the verification IP are mechanically derived, allowing ARM to apply a uniform ISA-Formal approach across processors ranging from simple 3-stage microcontrollers to sophisticated 64-bit out-of-order designs.