Correctness Proofs Outline for Newton-Raphson Based Floating-Point Divide and Square Root Algorithms

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

• Type: Conference
• Year: 1999
• Where: ARITH
• Authors: Marius A. Cornea-Hasegan, Roger A. Golliver, Peter W. Markstein
• Keywords: Applied Computing, ARITH 1999, IEEE Correctness, Square Root, Square Root Algorithm