Abstract
Formal verification of arithmetic datapaths has been part of the established methodology for most Intel processor designs over the last years, usually in the role of supplementing more traditional coverage oriented testing activities. For the recent Intel\(^{\tiny\circledR}\) CoreTM i7 design we took a step further and used formal verification as the primary validation vehicle for the core execution cluster, the component responsible for the functional behaviour of all microinstructions. We applied symbolic simulation based formal verification techniques for full datapath, control and state validation for the cluster, and dropped coverage driven testing entirely. The project, involving some twenty person years of verification work, is one of the most ambitious formal verification efforts in the hardware industry to date. Our experiences show that under the right circumstances, full formal verification of a design component is a feasible, industrially viable and competitive validation approach.
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
First the Tick, Now the Tock: Next Generation Intel® Microarchitecture (Nehalem) Intel Corp., http://www.intel.com/technology/architecture-silicon/next-gen/whitepaper.pdf
IA-32 Intel® Architecture Software Developer’s Manual, Vol. 2A and 2B. Intel Corp.
Aagaard, M.D., Jones, R.B., Melhan, T.F., O’Leary, J.W., Seger, C.-J.H.: A methodology for large-scale hardware verification. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 263–282. Springer, Heidelberg (2000)
Beers, R.: Pre-RTL formal verification: an Intel experience. In: DAC 2008: Proc. of the 45th annual conf. on Design automation, pp. 806–811. ACM, New York (2008)
Bentley, B.: Validating a modern microprocessor. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 2–4. Springer, Heidelberg (2005)
Flaisher, A., Gluska, A., Singerman, E.: Case study: Integrating FV and DV in the verification of the Intel CoreTM 2 Duo microprocessor. In: FMCAD, Formal Methods in Computer-Aided Design, pp. 192–195 (2007)
Grundy, J., Melhan, T., O’Leary, J.: A reflective functional language for hardware design and theorem proving. Journal of Functional Programming 16(2), 157–196 (2006)
Hazelhurst, S., Seger, C.-J.H.: Symbolic trajectory evaluation. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol. 1287, pp. 3–78. Springer, Heidelberg (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)
Jones, R.B.: Symbolic Simulation Methods for Industrial Formal Verification. Kluwer Academic Publishers, Dordrecht (2002)
Kaivola, R.: Formal verification of Pentium® 4 components with symbolic simulation and inductive invariants. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 170–184. Springer, Heidelberg (2005)
Kaivola, R., Aagaard, M.D.: Divider circuit verification with model checking and theorem proving. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 338–355. Springer, Heidelberg (2000)
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)
Kaivola, R., Naik, A.: Formal verification of high-level conformance with symbolic simulation. In: HLDVT, High-Level Design Validation and Test, pp. 153–159 (2005)
Kaivola, R., Narasimhan, N.: Formal verification of the Pentium® 4 floating-point multiplier. In: DATE, Design, Automation and Test in Europe, pp. 20–27 (2002)
O’Leary, J.: Using a reflective functional language for hardware verification and theorem proving. In: Third Workshop on Applied Semantics (APPSEM 2005), September 12–15, 2005, pp. 12–15 (2005)
O’Leary, J.W., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel. Technology Journal Q1 (Feburary 1999)
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)
Slobodova, A.: Challenges for formal verification in industrial setting. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 1–22. Springer, Heidelberg (2007)
Slobodova, A.: Formal verification of hardware support for advanced encryption standard. In: FMCAD, Formal Methods in Computer-Aided Design, pp. 61–64 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kaivola, R. et al. (2009). Replacing Testing with Formal Verification in Intel\(^{\scriptsize\circledR}\) CoreTM i7 Processor Execution Engine Validation. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)