Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking

This paper presents the formal verification of all sub-circuits in a floating-point arithmetic unit (FPU) from an Intel microprocessor using a word-level model checker. This work represents the first large-scale application of word-level model checking techniques. The FPU can perform addition, subtraction, multiplication, square root, division, remainder, and rounding operations; verifying such a broad range of functionality required coupling the model checker with a number of other techniques, such as property decomposition, property-specific model extraction, and latch removal. We will illustrate our verification techniques using the Weitek WTL3170/3171 Sparc floating point coprocessor as an example. The principal contribution of this paper is a practical verification methodology explaining what techniques to apply (and where to apply them) when verifying floating-point arithmetic circuits. We have applied our methods to the floating-point unit of a state-of-the-art Intel microprocessor, which is capable of extended precision (64-bit mantissa) computation. The success of this effort demonstrates that word-level model checking, with the help of other verification techniques, can verify arithmetic circuits of the size and complexity found in industry.