Technical reports
An algebraic framework for modelling and verifying microprocessors using HOL
Anthony Fox
March 2001, 24 pages
DOI: 10.48456/tr-512
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-512.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-512}, number = {UCAM-CL-TR-512} }