Abstract
Generalized STE (Symbolic Trajectory Evaluation) [21,22,23] is a very significant extension of STE [11,20] that truly combines the efficiency, capacity and ease of use of STE with the ability of classic symbolic model checking for verifying a much richer set of properties [9]. GSTE provides a unified model checking framework that gives one the power to choose and seamlessly adjust the level of abstraction in a model as well as in a specification during a verification effort. This paper describes some of the techniques that made this possible using a simple FIFO example for illustration. Finally, a set of real life verification results is provided to strongly demonstrate the viability of GSTE as a new generation model checking solution for complex designs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Aagaard, R. Jones, T. Melham, J. O’Leary, and C.-J. Seger. A methodology for large-scale hardware verification. In FMCAD’2000, November 2000.
M. Aagaard, R. Jones, and C.-J. Seger. Combining theorem proving and trajectory evaluation in an industrial environment. In Proceedings of the 35th DAC, pages 538–541, June 1998.
M. Aagaard, R. Jones, and C.-J. Seger. Formal verification using parametric representations of boolean constraints. In Proceedings of the 36th DAC, June 1999.
F. Balarin and A. Sangiovanni-Vincentelli. An iterative approach to language containment. In Proc. of the 5th Workshop on CAV, pages 193–195, 1999.
D. Beatty and R. Bryant. Formally verifying a microprocessor using symbolic simulation methodology. In Proceedings of the 31st DAC, June 1994.
R. Bryant and C.-J. Seger. Formal verification of digital circuits using symbolic ternary system models. In DIMAC Workshop on Computer-Aided Verification, June 1990.
J. Burch, E. Clarke, and D. Long. Symbolic model checking with partitioned transition relations. In Proc. of International Conference on VLSI, 1991.
C.-T. Chou. The mathematical foundation of symbolic trajectory evaluation. In CAV’1999, July 1999.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999.
O. Coudert, J. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In Proc. of CAV’90, pages 23–32, 1990.
S. Hazelhurst and C.-J. Seger. A simple theorem prover based on symbolic trajectory evaluation and OBDDs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 14(4):413–422, April 1995.
S. Hazelhurst and C.-J. Seger. Model checking lattices: Using and reasoning about information orders for abstraction. Logic Journal of the IGPL, Volume 7:375–411, May 1999.
R. Hojati, S. Krishnan, and R. Brayton. Early quantification and partitioned transition relations. In Proc. of the 1996ICCAD, pages 12–19, 1996.
A. Jain. Formal Hardware Verification by Symbolic Trajectory Evaluation. PhD thesis, ECE, Carnegie-Mellon University, August 1997.
K. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.
J. O’Leary, X. Zhao, R. Gerth, and C.-J. Seger. Formally verifying ieee compliance of floating-point hardware. Intel Technology Journal, Q1: 147–190, 1999.
M. Pandey and R. Bryant. Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(7):918–935, July 1999.
M. Pandey, R. Raimi, D. Beatty, and R. Bryant. Formal verification of PowerPC(TM) arrays using symbolic trajectory evaluation. In Proceedings of the 33rd DAC, pages 649–654, June 1996.
M. Pandey, R. Raimi, D. Beatty, R. Bryant, and M. Abadir. Formal verification of content addressable memories using symbolic trajectory evaluation. In Proceedings of the 34th DAC, June 1997.
C.-J. Seger and R. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6(2): 147–190, March 1995.
J. Yang. Generalized symbolic trajectory evaluation. STE Symposium, CAV’2000, 2000.
J. Yang and C.-J. Seger. Generalized symbolic trajectory evaluation. Intel SCL Technical Report (submitted for journal publication), 2000.
J. Yang and C.-J. Seger. Introduction to generalized symbolic trajectory evaluation. In Proc. ofICCD, September 2001.
J. Yang and A. Tiemeyer. Lazy symbolic model checking. In DAC’00, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, J., Seger, CJ.H. (2002). Generalized Symbolic Trajectory Evaluation — Abstraction in Action. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_5
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive