Technical reports
Formal specification and verification of microprocessor systems
Jeffrey Joyce
September 1988, 24 pages
DOI: 10.48456/tr-147
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} }