Affordable Access

DDD-FM9001: Derivation of a verified microprocessor

IFIP Lecture Notes in Computer Science (LNCS)
Publication Date
  • Design
  • Engineering


The is a 32-bit general purpose microprocessor directly from Hunts mechanically verified specification. The exercise was part of a project to construct an implementation of the FM9001 by applying the to the Nqthm FM9001 specification. The main thesis of this work maintains that and 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 Hunts . 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.Full Text at Springer, may require registration or fee

There are no comments yet on this publication. Be the first to share your thoughts.