Solving the generalized mask constraint for test generation of binary floating point add operation. (English) Zbl 1064.68008
Summary: The mathematical problem discussed is important for generating test cases in order to debug floating point adders designs. Floating point numbers are assumed to be written as strings of \({0,1}\) bits, in a format compatible with IEEE standard 754. A mask is a string of characters, composed of {‘0’, ‘1’, ‘x’}. A number and a mask are compatible if they have the same length and each numerical character of the mask (‘0’ or ‘1’) is equal, numerically, to the bit of the number, in the same position. The problem discussed is: Given masks \(M_{a},\) \(M_{b},\) \(M_{c},\) of identical lengths, generate three floating point numbers \(\bar a,\bar b,\bar c\), which are compatible with the masks and satisfy \(\bar c=\text{round}(\bar a\pm \bar b)\). If there are many solutions, choose one at random. A fast algorithm is given which solves the problem for all IEEE floating point data types and all rounding modes.
MSC:
| 68M07 | Mathematical problems of computer architecture |
References:
| [1] | M.D. Aagaard, R.B. Jones, R. Kaivola, K.R. Kohastsu, Carl-Johan, J. Seger, Formal Verification of Iterative Algorithms in Microprocessors, Intel Corporation, Hillsboro, Oregon, USA, DAC 2000.; M.D. Aagaard, R.B. Jones, R. Kaivola, K.R. Kohastsu, Carl-Johan, J. Seger, Formal Verification of Iterative Algorithms in Microprocessors, Intel Corporation, Hillsboro, Oregon, USA, DAC 2000. |
| [2] | A. Aharon, D. Goodman, M. Levinger, Y. Lichtenstein, Y. Malka, C. Metzger, M. Molcho, G. Shurek, Test program generation for functional verification of powerPC processors in IBM, 32nd Design Automation Conference, San Francisco, June 1995, pp. 279-285.; A. Aharon, D. Goodman, M. Levinger, Y. Lichtenstein, Y. Malka, C. Metzger, M. Molcho, G. Shurek, Test program generation for functional verification of powerPC processors in IBM, 32nd Design Automation Conference, San Francisco, June 1995, pp. 279-285. |
| [3] | Beizer, B., Software Testing Techniques (1990), Van Nostrand Reinhold: Van Nostrand Reinhold New York |
| [4] | Clarke, E. M.; German, S. M.; Zhao, X., Verifying the SRT division algorithm using theorem proving techniques, Formal Methods System Des., 14, 1, 7-44 (1999) |
| [5] | L. Fournier, Y. Arbetman, M. Levinger, Functional verification methodology for microprocessors using the genesys test program generator, Application to the x86 Microprocessors Family, DATE99, Munchen, 1999.; L. Fournier, Y. Arbetman, M. Levinger, Functional verification methodology for microprocessors using the genesys test program generator, Application to the x86 Microprocessors Family, DATE99, Munchen, 1999. |
| [6] | L. Fournier, D. Lewin, M. Levinger, E. Roytman, G. Shurek, Constraint satisfaction for test program generation, Internat. Phoenix Conf. on Computers and Communications, March 1995.; L. Fournier, D. Lewin, M. Levinger, E. Roytman, G. Shurek, Constraint satisfaction for test program generation, Internat. Phoenix Conf. on Computers and Communications, March 1995. |
| [7] | R. Grinwald, E. Harel, M. Orgad, S. Ur, A. Ziv, User defined coverage—a tool supported methodology for design verification, in: Proc. 35th Design Automation Conf. (DAC), June 1998, pp. 158-163.; R. Grinwald, E. Harel, M. Orgad, S. Ur, A. Ziv, User defined coverage—a tool supported methodology for design verification, in: Proc. 35th Design Automation Conf. (DAC), June 1998, pp. 158-163. |
| [8] | IEEE standard for binary floating point arithmetic, An American National Standard, ANSI/IEEE Std 754-1985.; IEEE standard for binary floating point arithmetic, An American National Standard, ANSI/IEEE Std 754-1985. |
| [9] | C. Kaner, Software negligence and testing coverage, in: Proc. of STAR 96: the Fifth Internat. Conf., Software Testing, Analysis and Review, June 1996, pp. 299-327.; C. Kaner, Software negligence and testing coverage, in: Proc. of STAR 96: the Fifth Internat. Conf., Software Testing, Analysis and Review, June 1996, pp. 299-327. |
| [10] | Y. Lichtenstein, Y. Malka, A. Aharon, Model-Based Test Generation For Processor Design Verification, Innovative Applications of Artificial Intelligence (IAAI), AAAI Press, New York, 1994.; Y. Lichtenstein, Y. Malka, A. Aharon, Model-Based Test Generation For Processor Design Verification, Innovative Applications of Artificial Intelligence (IAAI), AAAI Press, New York, 1994. |
| [11] | Marick, B., The Craft of Software Testing, Subsystem Testing Including Object-Based and Object-Oriented Testing (1995), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ |
| [12] | Mueller, S. M.; Paul, W. J., Computer Architecture, Complexity and Correctness (2000), Springer: Springer Berlin, Heidelberg · Zbl 0966.68023 |
| [13] | J. o’Leary, X. Zhao, R. Gerth, C.-J.H. Seger, Formally verifying IEEE compliance of floating-point hardware, Intel Technology Journal, vol. 1999-Q1, pp. 1-14. Available on the Web as http://developer.intel.com/technology/itj/q11999/articles/art_5.htm; J. o’Leary, X. Zhao, R. Gerth, C.-J.H. Seger, Formally verifying IEEE compliance of floating-point hardware, Intel Technology Journal, vol. 1999-Q1, pp. 1-14. Available on the Web as http://developer.intel.com/technology/itj/q11999/articles/art_5.htm |
| [14] | M. Parks, Number-theoretic test generation for directed rounding, 14th IEEE Symposium on Computer Arithmetic, Adelaida, Australia, April 1999, pp. 241-248.; M. Parks, Number-theoretic test generation for directed rounding, 14th IEEE Symposium on Computer Arithmetic, Adelaida, Australia, April 1999, pp. 241-248. |
| [15] | Russinoff, D. M., A mechanically checked proof of correctness of the AMD K5 floating point square root microcode, Formal Methods System Des., 14, 1, 75-125 (1999) |
| [16] | A. Ziv, L. Fournier, Test generation for the binary floating point add operation with mask-mask-mask constraints, IBM Research and Development Laboratories in Israel, Technical Report 88.388, February 2001.; A. Ziv, L. Fournier, Test generation for the binary floating point add operation with mask-mask-mask constraints, IBM Research and Development Laboratories in Israel, Technical Report 88.388, February 2001. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
