Abstract
We examine the challenges presented by large-scale formal verification of industrial-size circuits, based on our experiences in verifying the class of all micro-operations executing on the floating-point division and square root unit of the Intel IA-32 Pentium®4 microprocessor. The verification methodology is based on combining human-guided mechanised theorem-proving with low-level steps verified by fully automated model-checking. A key observation in the work is the need to explicitly address the issues of proof design and proof engineering, i.e. the process of creating proofs and the craft of structuring and formulating them, as concerns on their own right.
Chapter PDF
Similar content being viewed by others
Keywords
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
M. D. Aagaard, R. B. Jones, T. F. Melhan, J. W. O’Leary, and C.-J. H. Seger. A methodology for large-scale hardware verification. In FMCAD, volume 1954 of LNCS, pages 263–282. Springer, 2000.
M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Lifted-fl: A pragmatic implementation of combined model checking and theorem proving. In TPHOLs. Springer, 1999.
M. D. Aagaard, T. F. Melham, and J. W. O’Leary. Xs are for trajectory evaluation, Booleans are for theorem proving. In CHARME. Springer, 1999.
C.-T. Chou. The mathematical foundation of symbolic trajectory evaluation. In CAV. Springer, 1999.
P. Curzon. The importance of proof maintenance and reengineering. In J. Alves-Foss, editor, HOL-95: B-track Proceedings, pages 17–31, Sept. 1995.
M. D. Ercegovac and T. Lang. Division and Square Root, Digit-Recurrence Algorithms and Implementations. Kluwer Academic, 1994.
D. Gries. The Science of Programming. Springer-Verlag, 1981.
I. Hayes. Applying formal verification to software development in industry. In I. Hayes, editor, Specification case studies, pages 285–310. Prentice-Hall, 1987.
S. Hazelhurst and C.-J. H. Seger. Symbolic trajectory evaluation. In T. Kropf, editor, Formal Hardware Verification, chapter 1, pages 3–78. Springer Verlag; New York, 1997.
Hinton, G., Sager, D., Upton, M., Boggs, D., Carmean, D, Kyker, A. and Roussel, P. The microarchitecture of the Pentium 4 processor. Intel Technology Journal, Q1, Feb. 2001.
IEEE. IEEE Standard for binary floating-point arithmetic. ANSI/IEEE Std 754-1985, 1985.
M. Jones and G. Gopalakrishnan. A PCI formalization and refinement. In TPHOLs 2000, Supplemental Proceedings, OGI Technical Report CSE 00-090, pages 115–124, 2000.
R. Kaivola and M. D. Aagaard. Divider circuit verification with model checking and theorem proving. In TPHOLs, volume 1869 of LNCS, pages 338–355. Springer, 2000.
R. Kaivola and N. Narasimhan. Multiplier verification with symbolic simulation and theorem proving. Submitted for publication, 2001.
A. Mokkedem and T. Leonard. Formal verification of the Alpha 21364 network protocol. In TPHOLs, volume 1869 of LNCS, pages 443–461. Springer, 2000.
L. Paulson. ML for the Working Programmer., Cambridge University Press, 1996.
D. M. Russinoff. A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. London Mathematical Society Journal of Computational Mathematics, 1:148–200, 1998.
C.-J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6(2): 147–189, Mar. 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kaivola, R., Kohatsu, K. (2001). Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_18
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive