Technical reports
A HOL specification of the ARM instruction set architecture
Anthony C.J. Fox
June 2001, 45 pages
DOI: 10.48456/tr-545
Abstract
This report gives details of a HOL specification of the ARM instruction set architecture. It is shown that the HOL proof tool provides a suitable environment in which to model the architecture. The specification is used to execute fragments of ARM code generated by an assembler. The specification is based primarily around the third version of the ARM architecture, and the intent is to provide a target semantics for future microprocessor verifications.
Full text
PDF (0.4 MB)
BibTeX record
@TechReport{UCAM-CL-TR-545, author = {Fox, Anthony C.J.}, title = {{A HOL specification of the ARM instruction set architecture}}, year = 2001, month = jun, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-545.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-545}, number = {UCAM-CL-TR-545} }