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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J. Bergeron, Writing Testbenches: Functional Verification of HDL Models, Kluwer Academic Publishers, 2000.
T. Kropf, Introduction to Formal Hardware Verification, Springer-Verlag, 1999.
Á. 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.
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.
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.
L. Paulson, ML for the Working Programmer, Cambridge University Press, 1996.
E. M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999.
R. E. Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677–691, 1986.
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.
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.
M. J. C. Gordon and T. F. Melham, Eds., Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, 1993.
L. Augustson, “A compiler for lazy-ml,” in ACM Symposium on Functional Programming, 1984, pp. 218–227.
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.
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.
J. Feldman and C. Retter, Computer Architecture: A Designer’s Text Based on a Generic RISC, McGraw-Hill, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aagaard, M.D., Jones, R.B., Melham, T.F., O’Leary, J.W., Seger, CJ.H. (2000). A Methodology for Large-Scale Hardware Verification. In: Hunt, W.A., Johnson, S.D. (eds) Formal Methods in Computer-Aided Design. FMCAD 2000. Lecture Notes in Computer Science, vol 1954. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40922-X_17
Download citation
DOI: https://doi.org/10.1007/3-540-40922-X_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41219-9
Online ISBN: 978-3-540-40922-9
eBook Packages: Springer Book Archive