Implementation Specific Verification of Divide and Square Root Instructions

Floating point operations such as divide and square root are typically implemented in microcode rather than dedicated logic. Bugs in these operations missed by generic black-box verification tools, were analyzed. This led to the conclusion that the corner cases, in addition to being implementation dependent, could not be characterized in terms of special input or output values in a straightforward manner. However, many of those cases can be easily generalized for many known implementations. The typical implementation uses a known iterative approximation algorithm, such as the Newton-Raphson method, to calculate the desired result; thus, it is sufficient to produce the corner cases associated with the specific algorithm. We investigated the following problem: given an iterative algorithm to compute a binary floating point operation, the iteration number, and an interval, find random inputs for the operation that, after the requested iteration, yield a relative error within the specified interval. This paper describes a method to solve this problem. This method was implemented in a floating-point test generator and is currently being used to verify the floating-point units of several processors.