Advertisement

Embedding hardware verification within a commercial design framework

  • Thomas Kropf
  • Ramayya Kumar
  • Klaus Schneider
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

Abstract

A methodology for verifying complex circuits is presented, based on a strong coupling of design verification with the hierarchical design process. This goal has been achieved by integrating MEPHISTO, a tool for semi-automated hardware verification, into a commercial design framework. MEPHISTO decomposes the verification goal by a set of hardware-specific proof tactics and provides strategies for synthesizing pre-verified regular components. In case of erroneous implementations, MEPHISTO aids the designer in debugging the circuit by generating a counter model, i.e. input stimuli where specification and implementation behave differently.

Keywords

Counter Model Verification Process Hardware Description Language Proof Step Correct Circuit 
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.
    M.C. McFarland, A.C. Parker, and R. Camposano. Tutorial on high-level synthesis. In 25th Design Automation Conference, pages 330–336, 1988.Google Scholar
  2. 2.
    O. Coudert, C. Berthet, and J.C. Madre. Verification of synchronous sequential machines based on symbolic execution. In Workshop on Automatic Verification Methods for Finite State Systems, pages 365–373, June 1989.Google Scholar
  3. 3.
    J.R. Burch, E.M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In 28th Design Automation Conference, pages 403–407, 1991.Google Scholar
  4. 4.
    Th. Kropf and H.-J. Wunderlich. A common approach to test generation and hardware-verification based on temporal logic. In Proceedings of the International Test Conference, pages 57–66, October 1991.Google Scholar
  5. 5.
    W. A. Hunt. FM8501: A Verified Microprocessor. PhD thesis, University of Texas, Austin, 1985.Google Scholar
  6. 6.
    M.J.C. Gordon. A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1988.Google Scholar
  7. 7.
    R. Kumar, K. Schneider, and Th. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment. Journal of Formal System Design, 2(2):165–230, 1993.Google Scholar
  8. 8.
    M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. Milne and P.A. Subrahmanyam, editors, Formal aspects of VLSI Design. North-Holland, 1986.Google Scholar
  9. 9.
    J. Joyce. Formal verification and implementation of a microprocessor. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1988.Google Scholar
  10. 10.
    J. Joyce. More reasons why higher-order logic is a good formalism for specifying and verifying hardware. In International Workshop on Formal Methods in VLSI Design, Miami, 1991.Google Scholar
  11. 11.
    J.D. Morison, N.E. Peeling, and T.L. Thorp. ELLA: A hardware description language. In International Conference on Circuits and Computers, pages 604–607, 1988.Google Scholar
  12. 12.
    R. Boulton, A. Gordon, M. Gordon, J. Herbert, and J. van Tassel. Experiences with Embedding hardware description languages in HOL. In V. Stavridou, T.F. Melham, and R. Boute, editors, Conference on Theorem Provers in Circuit Design, IFIP Transactions A-10, pages 129–156. North-Holland, 1992.Google Scholar
  13. 13.
    CADENCE Design Systems Inc. CADENCE User Manuals, July 1989.Google Scholar
  14. 14.
    E. Mayger and M. P. Fourman. Integration of formal methods with system design. In International Conference on Very Large Scale Integration, pages 59–69, 1991. Edinburgh.Google Scholar
  15. 15.
    F.K. Hanna and N. Daeche. Specification and verification using higher-order logic. In C.J. Koomen and T. Moto-Oka, editors, Conference on Computer Hardware Description Languages and their Applications, pages 418–433. North-Holland, 1985.Google Scholar
  16. 16.
    P. Camurati and P. Prinetto. Formal verification of hardware correctness: Introduction and survey of current research. IEEE-Computer, pages 8–19, 1988.Google Scholar
  17. 17.
    H. Eveking. Verifikation digitaler Systeme. Teubner Verlag, 1991.Google Scholar
  18. 18.
    J.H. Gallier. Logic for Computer Science—Foundations of Automated Theorem Proving. Number 5 in Computer Science and Technology Series. Harper & Row, 1986.Google Scholar
  19. 19.
    K. Schneider, R. Kumar, and Th. Kropf. The FAUST prover. In D. Kapur, editor, 11th Conference on Automated Deduction, number 607 in Lecture Notes in Computer Science, pages 766–770. Springer Verlag, Albany, New York,1992.Google Scholar
  20. 20.
    K. Schneider, R. Kumar, and Th. Kropf. Accelerating tableaux proofs using compact representations. Journal of Formal System Design, 1993.Google Scholar
  21. 21.
    K. Schneider, R. Kumar, and Th. Kropf. Modelling generic hardware structures by abstract datatypes. In M. Gordon L. Claesen, editor, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 419–429. Elsevier Science Publishers, 1992.Google Scholar
  22. 22.
    K. Schneider, R. Kumar, and Th. Kropf. Hardware verification with first-order BDD's. In Conference on Computer Hardware Description Languages, 1993.Google Scholar
  23. 23.
    K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. Monatshefte für Mathematik und Physik, 1, 1931.Google Scholar
  24. 24.
    R. Reetz and Th. Kropf. Ein formales Flußgraphenmodell zur Integration von Hardwarebeschreibungssprachen in die Hardware-Verifikation (in german). In Th. Kropf, R. Kumar, and D. Schmid, editors, Proc. GI/ITG Workshop on Formal Methods for Correct System Design, Technical Report 10/93. University of Karlsruhe, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Thomas Kropf
    • 1
  • Ramayya Kumar
    • 1
  • Klaus Schneider
    • 1
  1. 1.Institut für Rechnerentwurf und FehlertoleranzUniversität KarlsruheKarlsruhe 1Germany

Personalised recommendations