Guest lecture by Roope Kaivola
|
Title
Proof Engineering in the Large: Formal Verification of Pentium 4
Floating-Point Divider
Speaker
Time and Place
- Monday, September 10, 2001
- at 10 - 12
- Room A 414 (4th floor), Department of Computer Science
Abstract
We examine the challenges presented by large-scale formal
verification of industrial-size circuits, based on our
experiences in verifying the class of all micro-operations
executing on the floating-point division and square root
unit of the Intel IA-32 Pentium 4 microprocessor. The
verification methodology is based on combining human-guided
mechanised theorem-proving with low-level steps verified
by fully automated model-checking. A key observation
in the work is the need to explicitly address the issues of
proof design and proof engineering, i.e. the process of
creating proofs and the craft of structuring and formulating
them, as concerns on their own right.
|