Subscribe

Issue No.02 - February (2011 vol.60)

pp: 176-188

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

ABSTRACT

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.

INDEX TERMS

Computer arithmetic, verification, test generation.

CITATION

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.165REFERENCES

- [1] N.H.F. Beebe, "IEEE754 Floating-Point Test Software," http://www.math.utah.edu/beebe/softwareieee, 2010.
- [2]
IEEE Standard for Binary Floating-Point Arithmetic, IEEE Std. 754-2008, pp. 1-58, 2008.- [3] R.C. Agarwal, F.G. Gustavson, and M.S. Schmookler, "Series Approximation Methods for Divide and Square Root in the Power3™ Processor,"
Proc. 14th IEEE Computer Arithmetic Symp. (ARITH-14), pp. 116-123, 1999.- [4] L.D. McFearin and D.W. Matula, "Generation and Analysis of Hard to Round Cases for Binary Floating Point Division,"
Proc. 15th IEEE Computer Arithmetic Symp. (ARITH-15), pp. 119-127, 2001.- [5] M. Aharoni, S. Asaf, L. Fournier, A. Koyfman, and R. Nagel, "FPgen—A Test Generation Framework for Datapath Floating Point Verification,"
Proc. IEEE Int'l. High Level Design Validation and Test Workshop (HLDVT '03), 2003. - [6] R. Ziv, M. Aharoni, and S. Asaf, "Solving Range Constraints for Binary Floating-Point Instructions,"
Proc. 16th IEEE Computer Arithmetic Symp. (ARITH-16), pp. 158-164, 2003.- [7] "Floating-Point Test Suite for IEEE 754R Standard," http://www.haifa.il.ibm.com/projects/verification/ fpgenieeets.html, 2010.
- [8] E.M. Clarke, S.M. German, and X. Zhao, "Verifying the SRT Division Algorithm Using Theorem Proving Techniques,"
Formal Methods in System Design, vol. 14, no. 1, pp. 7-44, 1999.- [9] S.D. Trong, M. Schmookler, E.M. Schwarz, and M. Kroener, "P6 Binary Floating-Point Unit,"
Proc. 18th IEEE Computer Arithmetic Symp. (ARITH-18), pp. 77-86, 2007.- [10] J. Harrison, "Formal Verification of IA-64 Division Algorithms,"
Lecture Notes in Computer Science, pp. 233-251, Springer, 2000.- [11] J. Harrison, "Isolating Critical Cases for Reciprocals Using Integer Factorization,"
Proc. 16th IEEE Computer Arithmetic Symp. (ARITH-16), pp. 148-157, 2003.- [12] R. Grinwald, E. Harel, M. Orgad, S. Ur, and A. Ziv, "User Defined Coverage—A Tool Supported Methodology for Design Verification,"
Proc. 35th Design Automation Conf. (DAC-35), pp. 158-165, June 1998.- [13] A.Y. Khinchin,
Continued Fractions. Dover, 1997.- [14] M. Aharoni, R. Maharik, and A. Ziv, "Solving Constraints on the Intermediate Result of Decimal Floating-Point Operations,"
Proc. 18th IEEE Computer Arithmetic Symp. (ARITH-18), pp. 38-45, 2007.- [15] C. Iordache and D.W. Matula, "On Infinitely Precise Rounding for Division, Square Root, Reciprocal and Square Root Reciprocal,"
Proc. 14th IEEE Computer Arithmetic Symp. (ARITH-14), pp. 233-240, 1999.- [16] M. Aharoni, S. Asaf, R. Maharik, I. Nehama, I. Nikulshin, and A. Ziv, "Solving Constraints on the Invisible Bits of the Intermediate Result for Floating-Point Verification,"
Proc. 17th IEEE Computer Arithmetic Symp. (ARITH-17), pp. 76-83, 2005.- [17] E. Guralnik, A.J. Birnbaum, A. Koyfman, and A. Kaplan, "Implementation Specific Verification of Divide and Square Root Instructions,"
Proc. 19th IEEE Computer Arithmetic Symp. (ARITH-19), pp. 114-121, 2009.- [18] Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus, and G. Shurek, "Constraint-Based Random Stimuli Generation for Hardware Verification,"
AI Magazine, vol. 28, no. 3, p. 1330, 2007.- [19] A. Aharon, Y. Lichtenstein, and Y. Malka, "Model-Based Test Generator for Processor Design Verification,"
Innovative Applications of Artificial Intelligence (IAAI), 1994. |