Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Formal Specification and Verification of ARM6
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.
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.
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.
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.