ARM Architecture Reference Manual

Concept

The ARM Architecture Reference Manual is ARM's official specification document for its processor instruction set architectures. In the v8 era it is published in two main volumes, the v8-A/R manual covering over 2,500 pages and the v8-M manual covering over 600 pages, encoding the full instruction behaviour in the Architecture Specification Language (ASL). ARM has developed mechanical tooling that translates the ARM Architecture Reference Manuals into executable Verilog specifications, a step that is central to its ISA-Formal end-to-end verification framework.

First seen 8/18/2026

Last seen 8/18/2026

Evidence 4 chunks

Wiki v1

WIKI

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.

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

ISA-Formal ← uses 100% 2e

ISA-Formal uses a mechanical translation of ARM's Architecture Reference Manuals to Verilog.

Architecture Specification Language (ASL) ← implements 90% 2e

ASL is the formal language used to write the ARM Architecture Reference Manuals.

LINKED ENTITIES

2 links

ISA-Formal USES Extracted graph relationship

Architecture Specification Language (ASL) IMPLEMENTS Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[1] The ARM v8-A/R architecture reference manual defines 1,280 instruction encodings and is over 2,500 pages long; the v8-M manual defines 384 instruction encodings and is over 600 pages long. End-to-End Verification of ARM Processors with ISA-Formal

[2] ASL grew out of the pseudocode used in earlier versions of the architecture reference manuals and is an indentation-sensitive, imperative, strongly typed, first-order language with type inference, exceptions, enumerations, arrays, records, no pointers, unbounded integers, N-bit bitstrings, and bitstring-polymorphic functions. End-to-End Verification of ARM Processors with ISA-Formal

[3] ARM developed tools that automatically transform ARM's official Architecture Reference Manuals into executable Verilog specifications of the v8-A/R and v8-M architectures. End-to-End Verification of ARM Processors with ISA-Formal

[4] Translating ASL to synthesizable SystemVerilog requires handling finite integer bitwidths, a mostly declarative target language, lack of unbounded loops, lack of exceptions, and lack of bitwidth polymorphism, via value-range analysis, a procedural Verilog subset, loop unrolling with user bounds, explicit exception control flow, and monomorphisation of bitwidth-polymorphic functions. End-to-End Verification of ARM Processors with ISA-Formal

[5] The mechanical translation of the ARM Architecture Reference Manual to Verilog is a key part of making the ISA-Formal approach scale and allows the verification task to be split into thousands of small properties across compute clusters. End-to-End Verification of ARM Processors with ISA-Formal