ARMv8-A Architecture

Concept

ARMv8-A is the Application profile of the ARMv8 architecture, defined in ARM's Architecture Reference Manual and characterized by a large instruction encoding space (1280 instruction encodings described in an ISA specification spanning over 2500 pages). It is a primary target for ARM's ISA-Formal end-to-end verification methodology, which generates executable specifications from the official ARM Architecture Reference Manual and uses them to formally verify ARM processor implementations.

First seen 8/18/2026

Last seen 8/18/2026

Evidence 2 chunks

Wiki v1

WIKI

Overview

ARMv8-A is the Application profile of the ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) published by ARM Ltd. It is the mainstream 64-bit-capable application processor architecture used in mobile, client, and server-class devices.

Specification Size and Complexity

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

1 connections

End-to-End Verification of ARM Processors with ISA-Formal ← mentions 100% 1e

The paper mentions the ARMv8-A architecture specification size and complexity.

LINKED ENTITIES

1 links

End-to-End Verification of ARM Processors with ISA-Formal MENTIONS Extracted graph relationship

CITATIONS

10 sources

10 citations — click to expand

[1] The ARMv8-A/R architecture has 1280 instruction encodings and its instruction set specification is over 2500 pages long. End-to-End Verification of ARM Processors with ISA-Formal

[2] The ARMv8-M architecture has 384 instruction encodings and an ISA specification over 600 pages long. End-to-End Verification of ARM Processors with ISA-Formal

[3] ARM's Architecture Specification Language (ASL) is an indentation-sensitive, imperative, strongly typed, first-order language with type inference, exceptions, enumerations, arrays, records, no pointers, unbounded integers, native support for N-bit bitstrings, and polymorphism in bitstring width. End-to-End Verification of ARM Processors with ISA-Formal

[4] ISA-Formal is now a key part of ARM's formal verification strategy and has been applied to 8 different ARM processors spanning all stages of development up to release. End-to-End Verification of ARM Processors with ISA-Formal

[5] The methodology can detect decoder bugs, forwarding logic errors caused by instruction interactions, and datapath errors. End-to-End Verification of ARM Processors with ISA-Formal

[6] Verification is currently performed using bounded model checking for sequences of n instructions. End-to-End Verification of ARM Processors with ISA-Formal

[7] The executable architecture specification was tested using ARM's internal architecture conformance testsuite with billions of instructions probing instruction corner cases. End-to-End Verification of ARM Processors with ISA-Formal

[8] The ISA-Formal technique is described as the most broadly applicable formal verification technique for verifying processor pipeline control in mainstream commercial use. End-to-End Verification of ARM Processors with ISA-Formal

[9] A 2020 study (Scam-V) validated data-cache side-channel models against a Raspberry Pi 3 board whose processor implements the ARMv8-A architecture, and identified model bugs due to hidden micro-architectural behavior. Validation of Abstract Side-Channel Models for Computer Architectures

[10] A 2022 study explored relaxed virtual memory semantics in Armv8-A, including pKVM hypervisor use cases from Google, axiomatic concurrency models, and integrated tooling with full Armv8-A ISA semantics. Relaxed virtual memory in Armv8-A (extended version)