ARM V6 Instruction Set

The ARM V6 (also referred to in the evidence as ARM Version 6 or ARMv6) instruction set is the instruction set architecture (ISA) at the center of a formal-verification effort targeting the SimSoC full-system simulator. Within SimSoC, the ARM V6 ISS executes embedded applications by fetching, decoding, and executing real binary code; in the first dynamic-translation mode considered by the verification work, each ARM V6 instruction is translated into a C structure that has an associated semantics function, and it is these C semantic functions that are being verified.

Architecture Reference and Formal Model Construction

No vendor-provided formal specification of the ARM architecture was available, so the formal model was derived from the ARM Architecture Reference Manual using a semi-automated process. The main chapters of the manual used to build the model are:

Programmer's Model — introduces the main features of the ARMv6 architecture, including data types, registers, and exceptions.
The ARM Instruction Set — explains the general instruction encoding and groups instructions into categories.
ARM Instructions — lists all 147 ARM instructions in the ARMv6 architecture in alphabetical order.
ARM Addressing Modes — explains the five kinds of addressing modes.

For each of the 147 ARM V6 instructions, the manual provides an encoding table, syntax, a piece of pseudo-code describing its operation, its exceptions, usage, and notes. From these, three kinds of information are extracted: the binary encoding format, the corresponding assembly syntax, and the instruction semantics (an algorithm operating on the processor state). The semantics algorithm may call basic functions defined elsewhere in the manual, for which a Coq library is provided.

The construction of the Coq formal model proceeds in three automated steps:

Extracting information from the PDF of the manual.
Parsing the extracted data into abstract syntax trees (ASTs).
Automated translation from the ASTs into the Coq formal model.

Some information cannot be automatically extracted, notably validity constraints required by the decoder generator, but the most tedious and error-prone part (the pseudo-code semantics) is expressed in a precise and regular style that supports the automated extraction. A dozen documentation problems were uncovered during this process and acknowledged by ARM Ltd., though none were relevant to instruction semantics. The resulting model was also tested on real programs to check that the same results are obtained, providing additional confidence.

ISS Implementation in C

In the SimSoC ISS, each ARM V6 instruction is implemented as a standalone C function. Each such function:

has its own correctness proof,
consists of a return type, argument variables, local variables, and a function body,
modifies the processor state and possibly the memory state (everything is represented in memory on the simulation host machine), and
may call basic functions from a supporting library.

The C code of the ISS avoids constructions with "unspecified behavior" in the C language specification and uses only a very limited set of C library functions (e.g., memset(), memcpy()) that do not invoke the operating system.

Example: the BL (Branch and Link) Instruction

The paper gives the C implementation of the ARM BL instruction as a representative example. The function takes a pointer to a SLv6_Processor structure and parameters L, SLv6_Condition cond, and signed_immed_24. Its body checks whether the condition passes; if L == 1, it stores the address of the next instruction in register 14, and then sets the program counter using a sign-extended and shifted immediate offset added to the value of register 15 (the PC).

Proof Methodology

The verification effort proves, in the Coq proof assistant, that the ISS semantics faithfully implement the formal model of the ARM processor. The key elements are:

CompCert C supplies the formal operational semantics of the C ISS source code and a verified compiler, giving both executable machine code and a Coq formal semantics for the compiled C program.
CompCert Coq library provides formalized properties for words, half-words, bytes, and bitwise operations used to describe the instruction set model.
A global memory model with load and store functions supports read/write operations on the concrete side, while the abstract Coq model directly uses the processor state st.
The proof for each instruction proceeds in a top-down manner: it follows the structure of the C function body, splitting it into statements and then into expressions, comparing the concrete post-state produced by the C semantics with the abstract post-state produced by the formal model after projecting the concrete state.
The proof style is relational, chosen because it is more flexible than functional style when dealing with constraints and fits well with operational semantics.

A dedicated Lemmas Library supports these per-instruction proofs by providing lemmas about memory state changes and the relation between abstract and concrete state modifications during expression evaluation.

SimSoC as the Hosting Simulator

SimSoC is an open-source full system simulator of System-on-Chips that uses the SystemC kernel to simulate hardware parallelism and Transaction Level Modeling (TLM) to model inter-module communications. It includes ISS components to execute embedded applications on various processors, and the ARM V6 ISS is the specific component under formal verification in the cited work. The verification target is the dynamic-translation mode in which a binary decoder translates each instruction into a C structure carrying a semantics function, and it is assumed that a correct decoder exists (the decoder itself is out of scope for the proof).