Technical reports

Formal specification and verification of microprocessor systems

Jeffrey Joyce

September 1988, 24 pages

Abstract

This paper describes the use of formal methods to verify a very simple microprocessor. The hierarchical structure of the microprocessor implementation is formally specified in higher-order logic. The behaviour of the microprocessor is then derived from a switch level model of MOS (Metal Oxide Semiconductor) behaviour using inference rules of higher-order logic with assistance from a mechanical theorem proving system. The complexity of the formal proof is controlled by a multi-level approach based on increasingly abstract views of time and data. While traditional methods such as multi-level simulation may reveal errors or inconsistencies, formal verification can provide greater certainty about the correctness of a design. The main difference with formal verification, and its strength, is that behaviour at one level is formally dervied from lower levels with a precise statement of the conditions under which one level accurately models lower levels.

Full text

PDF (1.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-147,
  author =	 {Joyce, Jeffrey},
  title = 	 {{Formal specification and verification of microprocessor
         	   systems}},
  year = 	 1988,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-147.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-147},
  number = 	 {UCAM-CL-TR-147}
}