NOTE ON RECENT WORK

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:

(i) to provide a reference semantics for use by mechanised formal verification tools;

(ii) to provide a research platform for gaining a deeper scientific understanding of areas whose mathematical specification is challenging.

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.