Issue No.02 - February (2011 vol.60)
Elena Guralnik , IBM Research Haifa, Haifa
Merav Aharoni , IBM Research Haifa, Haifa
Ariel J. Birnbaum , IBM Research Haifa, Haifa
Anatoly Koyfman , IBM Research Haifa, Haifa
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2010.165
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.
Computer arithmetic, verification, test generation.
Elena Guralnik, Merav Aharoni, Ariel J. Birnbaum, Anatoly Koyfman, "Simulation-Based Verification of Floating-Point Division", IEEE Transactions on Computers, vol.60, no. 2, pp. 176-188, February 2011, doi:10.1109/TC.2010.165