[Leeds University logo] [Leeds School of Computer Studies logo] [University of Cambridge Computer Laboratory logo] [ARM logo]



The now finished ARM6 project was concerned with micro-architecture verification. Current work builds on top of an ISA model, which evolved from the version verified against the ARM6 micro-architecture, but is now validated by testing. A brief description of recent and current work is below.

The ARM verification project has produced a mathematical model (formalised in higher order logic) of current ARM instruction set architectures as found in phones and forthcoming netbooks (e.g. ISA version ARMv7-A is supported). It is believed that this is one of the most complete formal model of a COTS processor family in existence. We have been testing the HOL model against a processor chip, and this has enabled us to identify and fix errors in earlier versions of the model. We were also able to identify bugs in the GNU Assembler (Gas), which is a commonly used ARM assembler. Bug reports were submitted and these have now been fixed by GNU developers.

A web-based ARM instruction evaluator implemented using the HOL model is available here.

Two purposes of the ARM model are:

An example of (i) is the verification (by Magnus Myreen) of a complete prototype functional language implementation in ARM machine code, including a garbage collector for memory management. Examples of (ii) include models of interrupts, input-output and (in collaboration with Peter Sewell's group at Cambridge) mathematical formalisations of ARM's weak memory model as used in multi-processor systems.

Formal Specification and Verification of ARM6

This page documents results of the University of Cambridge part of EPSRC project GR/N13135.
The research was carried out by Anthony Fox. The Principal Investigator was Mike Gordon.

Professor Mike Gordon
University of Cambridge Computer Laboratory
Room FE19, William Gates Building
JJ Thomson Avenue, Cambridge CB3 0FD
United Kingdon
work phone: +44 1223 334627
work fax: +44 1223 334678
email: mjcg@cl.cam.ac.uk