Skip to content
STIMSMITH

ARMv8 instruction set

Concept WIKI v1 · 9/5/2026

The ARMv8 instruction set is a reduced instruction set computer (RISC) architecture developed by ARM, for which formal executable semantics have been published. It is referenced in research on mutation-based test generation for GPU instruction sets and is one of the ISAs covered by an integrated ISA semantics paper covering ARMv8-A, RISC-V, and CHERI-MIPS.

Overview

The ARMv8 instruction set is the instruction set architecture (ISA) introduced by ARM as the first 64-bit extension of the ARM architecture. It has been the subject of formal executable ISA semantics research, and is mentioned in academic work that develops mutation-based test suite generation methods for instruction set simulators.

Formal semantics

A complete executable formal semantics for ARMv8-A, together with RISC-V and CHERI-MIPS, was published by Armstrong, Bauereiss, Campbell, Reid, Gray, Norton, Mundkur, Wassell, French, Pulte, Flur, Stark, Krishnaswami, and Sewell in Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1–31, January 2019 (DOI 10.1145/3290384). The paper is titled "ISA semantics for ARMv8-a, RISC-V, and CHERI-MIPS" and provides the semantic foundation that downstream work uses when mutating or testing the architecture.

A separate effort by Dasgupta, Park, Kasampalis, Adve, and Rosu ("A Complete Formal Semantics of x86-64 User-level Instruction Set Architecture," PLDI 2019) provides a comparable executable semantics for x86-64, cited in the same line of testing research that targets ARMv8.

Testing and mutation research

The ARMv8 ISA is discussed in the registered report "Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking" (Shitrit et al.), which compares its mutation-and-equivalence-checking approach against earlier coverage-guided fuzzing of instruction set simulators. The paper contrasts its method of mutating a stand-alone ISA semantics and using equivalence checking to surface inputs that trigger injected bugs, with prior work that instruments the executable specification of the ISA inside an instruction set simulator to obtain path coverage and then solves path constraints with CVC4.

References in the broader testing literature

Other ISA-testing references cited in the same body of work include:

  • Litmus (Alglave, Maranget, Sarkar, Sewell) for running tests against hardware.
  • NVIDIA's PTX: Parallel Thread Execution ISA, 7th edition (2021).
  • Carrington and Stocks, "A tale of two paradigms: Formal methods and software testing," Z User Workshop, Cambridge 1994, Springer.

LINKED ENTITIES

2 links
Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking MENTIONS
ISA semantics for ARMv8-a, RISC-V, and CHERI-MIPS MENTIONS

CITATIONS

3 sources
3 citations
[1] A formal executable semantics for ARMv8-A was published by Armstrong et al. in POPL 2019, jointly with RISC-V and CHERI-MIPS (DOI 10.1145/3290384). Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking
[2] The Shitrit et al. registered report mutates a stand-alone ISA semantics and uses equivalence checking to surface inputs that trigger injected bugs, in contrast to prior work that instruments the executable specification of the ISA inside an instruction set simulator to obtain path coverage and uses CVC4 to solve path constraints. Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking
[3] A complete formal semantics of x86-64 user-level ISA was published by Dasgupta, Park, Kasampalis, Adve, and Rosu at PLDI 2019 (DOI 10.1145/3314221.3314601), cited alongside ARMv8 ISA-semantics work in mutation-based testing research. Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking