A Methodology for Large-Scale Hardware Verification
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.
KeywordsModel Check Theorem Prove High Order Logic Symbolic Model Check Circuit Structure
Unable to display preview. Download preview PDF.
- J. Bergeron, Writing Testbenches: Functional Verification of HDL Models, Kluwer Academic Publishers, 2000.Google Scholar
- T. Kropf, Introduction to Formal Hardware Verification, Springer-Verlag, 1999.Google Scholar
- 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/
- 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
- L. Paulson, ML for the Working Programmer, Cambridge University Press, 1996.Google Scholar
- E. M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999.Google Scholar
- 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
- 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
- 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
- L. Augustson, “A compiler for lazy-ml,” in ACM Symposium on Functional Programming, 1984, pp. 218–227.Google Scholar
- 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
- J. Feldman and C. Retter, Computer Architecture: A Designer’s Text Based on a Generic RISC, McGraw-Hill, 1994.Google Scholar