Automatic Formal Verification of Fused-Multiply-Add FPUs

In this paper we describe a fully-automated methodology for formal verification of fused-multiply-add floating point units (FPU). Our methodology verifies an implementation FPU against a simple reference model derived from the processor's architectural specification, which may include all aspects of the IEEE specification including denormal operands and exceptions. Our strategy uses a combination of BDD- and SAT-based symbolic simulation. To make this verification task tractable, we use a combination of case-splitting, multiplier isolation, and automatic model reduction techniques. The case-splitting is defined only in terms of the reference model, which makes this approach easily portable to new designs. The methodology is directly applicable to multi-GHz industrial implementation models (e.g., HDL or gate-level circuit representations) that contain all details of the high-performance transistor-level model, such as aggressive pipelining, clocking, etc. Experimental results are provided to demonstrate the computational efficiency of this approach.