|
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
|