Verification of Floating-Point Adders
Abstract
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 implementation. 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 EP adder designs. For each adder, the verification task finished in 2 CPU hours on a Sun UltraSPARC-II server.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1997
- Accession Number
- ADA346061
Entities
People
- Randal Bryant
- Yirng-an Chen
Organizations
- Carnegie Mellon University