Advertisement

DDD-FM9001: Derivation of a verified microprocessor

An exercise in integrating verification with formal derivation
  • Bhaskar Bose
  • Steven D. Johnson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

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.

Keywords

Field Programmable Gate Array Register File Digital Design Logical Organization Boolean Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Actel Corporation, Sunnyvale, CA. ACT Family Field Programmable Gate Array Databook, 1991.Google Scholar
  2. 2.
    S. B. Akers. Binary Decision Diagrams. In IEEE Transactions on Computers, volume C-27, pages 509–516, June 1978.Google Scholar
  3. 3.
    Bhaskar Bose, Steven D. Johnson, and Shyamsundar Pullela. Integrating boolean verification with formal derivation. In Proceedings of the IFIP Conference on Hardware Description Languages and their applications (CHDL), 1993.Google Scholar
  4. 4.
    C. David Boyer and Steven D. Johnson. Using the digital design derivation system: Case study of a VLSI garbage collector. In J. Darringer and F. Ramming, editors, Proceedings of the IFIP WG 10.2 Ninth International Symposium on Computer Hardware Description Languages (CHDL), Amsterdam, 1989. Elsevier.Google Scholar
  5. 5.
    Robert S. Boyer and J. Struther Moore. A Computational Logic Handbook. Academic Press, New York, 1988.Google Scholar
  6. 6.
    R. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers, volume C-35, pages 677–691, August 1986.Google Scholar
  7. 7.
    R. Bryant. COSMOS: A Compiled Simulator for MOS Circuits. In Proceedings of the 24th Design Automation Conference, 1987.Google Scholar
  8. 8.
    John A. Darringer. The application of program verification techniques to hardware verification. In Proceedings of the 16th Design Automation Conference, June 1979.Google Scholar
  9. 9.
    Jr. Hunt, Warren A. FM8501: A Verified Microprocessor. PhD thesis, The University of Texas at Austin, 1985. Also published as Technical Report 47 (December, 1985).Google Scholar
  10. 10.
    Warren A. Hunt. A formal HDL and its use in the FM9001 verification. In C.A.R. Hoare and M.J.C. Gordon, editors, Mechanized Reasoning in Hardware Design. Prentice-Hall, 1992.Google Scholar
  11. 11.
    S. D. Johnson and Bhaskar Bose. A system for mechanized digital design derivation. In Subramanyam, editor, Proceedings of ACM International Workshop on Formal Methods in VLSI Design. January 1991.Google Scholar
  12. 12.
    Steven D. Johnson. Synthesis of Digital Designs from Recursion Equations. The MIT Press, Cambridge, 1984.Google Scholar
  13. 13.
    Steven D. Johnson. Manipulating logical organization with system factorizations. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, pages 260–281. Proceedings of Mathematical Sciences Institute Workshop, Cornell University, Springer-Verlag, July 1989.Google Scholar
  14. 14.
    Steven D. Johnson, Bhaskar Bose, and C. David Boyer. A tactical framework for digital design. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 349–383. Kluwer Academic Publishers, Boston, 1988.Google Scholar
  15. 15.
    Steven D. Johnson, Robert M. Wehrmeister, and Bhaskar Bose. On the interplay of synthesis and verification: Experiments with the FM8501 processor description. In Luc Claesen, editor, Applied Formal Methods For Correct VLSI Design, pages 385–404, Amsterdam, Netherlands, 1989. IMEC, Elsevier.Google Scholar
  16. 16.
    Michael C. McFarland, Alice C. Parker, and Raul Camposano. Tutorial on high-level synthesis. In 25 th ACM/IEEE Design Automation Conference, pages 330–336, 1988.Google Scholar
  17. 17.
    Kamlesh Rath and Steven D. Johnson. Toward a basis for protocol specification and process decomposition. In Proceedings of the IFIP Conference on Hardware Description Languages and their applications (CHDL), 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Bhaskar Bose
    • 1
  • Steven D. Johnson
    • 1
  1. 1.Indiana UniversityBloomingtonUSA

Personalised recommendations