This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Simulation-Based Verification of Floating-Point Division
February 2011 (vol. 60 no. 2)
pp. 176-188
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
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.

[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.

Index Terms:
Computer arithmetic, verification, test generation.
Citation:
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, Feb. 2011, doi:10.1109/TC.2010.165
Usage of this product signifies your acceptance of the Terms of Use.