Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice

Model checking and theorem proving have largely complementary strengths and weaknesses. Thus, a research goal for many years has been to find effective and practical ways of combining these approaches. However, this goal has been much harder to reach than originally anticipated, and several false starts have been reported in the literature. In fact, some researchers have gone so far as to question whether there even exists an application domain in which such a hybrid solution is needed. In this talk I will argue that formal verification of the floating-point circuits of modern high-performance microprocessors is such a domain. In particular, when a correctness statement linking the actual low-level (gate-level) implementation with abstract floating-point numbers is needed, a combined model checking and theorem proving based approach is essential. To substantiate the claim, I will draw from data we have collected during the verification of the floating point units of several generations of Intel microprocessors. In addition, I will discuss the in-house formal verification environment we have created that has enabled this effort with an emphasis on how model checking and theorem proving have been integrated without sacrificing usability.

Authors and Affiliations

1. Intel Strategic CAD Labs, Portland, OR

   Carl-Johan Seger

Editors and Affiliations

1. Toyota Technological Institute at Chicago, 1427 E. 60th Street, 60637, Chicago, Illinois

   David McAllester

Reprints and permissions

© 2000 Springer-Verlag Berlin Heidelberg

Policies and ethics