DDD-FM9001: Derivation of a verified microprocessor
The work
| Authors | Bhaskar Bose; Steven D. Johnson |
|---|---|
| Editors | |
| Type | incollection |
| Year | 1993 |
| Citekey | bose1993dddfm9001 |
Where it appeared
| Published in | Correct Hardware Design and Verification Methods |
|---|---|
| Publisher | Springer Berlin Heidelberg |
| Series | Lecture Notes in Computer Science |
| Pages | 191--202 |
Identifiers
| DOI | 10.1007/bfb0021724 |
|---|---|
| ISSN | 0302-9743 |
| ISBN | 978-3-540-56778-3 |
Access
| Landing page | https://doi.org/10.1007/bfb0021724 |
|---|
From crossref.
Abstract
The DDD-FM9001 is a 32-bit general purpose microprocessor formally derived directly from Hunt's mechanically verified Nqthm FM9001 microprocessor specification. The exercise was part of a project to construct an implementation of the FM9001 by applying the DDD design derivation system to the Nqthm FM9001 specification. The main thesis of this work maintains that derivation and verification represent interdependent facets of design and must be integrated if formal methods are to support the natural analytical and generative reasoning that takes place in engineering practice. In this paper we describe the continuation of previous work in which the DDD system was applied to Hunt's FM8501 specification. This paper describes the derivation of the DDD-FM9001 and compares the derived architecture and hardware realization with that of the FM9001 in an effort to better understand the interplay between derivation and verification.
A copy is held
pdf, 598.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-22 21:12 UTC |
| Approved by | a person 2026-10-22 22:41 UTC |
Filed under
Cite it as
@incollection{bose1993dddfm9001,
title = {DDD-FM9001: Derivation of a verified microprocessor},
author = {Bhaskar Bose and Steven D. Johnson},
year = {1993},
booktitle = {Correct Hardware Design and Verification Methods},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
pages = {191--202},
isbn = {978-3-540-56778-3},
issn = {0302-9743},
doi = {10.1007/bfb0021724},
}
This record lives at https://refs.drheap.org/bose1993dddfm9001/ and will keep doing so.