loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
14th IEEE Symposium on Computer Arithmetic (ARITH-14 '99)
Correctness Proofs Outline for Newton-Raphson Based Floating-Point Divide and Square Root Algorithms
Adelaide, Australia
April 14-April 16
ISBN: 0-7695-0116-8
Marius A. Cornea-Hasegan, Intel Corporation
Roger A. Golliver, Intel Corporation
Peter Markstein, Hewlett-Packard
This paper describes a study of a class of algorithms for the floating-point divide and square root operations, based on the Newton-Raphson iterative method. The two main goals were: (1) Proving the IEEE correctness of these iterative floating-point algorithms, i.e. compliance with the IEEE-754 standard for binary floating-point operations [1]. The focus was on software driven iterative algorithms, instead of the hardware based implementations that dominated until now. (2) Identifying the special cases of operands that require software assistance due to possible overflow, underflow, or loss of precision of intermediate results.This study was initiated in an attempt to prove the IEEE correctness for a class of divide and square root algorithms based on the Newton-Rapshson iterative methods. As more insight into the inner workings of these algorithms was gained, it became obvious that a formal study and proof were necessary in order to achieve the desired objectives. The result is a complete and rigorous proof of IEEE correctness for floating-point divide and square root algorithms based on the Newton-Raphson iterative method. Even more, the method used in proving the IEEE correctness of the square root algorithm is applicable in principle to any iterative algorithm, not only based on the Newton-Raphson method. Conditions requiring Software Assistance (SWA) were also determined, and were used to identify cases when alternate algorithms are needed to generate correct results. Overall, this is one important step toward flawless implementation of these floating-point operations based on software implementations.
Citation:
Marius A. Cornea-Hasegan, Roger A. Golliver, Peter Markstein, "Correctness Proofs Outline for Newton-Raphson Based Floating-Point Divide and Square Root Algorithms," arith, pp.96, 14th IEEE Symposium on Computer Arithmetic (ARITH-14 '99), 1999
Usage of this product signifies your acceptance of the Terms of Use.