Formal specification and verification of microprocessor systems
The work
| Authors | Jeffrey J. Joyce |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1988 |
| Citekey | joyce1988formal |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-147 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| DOI | 10.48456/tr-147 |
|---|---|
| report_number | UCAM-CL-TR-147 |
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-147.html |
|---|
Related
| Distinct from | basin1989verification |
|---|---|
| Distinct from | bryant1981switchlevel |
| Distinct from | camilleri1988simulation |
| Distinct from | cohn1988correctness |
| Distinct from | gordon1985hol |
| Distinct from | gordon1987hol |
| Distinct from | jacobi2002formal |
| Distinct from | joyce1986proving |
| Distinct from | joyce1987hardware |
| Distinct from | joyce1990multilevel |
| Distinct from | melham1990formalizing |
| Distinct from | mermet1997survey |
| Distinct from | oulkaid2025modeles |
| Distinct from | traub1986formal |
From bibtex.
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 derived from lower levels with a precise statement of the conditions under which one level accurately models lower levels.
A copy is held
pdf, 1.1 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-15 21:18 UTC |
| Approved by | a person 2026-09-23 14:09 UTC |
Filed under
Cite it as
@techreport{joyce1988formal,
title = {Formal specification and verification of microprocessor systems},
author = {Jeffrey J. Joyce},
year = {1988},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
issn = {1476-2986},
doi = {10.48456/tr-147},
}
This record lives at https://refs.drheap.org/joyce1988formal/ and will keep doing so.