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.
Chapter PDF
Similar content being viewed by others
References
Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Form. Methods Syst. Des. 15(1), 75–92 (1999)
Bensalem, S., Lakhnech, Y., Owre, S.: InVeST: A tool for the verification of invariants. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 505–510. Springer, Heidelberg (1998)
Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 454–464. Springer, Heidelberg (2001)
Bjørner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci. 173(1), 49–87 (1997)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Comp. C-35(8), 677–691 (1986)
Burstall, R.: Program proving as hand simulation with a little induction. In: Information Processing, August 1974, pp. 308–312. North Holland Publishing Company, Amsterdam (1974)
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001)
Edmund, J., Clarke, M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)
Floyd, R.W.: Assigning meaning to programs. In: Proceedings of Symposium in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)
Hazelhurst, S., Seger, C.-J.H.: Symbolic trajectory evaluation. In: Kropf, T. (ed.) Formal Hardware Verification, ch. 1, pp. 3–78. Springer, New York (1997)
Hinton, G., Sager, D., Upton, M., Boggs, D., Carmean, D., Kyker, A., Roussel, P.: The microarchitecture of the Pentium 4 processor. Intel. Technology Journal Q1 (February 2001)
Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In: SIGSOFT 1998/FSE-6, Proceedings, pp. 56–69. ACM Press, New York (1998)
Jones, R.B.: Symbolic Simulation Methods for Industrial Formal Verification. Kluwer Academic Publishers, Dordrecht (2002)
Kaivola, R., Kohatsu, K.: 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)
Khasidashvili, Z., Moondanos, J., Kaiss, D., Hanna, Z.: An enhanced cut-points algorithm in formal equivalence verification. In: HLDVT 2001, p. 171. IEEE, Los Alamitos (2001)
Kwak, H.H., Moon, I.-H., Kukula, J.H., Shiple, T.R.: Combinational equivalence checking through function transformation. In: ICCAD 2002, pp. 526–533. ACM Press, New York (2002)
Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, New York (1995)
Paulson, L.: ML for the Working Programmer. Cambridge University Press, Cambridge (1996)
Schubert, T.: High level formal verification of next-generation microprocessors. In: DAC 2003: Proceedings of the 40th conference on Design automation, pp. 1–6. ACM Press, New York (2003)
Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6(2), 147–189 (1995)
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a sat-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Tiwari, A., Rueß, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kaivola, R. (2005). Formal Verification of Pentium ® 4 Components with Symbolic Simulation and Inductive Invariants. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_19
Download citation
DOI: https://doi.org/10.1007/11513988_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
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.
