Verification of Floating-Point Adders

The floating-point(FP) division bug in Intel’s Pentium processor and the overflow flag erratum of the FIST instruction in Intel’s Pentium Pro and Pentium II processor have demonstrated the importance and the difficulty of verifying FP arithmetic circuits. In this paper, we present the verification of FP adders with reusable specifications, using extended word-level SMV, which is improved by using the Multiplicative Power HDDs (*PHDDs), and by incorporating conditional symbolic simulation as well as a short-circuiting technique. Based on the case analysis, the specifications of FP adders are divided into several hundreds of implementation-independent sub-specifications. We applied our system and these specifications to verify the IEEE double precision FP adder in the Aurora III Chip at the University of Michigan. Our system found several design errors in this FP adder and generated one counterexample for each error within several minutes. A variant of the corrected FP adder is created to illustrate the capability of our system to handle different FP adder designs. For each of FP adders, the verification task finished in 2 CPU hours on a Sun Ultra-SPARCII server.