Technical reports
Formal verification of the ARM6 micro-architecture
Anthony Fox
November 2002, 59 pages
DOI: 10.48456/tr-548
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-548.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-548}, number = {UCAM-CL-TR-548} }