Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE '04
Download PDF

Abstract

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.
Like what you’re reading?
Already a member?Sign In
Member Price
$11
Non-Member Price
$21
Add to CartSign In
Get this article FREE with a new membership!

Related Articles