Solving range constraints for binary floating-point instructions

Abstract

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 x̄, ȳ, z̄ such that x̄ ∈ Rx, ȳ ∈ Ry, z̄ ∈ Rz, and z̄ = round(x̄ op ȳ). 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 floating-point units of several processors.