Solving Range Constraints for Binary Floating-Point Instructions

We present algorithms that solve the following prob-lem: 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, y ̄ ∈ 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 con-sidering ranges of machine numbers. We provide full solu-tions 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 ver-ification 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.