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.
Publications and Reports
- A.C.J Fox and N.A. Harman. Algebraic models of correctness for
abstract pipelines. The Journal of Logic and Algebraic Programming,
57(1-2): 71-107, 2003.
- A.C.J Fox. Formal specification and verification of ARM6. In David
Basin and Burkhart Wolff, editors, TPHOLs '03, volume 2758 of LNCS,
pages 25-40. Springer-Verlag, 2003.
- A.C.J. Fox, Formal verification of
the ARM6 micro-architecture. Technical report No. 548, University
of Cambridge Computer Laboratory, November 2002.
- A.C.J. Fox, A HOL specification of
the ARM instruction set architecture. Technical report No. 545,
University of Cambridge Computer Laboratory, June 2001.
- A.C.J. Fox, An algebraic framework
for modelling and verifying microprocessors using HOL. Technical
report No. 512, University of Cambridge Computer Laboratory, April
2001.
- A.C.J. Fox and N.A. Harman,
Algebraic Models of Correctness for Microprocessors. Formal
Aspects of Computing, 12(4): 298-312, 2000.
Unpublished papers
Other outputs
Follow on research plans
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
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.