Abstract
Symbolic Trajectory Evaluation (STE) is a powerful technique for model checking. It is based on 3-valued symbolic simulation, using 0,1 and X (”unknown”). The X value is used to abstract away parts of the circuit. The abstraction is derived from the user’s specification. Currently the process of abstraction and refinement in STE is performed manually. This paper presents an automatic refinement technique for STE. The technique is based on a clever selection of constraints that are added to the specification so that on the one hand the semantics of the original specification is preserved, and on the other hand, the part of the state space in which the ”unknown” result is received is significantly decreased or totally eliminated. In addition, this paper raises the problem of vacuity of passed and failed specifications. This problem was never discussed in the framework of STE. We describe when an STE specification may vacuously pass or fail, and propose a method for vacuity detection in STE.
Chapter PDF
Similar content being viewed by others
References
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Chou, C.-T.: The mathematical foundation of symbolic trajectory evaluation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 196–207. Springer, Heidelberg (1999)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counter example-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Hazelhurst, S., Seger, C.-J.H.: Model checking lattices: Using and reasoning about information orders for abstraction. Logic journal of IGPL 7(3) (1999)
Kurshan, R.P.: Computer-Aided Verification of coordinating processes - the automata theoretic approach (1994)
Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: DAC (1997)
Roorda, J.-W., Claessen, K.: A new SAT-based algorithm for symbolic trajectory evaluation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 238–253. Springer, Heidelberg (2005)
Roorda, J.-W., Claessen, K.: SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 175–189. Springer, Heidelberg (2006)
Schubert, T.: High level formal verification of next-generation microprocessors. In: DAC 2003 (2003)
Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6(2) (1995)
Seger, C.-J.H., Jones, R.B., O’Leary, J.W., Melham, T.F., Aagaard, M., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 24(9) (2005)
Tzoref, R.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. Master’s thesis, Department of Computer Science, Technion, Israel (2006)
Wile, B., Roesner, W., Goss, J.: Comprehensive Functional Verification: The Complete Industry Cycle. Morgan Kaufmann, San Francisco (2005)
Wilson, J.C.: Symbolic Simulation Using Automatic Abstraction of Internal Node Values. PhD thesis, Stanford University, Dept. of Electrical Engineering (2001)
Yang, J., Gil, R., Singerman, E.: satGSTE: Combining the abstraction of GSTE with the capacity of a SAT solver. In: DCC (2004)
Yang, J., Goel, A.: GSTE through a case study. In: ICCAD (2002)
Yang, J., Seger, C.-J.H.: Generalized symbolic trajectory evaluation - abstraction in action. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)
Yang, J., Seger, C.-J.H.: Introduction to generalized symbolic trajectory evaluation. IEEE Trans. Very Large Scale Integr. Syst. 11(3) (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tzoref, R., Grumberg, O. (2006). Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_20
Download citation
DOI: https://doi.org/10.1007/11817963_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)