CMU-CS-98-121
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-98-121

Verification of Floating-Point Adders

Yirng-An Chen, Randal E. Bryant

April 1998

CMU-CS-98-121.ps


The floating-point 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 floating-point arithmetic circuits. In this paper, we present a "black box" version of verification of FP adders. In our approach, FP adders are verified by an extended word-level SMV using reusable specifications without knowing the circuit mplementation. Word-level SMV is improved by using Multiplicative Power HDDs (*PHDDs), and by incorporating conditional symbolic simulation as well as a short-circuiting technique. Based on a case analysis, the adder specification is divided into several hundred implementation-independent sub-specifications. We applied our system and these specifications to verify the IEEE double precision FP adder in the Aurora III Chip from the University of Michigan. Our system found several design errors in this FP adder. Each specification can be checked in less than 5 minutes. A variant of the corrected FP adder was created to illustrate the ability of our system to handle different FP adder designs. For each adder, the verification task finished in 2 CPU hours on a Sun UltraSPARC-II server.

Keywords: Binary moment diagram, *BMD, hybrid decision diagram, HDD, K*BMD, multiplicative power hybrid decision diagram, *PHDD, arthimetic circuit, floating-point adder, IEEE standard, formal verification


22 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu