Department of Computer Science and Technology

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},
  number = 	 {UCAM-CL-TR-147}
}