16th IEEE Symposium on Computer Arithmetic (ARITH-16 '03)
Solving Range Constraints for Binary Floating-Point Instructions
Santiago de Compostela, Spain
June 15-June 18
ISBN: 0-7695-1894-X
We present algorithms that solve the following problem: given three ranges of floating-point numbers Rx, Ry, Rz, a floating-point operation (op), and a rounding-mode (round), generate three floating-point numbers \overline x ,\overline y ,\overline z such that \overline x \in R_x ,\overline y \in R_y ,\overline z \in R_z , and \overline z = round(\overline x op \overline y). This problem, although quite simple when dealing with intervals of real numbers, is much more complex when considering ranges of machine numbers. We provide full solutions for add and subtract, and partial solutions for multiply and divide. We use range constraints on the input operands and on the result operand of floating-point instructions to target corner cases when generating test cases for use in verification of floating-point hardware. The algorithms have been implemented in a floating-point test-generator and are currently being used to verify floatingpoint units of several processors.
Citation:
Abraham Ziv, Merav Aharoni, Sigal Asaf, "Solving Range Constraints for Binary Floating-Point Instructions," arith, pp.158, 16th IEEE Symposium on Computer Arithmetic (ARITH-16 '03), 2003