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}
}