Formal verification in Intel CPU design

Summary form only given. This article relates a success story: formal verification of floating-point operations implemented in hardware, using a combination of model checking (symbolic trajectory evaluation) and higher-order logic theorem proving. Our tools and methods have been applied to a number of design projects, including the Pentium (R) 4 processor. In designing the Pentium 4 formal verification was indispensable, capturing several extremely subtle bugs that eluded simulation. Any of these could have resulted in an FDIV-like recall. It explains the tools and technologies we used, the lessons we learned, and next challenges we face.