High-level formal verification of next-generation microprocessors

Formal property verification has been an effective complement to pre-silicon validation of several Intel® Pentium® 4 CPU designs at Intel Corporation. The principal objective of this program has been to prove design correctness rather than hunt for bugs. In the process, we have evolved our tools and methodology and are now applying FPV techniques to protocol level properties. Moving forward, new technologies such as GSTE and SAT offer the potential to significantly increase the scope of what can be formally verified. This paper discusses the application of FPV to validation of the Intel® Pentium® 4 microarchitecture and some approaches being considered to broaden the application of FV techniques, particularly at a higher level of design abstraction.