Computer Laboratory

Technical reports

An algebraic framework for modelling and verifying microprocessors using HOL

Anthony Fox

March 2001, 24 pages

Abstract

This report describes an algebraic approach to the specification and verification of microprocessor designs. Key results are expressed and verified using the HOL proof tool. Particular attention is paid to the models of time and temporal abstraction, culminating in a number of one-step theorems. This work is then explained with a small but complete case study, which verifies the correctness of a datapath with microprogram control.

Full text

PDF (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-512,
  author =	 {Fox, Anthony},
  title = 	 {{An algebraic framework for modelling and verifying
         	   microprocessors using HOL}},
  year = 	 2001,
  month = 	 mar,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-512.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-512}
}