Advertisement

A Methodology for Large-Scale Hardware Verification

  • Mark D. Aagaard
  • Robert B. Jones
  • Thomas F. Melham
  • John W. O’Leary
  • Carl-Johan H. Seger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

We present a formal verification methodology for datapathdominated hardware. This provides a systematic but flexible framework within which to organize the activities undertaken in large-scale verification efforts and to structure the associated code and proof-script artifacts. The methodology deploys a combination of model checking and lightweight theorem proving in higher-order logic, tightly integrated within a general-purpose functional programming language that allows the framework to be easily customized and also serves as a specification language. We illustrate the methodology-which has has proved highly effective in large-scale industrial trials-with the verification of an IEEE- compliant, extended precision floating-point adder.

Keywords

Model Check Theorem Prove High Order Logic Symbolic Model Check Circuit Structure 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    J. Bergeron, Writing Testbenches: Functional Verification of HDL Models, Kluwer Academic Publishers, 2000.Google Scholar
  2. [2]
    T. Kropf, Introduction to Formal Hardware Verification, Springer-Verlag, 1999.Google Scholar
  3. [3]
    Á. Th. Eirkksson, “The formal design of 1M-gate ASICs,” in Formal Methods in Computer-Aided Design, G. Gopalakrishnan and P. Windley, Eds. 1998, vol. 1522 of Lecture Notes in Computer Science, pp. 49–63, Springer Verlag.CrossRefGoogle Scholar
  4. [4]
    J. O'Leary, X. Zhao, R. Gerth, and C.-J. H. Seger, “Formally verifying IEEE compliance of floating-point hardware,” Intel Technical Journal, First quarter, 1999, Available at developer.http://intel.com/technology/itj/
  5. [5]
    Y. Xu, E. Cerny, A. Silburt, A. Coady, Y. Liu, and P. Pownall, “Practical appli-cation of formal verification techniques on a frame mux/demux chip from Nortel Semiconductors,” in Correct Hardware Design and VerificationMethods, Laurence Pierre and Thomas Kropf, Eds. 1999, vol. 1703 of Lecture Notes in Computer Science, pp. 110–124, Springer-Verlag.Google Scholar
  6. [6]
    C.-J. H. Seger and R. E. Bryant, “Formal verification by symbolic evaluation of partially-ordered trajectories,” Formal Methods in System Design, vol. 6, no. 2, pp. 147–189, March 1995.CrossRefGoogle Scholar
  7. [7]
    L. Paulson, ML for the Working Programmer, Cambridge University Press, 1996.Google Scholar
  8. [8]
    E. M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999.Google Scholar
  9. [9]
    R. E. Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677–691, 1986.CrossRefGoogle Scholar
  10. [10]
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, “Formal verification using parametric representations of boolean constraints,” in ACM/IEEE Design Automation Conference, 1999.Google Scholar
  11. [11]
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, “Combining theorem proving and trajectory evaluation in an industrial environment,” in ACM/IEEE Design Automation Conference, 1998, pp. 538–541.Google Scholar
  12. [12]
    M. J. C. Gordon and T. F. Melham, Eds., Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, 1993.Google Scholar
  13. [13]
    L. Augustson, “A compiler for lazy-ml,” in ACM Symposium on Functional Programming, 1984, pp. 218–227.Google Scholar
  14. [14]
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, “Lifted-fl: A pragmatic implementation of combined model checking and theorem proving,” in Theorem Proving in Higher Order Logics, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, Eds. 1999, vol. 1690 of Lecture Notes in Computer Science, pp. 323–340, Springer-Verlag.CrossRefGoogle Scholar
  15. [15]
    D. Syme, “Three tactic theorem proving,” in Theorem Proving in Higher Order Logics, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin,and L. Théry, Eds. 1999, vol. 1690 of Lecture Notes in Computer Science, pp. 203–220, Springer-Verlag.CrossRefGoogle Scholar
  16. [16]
    J. Feldman and C. Retter, Computer Architecture: A Designer’s Text Based on a Generic RISC, McGraw-Hill, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Mark D. Aagaard
    • 1
  • Robert B. Jones
    • 2
  • Thomas F. Melham
    • 3
  • John W. O’Leary
    • 2
  • Carl-Johan H. Seger
    • 2
  1. 1.Performance Microprocessor DivisionIntel CorporationHillsboroUSA
  2. 2.Strategic CAD LabsIntel CorporationHillsboroUSA
  3. 3.Department of Computing ScienceUniversity of GlasgowGlasgowScotland

Personalised recommendations