Floating-point division is known to exhibit an exceptionally wide array of corner cases, making its verification a difficult challenge. Despite the remarkable advances in formal methods, the intricacies of this operation and its implementation often render these inapplicable. Simulation-based methods remain the primary means for verification of division. FPgen is a test generation framework targeted at the floating point datapath. It has been successfully used in the simulation-based verification of a variety of hardware designs. FPgen comprises a comprehensive test plan and a powerful test generator. A proper response to the difficulties posed by division constitutes a major part of FPgen's capabilities. We present an overview of the relevant verification tasks supplied with FPgen and the underlying algorithms used to target them.

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.