Verification of complex datapath circuits such as floating-point dividers are known to be a challenging problem. In this paper, we present a formal verification methodology to verify floating-point (FP) dividers. In general, floating-point division unit builds around a fixed-point division implementation. Our solution performs a two-step verification.The first step verifies the fixed-point division implementation. We target fixed-point division algorithms that compute a fixed number of quotient bits in each iteration. This step uses a combination of equivalence checking and assertion-based property checking techniques. We used property checking to show correctness of radix-2 restoring division and equivalence checking to show equivalence between the radix-2 restoring division and a prescaled radix-4 non-restoring division.The second step uses equivalence checking to compare the floating-point divider with a software golden reference of FP division. In this step we assume the fixed-point division is working correctly to make the proof tractable. Using the proposed steps, verification of single precision FP divider took 1 hour 30 minutes and double precision FP divider took 7 hours and 30 minutes.

We present a generic digit serial method (DSM) to compute the digits of a real number V. Bounds on these digits, and on the errors in the associated estimates of V formed from these digits, are derived. To illustrate our results, we derive such bounds for a parameterized family of high-radix algorithms for division and square root. These bounds enable a DSM designer to determine, for example, whether a given choice of parameters allows rapid formation and rounding of its approximation to V.

Back in the 60's Goldschmidt presented a variation of Newton-Raphson iterations for division that is well suited for pipelining. The problem in using Goldschmidt's division algorithm is to present an error analysis that enables one to save hardware by using just the right amount of precision for intermediate calculations while still providing correct rounding. Previous implementations relied on combining formal proof methods (that span thousands of lines) with millions of test vectors. These techniques yield correct designs but the analysis is hard to follow and is not quite tight. We present a simple parametric error analysis of Goldschmidt's division algorithm. This analysis sheds more light on the effect of the different parameters on the error. In addition, we derive closed error formulae that allow to determine optimal parameter choices in four practical settings. We apply our analysis to show that a few bits of precision can be saved in the floating-point division (FP-DIV) microarchitecture of the AMD-K7/spl trade/ microprocessor. These reductions in precision apply to the initial approximation and to the lengths of the multiplicands in the multiplier. When translated to cost, the reductions reflect a savings of 10.6% in the overall cost of the FP-DIV microarchitecture.

Results are presented that identify when the computed value of a sum or difference is exact. The accuracy of an argument reduction algorithm is analyzed using these results. This analysis demonstrates that catastrophic cancellation does not occur in this algorithm's computation of the reduced argument.>

A technique for computing monotonicity preserving approximations F/sub a/(x) of a function F(x) is presented. This technique involves computing an extra precise approximation of F(x) that is rounded to produce the value of F/sub a/(x). For example, only a few extra bits of precision are used to make the accurate transcendental functions found on the Cyrix FasMath line of 80387 compatible math coprocessors monotonic.>

One can naively view a computer number system as a pair (F, P) consisting of a finite set F of real numbers and a rounding rule P. One such number system is a hyperbolic rational number system which has as F a finite set of rational numbers and as P the so-called mediant rounding rule. In this paper we demonstrate how one can simulate a hyperbolic rational number system in any high level language that supports floating point computation. From this simulation we infer that hyperbolic rational number systems form viable alternatives to traditional binary floating point number systems. Many properties of hyperbolic rational number systems are derived from the relationship of their rounding rule to the well-developed theory of best rational approximation.