Replacing Testing with Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation

Abstract

Formal verification of arithmetic data-paths has been part of the established methodology for most Intel processor designs over the last years. Usually formal verification has been in the role of supplementing more traditional coverage oriented testing activities. For the recent Intel(r) Core(tm) 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 of the design. We applied symbolic simulation based formal verification techniques for full data-path, 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.

Biography

Roope Kaivola is a Principal Engineer in the Converged Core Development Organization of Intel Corporation. He has worked on formal verification of Intel microprocessor component designs over the last ten years. During this time, formal verification in Intel has evolved from an untested technology giving one-off solutions to research grade problems to a mainstream engineering activity that is now routinely applied to new designs.

Roope Kaivola's area of specialization is the formal verification of arithmetic hardware. He has personally carried out formal verification of most recent Intel divider designs from Pentium 4 up to Intel Core i7, and he is the technical lead of a formal verification application group associated with a number of Intel's recent flagship processors. Prior to joining Intel in 1999, Roope Kaivola carried out academic study and research on formal verification for most of 1990's, including Ph.D. degrees in Computer Science from the University of Helsinki, Finland, and University of Edinburgh, Scotland, and a spell as a faculty member in Helsinki.