Solving range constraints for binary floating-point instructions
Abraham Ziv, Merav Aharoni, et al.
ARITH 2003
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. © 2006 IEEE.
Abraham Ziv, Merav Aharoni, et al.
ARITH 2003
Elena Guralnik, Ariel J. Birnbaum, et al.
ARITH 2009
Merav Aharoni, Sigal Asaf, et al.
ARITH 2005
Jeonghee Shin, John A. Darringer, et al.
SOCC 2011