Abstract
In this paper, we present a verification methodology that integrates formal verification techniques with verification by simulation, thereby providing means for generating simulation test suites that ensure coverage. We derive the test suites by means of BDD-based symbolic techniques for describing and traversing the implementation state space. In our approach, we provide a high-level of control over the generated test suites; a powerful abstraction mechanism directs the generation procedure to specific areas, that are the focus for verification, thereby withstanding the state explosion problem. The abstraction is achieved by partitioning the implementation state variables into categories of interest. We also depart from the traditional graph-algorithmic model for conformance testing; instead, using temporal logic assertions, we can generate a test suite where the set of state sequences (paths) satisfies some temporal properties as well as guaranteeing transition coverage. Our methodology has been successfully applied to the generation of test suites for IBM PowerPC and AS/400 systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Aharon, D. Goodman, M. Levinger, Y. Lichtenstein, Y. Malka, C. Metzger, M. Molcho, and G. Shurek. Test program generation for functional verification of powerpc processors in ibm. In 32nd Design Automation Conference, DAC 95, pages 279–285, 1995.
A. Aho, B. Kerningham, and P. Weinberger. The AWK Programming Language. Addison-Wesley, 1988.
I. Beer, M. Dvir, Kozitza B., Y. Lictenstein, S. Mack, W.J. Nee, Rappaport E., Schmierer Q., and Y. Zandman. VHDL Test Coverage in a BDLS/AUSSIM Environment. Technical Report 88 342 IBM Science and Technology, Haifa, Israel, 1993.
I. Beer, M. Yoeli, S. Ben-David, R. Gewirtzman, and D. Geist. Methodology and System for Practical Formal Verification of Reactive Hardware. In Computer Aided Verification, pages 182–193, 1994.
B. Beizer. Software Testing Techniques. Van Nostrand Reinhold, New York, 1990.
A. Benoit and D. Luckham. Validating Discrete Event Simulations Using Event Pattern Mappings. In ACM/IEEE Design Automation Conference, pages 414–419, 1992.
E. Brinksma. A theory for the derivation of tests. In S. Aggarwal and K Sabanni, editors, Protocol Specification, Testing, and Verification, HIV, pages 119–131. IFIP, North Holland, 1988.
R. E. Bryant. Graph based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35, 1986.
S.P. van de Burgt, J. Kroon, E. Kwast, and H.J. Wilts, the RNL Conformance Kit. In J. de Meer, L. Mackert, and W. Effelsberg, editors, Proc. of the 2nd International Workshop on Protocol Test Systems, pages 279–294. North-Holland, October 1989.
W. Y.L. Chan, S. T. Vuong, and M.R. Ito. On test sequence generation for protocols. In E. Brinksma, G Scollo, and C.A. Vissers, editors, Protocol Specification, Testing, and Verification, IX, pages 119–131. IFIP, North Holland, 1990.
A. Chandra, V. Iyengar, D. Jameson, R. Jawalkelar, I. Nair, B. Rosen, M. Mullen, J. Yoon, R. Armoni, D. Geist, and Y. Wolfsthal. AVPGEN — A Test Case Generator for Architecture Verification. IEEE Transactions on VLSI Systems, 6(6), June 1995.
E. Clarke, O. Grumberg, K.Mcmillan, and X. Zhao. Efficient generation of counter examples and witnesses in symbolic model checking. 32nd ACM/IEEE Design Automation Conference, pages 427–432, 1995.
M. Farkas, D. Geist, and K. Holtz. SysGen Architecture Verification Program Generator User's Guide. IBM Science and Technology, Haifa, Israel, first edition, 1994.
M. S. Garey and D. S. Johnson. Computers and Intractability. W. H. Freeman and Co., New York, 1979.
R. C. Ho, C. H. Yang, M. A. Horowitz, and D. L. Dill. Architecture validation for processors. In International Symposium of Computer Architecture 1995, pages 404–413, 1995.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
H. Iwashita, S. Kowatari, T. Nakata, and F. Hirose. Automatic test program generation for pipelined processors. In International Conference on Computer Aided Design, November 1994.
D. Levin, D. Lorenz, and S. Ur, A methodology for processor implementation verification. In FMCAD 96: Int. Conf. on Formal Methods in Computer-Aided Design, NOV 1996. to appear.
C. May, E. Silha, R. Simpson, H. Warren, eds. The PowerPC Architecture. Morgan Kaufmann, 1994.
K. L. McMillan. The SMV System DRAFT. Carnegie Mellon University, Pittsburgh, PA, 1992.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Press, Norwell, MA, 1993.
PCI Special Interests Group, Portland, OR. PCI Local Bus Specification, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geist, D., Farkas, M., Landver, A., Lichtenstein, Y., Ur, S., Wolfsthal, Y. (1996). Coverage-directed test generation using symbolic techniques. In: Srivas, M., Camilleri, A. (eds) Formal Methods in Computer-Aided Design. FMCAD 1996. Lecture Notes in Computer Science, vol 1166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031805
Download citation
DOI: https://doi.org/10.1007/BFb0031805
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61937-6
Online ISBN: 978-3-540-49567-3
eBook Packages: Springer Book Archive