Verification of Floating-Point Adders

摘要

The floating-point division bug in Intel's Pentium processor and the overflowflag erratum of the FIST instruction in Intel's Pentium Pro andPentium II processor have demonstrated the importance and the difficultyof 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-independ entsub-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.