High level formal verification of next-generation microprocessors
Tom Schubert · 2003
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 will discuss 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.