
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Elena Guralnik, Merav Aharoni, Ariel J. Birnbaum, Anatoly Koyfman, "SimulationBased Verification of FloatingPoint Division," IEEE Transactions on Computers, vol. 60, no. 2, pp. 176188, February, 2011.  
BibTex  x  
@article{ 10.1109/TC.2010.165, author = {Elena Guralnik and Merav Aharoni and Ariel J. Birnbaum and Anatoly Koyfman}, title = {SimulationBased Verification of FloatingPoint Division}, journal ={IEEE Transactions on Computers}, volume = {60}, number = {2}, issn = {00189340}, year = {2011}, pages = {176188}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2010.165}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  SimulationBased Verification of FloatingPoint Division IS  2 SN  00189340 SP176 EP188 EPD  176188 A1  Elena Guralnik, A1  Merav Aharoni, A1  Ariel J. Birnbaum, A1  Anatoly Koyfman, PY  2011 KW  Computer arithmetic KW  verification KW  test generation. VL  60 JA  IEEE Transactions on Computers ER   
[1] N.H.F. Beebe, "IEEE754 FloatingPoint Test Software," http://www.math.utah.edu/beebe/softwareieee, 2010.
[2] IEEE Standard for Binary FloatingPoint Arithmetic, IEEE Std. 7542008, pp. 158, 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. (ARITH14), pp. 116123, 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. (ARITH15), pp. 119127, 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 FloatingPoint Instructions," Proc. 16th IEEE Computer Arithmetic Symp. (ARITH16), pp. 158164, 2003.
[7] "FloatingPoint 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. 744, 1999.
[9] S.D. Trong, M. Schmookler, E.M. Schwarz, and M. Kroener, "P6 Binary FloatingPoint Unit," Proc. 18th IEEE Computer Arithmetic Symp. (ARITH18), pp. 7786, 2007.
[10] J. Harrison, "Formal Verification of IA64 Division Algorithms," Lecture Notes in Computer Science, pp. 233251, Springer, 2000.
[11] J. Harrison, "Isolating Critical Cases for Reciprocals Using Integer Factorization," Proc. 16th IEEE Computer Arithmetic Symp. (ARITH16), pp. 148157, 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. (DAC35), pp. 158165, 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 FloatingPoint Operations," Proc. 18th IEEE Computer Arithmetic Symp. (ARITH18), pp. 3845, 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. (ARITH14), pp. 233240, 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 FloatingPoint Verification," Proc. 17th IEEE Computer Arithmetic Symp. (ARITH17), pp. 7683, 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. (ARITH19), pp. 114121, 2009.
[18] Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus, and G. Shurek, "ConstraintBased Random Stimuli Generation for Hardware Verification," AI Magazine, vol. 28, no. 3, p. 1330, 2007.
[19] A. Aharon, Y. Lichtenstein, and Y. Malka, "ModelBased Test Generator for Processor Design Verification," Innovative Applications of Artificial Intelligence (IAAI), 1994.