Carnegie Mellon University

File(s) stored somewhere else

Please note: Linked content is NOT stored on Carnegie Mellon University and we can't guarantee its availability, quality, security or accept any liability.

Verification of Floating Point Adders

journal contribution
posted on 1998-01-01, 00:00 authored by Yirng-An Chen, Randal BryantRandal Bryant

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 wordlevel SMV, which is improved by using the Multiplicative Power HDDs (*PHDDs), and by incorporating conditional symbolic simulation as well as a shortcircuiting technique. Based on the case analysis, the specifications of FP adders are divided into several hundreds of implementation independent subspecifications. 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 UltraSPARCII server.


Publisher Statement

All Rights Reserved



Usage metrics


    Ref. manager