More Web Proxy on the site http://driver.im/

Article

Formal verification of pentium ® 4 components with symbolic simulation and inductive invariants

Author:

Roope KaivolaAuthors Info & Claims

CAV'05: Proceedings of the 17th international conference on Computer Aided Verification

Pages 170 - 184

https://doi.org/10.1007/11513988_19

Published: 06 July 2005 Publication History

Abstract

We describe a practical methodology for large-scale formal verification of control-intensive industrial circuits. It combines symbolic simulation with human-generated inductive invariants, and a proof tool for verifying implications between constraint lists. The approach has emerged from extensive experiences in the formal verification of key parts of the Intel IA-32 Pentium ® 4 microprocessor designs. We discuss it the context of two case studies: Pentium 4 register renaming mechanism and BUS recycle logic.

References

[1]

S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Form. Methods Syst. Des., 15(1):75-92, 1999.

Digital Library

[2]

S. Bensalem, Y. Lakhnech, and S. Owre. InVeST: A tool for the verification of invariants. In CAV '98, Proceedings, pages 505-510. Springer-Verlag, 1998.

Digital Library

[3]

P. Bjesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessor using satisfiability solvers. In CAV '01, Proceedings, pages 454-464. Springer-Verlag, 2001.

Digital Library

[4]

N. Bjørner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci., 173(1):49-87, 1997.

Digital Library

[5]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Comp., C-35(8):677-691, Aug. 1986.

Digital Library

[6]

R. Burstall. Program proving as hand simulation with a little induction. In Information Processing, pages 308 - 312. North Holland Publishing Company, aug 1974.

[7]

F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of bounded model checking at an industrial setting. In CAV '01, pages 436-453. Springer.

Digital Library

[8]

J. Edmund M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, 1999.

Digital Library

[9]

R. W. Floyd. Assigning meaning to programs. In Proceedings of Symposium in Applied Mathematics, volume 19, pages 19-32. American Mathematical Society, 1967.

[10]

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.

Digital Library

[11]

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.

[12]

R. Jeffords and C. Heitmeyer. Automatic generation of state invariants from requirements specifications. In SIGSOFT '98/FSE-6, Proceedings, pages 56-69. ACM Press, 1998.

Digital Library

[13]

R. B. Jones. Symbolic Simulation Methods for Industrial Formal Verification. Kluwer Academic Publishers, 2002.

[14]

R. Kaivola and K. Kohatsu. Proof engineering in the large: formal verification of Pentium 4 floating-point divider. Int'l J. on Software Tools for Technology Transfer, 4:323-334, 2003.

[15]

Z. Khasidashvili, J. Moondanos, D. Kaiss, and Z. Hanna. An enhanced cut-points algorithm in formal equivalence verification. In HLDVT '01, page 171. IEEE, 2001.

Digital Library

[16]

H. H. Kwak, I.-H. Moon, J. H. Kukula, and T. R. Shiple. Combinational equivalence checking through function transformation. In ICCAD '02, pages 526-533. ACM, 2002.

Digital Library

[17]

Z. Manna and A. Pnueli. Temporal verification of reactive systems: safety. Springer-Verlag New York, Inc., 1995.

Digital Library

[18]

L. Paulson. ML for the Working Programmer. Cambridge University Press, 1996.

Digital Library

[19]

T. Schubert. High level formal verification of next-generation microprocessors. In DAC '03: Proceedings of the 40th conference on Design automation, pages 1-6. ACM Press, 2003.

Digital Library

[20]

C.-J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partiallyordered trajectories. Formal Methods in System Design, 6(2):147-189, Mar. 1995.

Digital Library

[21]

M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a sat-solver. In FMCAD '00, pages 108-125. Springer-Verlag, 2000.

Digital Library

[22]

A. Tiwari, H. Rueß, H. Saïdi, and N. Shankar. A technique for invariant generation. In TACAS 2001, pages 113-127. Springer-Verlag, 2001.

Digital Library

Cited By

Goel SSlobodova ASumners RSwords SBlanchette JHriţcu C(2020)Verifying x86 instruction implementationsProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373811(47-60)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373811
Mitra SBanerjee ADasgupta PRosenstiel WMacii E(2012)Formal methods for ranking counterexamples through assumption miningProceedings of the Conference on Design, Automation and Test in Europe10.5555/2492708.2492937(911-916)Online publication date: 12-Mar-2012
https://dl.acm.org/doi/10.5555/2492708.2492937

Formal verification of pentium ® 4 components with symbolic simulation and inductive invariants
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation

Recommendations

Formal Verification of the Pentium 4 Multiplier
HLDVT '01: Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop (HLDVT'01)

We present the formal verification of the floating-point multiplier in the Intel IA-32 Pentium 4 microprocessor. The verification is based on a combination of theorem-proving and model-checking tasks performed in the Forte hardware verification ...
The Unabridged Pentium 4: IA32 Processor Genealogy
Applications of symbolic simulation to the formal verification of microprocessors

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV'05: Proceedings of the 17th international conference on Computer Aided Verification

July 2005

564 pages

ISBN:3540272313

Editors:
Kousha Etessami
LFCS, School of Informatics, University of Edinburgh
,
Sriram K. Rajamani
LFCS, School of Informatics, Microsoft Research India

Sponsors

Jasper Design Automation: Jasper Design Automation
Weizmann Institute: Weizmann Institute
Microsoft: Microsoft
Intel: Intel
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 06 July 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Goel SSlobodova ASumners RSwords SBlanchette JHriţcu C(2020)Verifying x86 instruction implementationsProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373811(47-60)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373811
Mitra SBanerjee ADasgupta PRosenstiel WMacii E(2012)Formal methods for ranking counterexamples through assumption miningProceedings of the Conference on Design, Automation and Test in Europe10.5555/2492708.2492937(911-916)Online publication date: 12-Mar-2012
https://dl.acm.org/doi/10.5555/2492708.2492937

View Options

View options

Media

Figures

Other

Tables

View Table of Contents