Computer Laboratory

Technical reports

Formal verification of the ARM6 micro-architecture

Anthony Fox

November 2002, 59 pages

Abstract

This report describes the formal verification of the ARM6 micro-architecture using the HOL theorem prover. The correctness of the microprocessor design compares the micro-architecture with an abstract, target instruction set semantics. Data and temporal abstraction maps are used to formally relate the state spaces and to capture the timing behaviour of the processor. The verification is carried out in HOL and one-step theorems are used to provide the framework for the proof of correctness. This report also describes the formal specification of the ARM6’s three stage pipelined micro-architecture.

Full text

PDF (0.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-548,
  author =	 {Fox, Anthony},
  title = 	 {{Formal verification of the ARM6 micro-architecture}},
  year = 	 2002,
  month = 	 nov,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-548.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-548}
}