Abstract
Generalized symbolic trajectory evaluation (GSTE) is a new model-checking approach that combines the industrially-proven scalability and capacity of classical symbolic trajectory evaluation with the expressive power of temporal-logic model checking. GSTE was originally developed at Intel and has been used successfully on Intel’s next-generation microprocessors. However, the supporting theory and algorithms for GSTE are still immature. In particular, GSTE specifications are given as assertion graphs, a variety of ∀-automata, and although an efficient model-checking algorithm exists to verify whether a circuit model obeys a specification assertion graph, there is no work on reasoning about assertion graphs themselves. This paper presents new algorithms to leverage GSTE model checking to efficiently decide whether one assertion graph implies another, and to model check one assertion graph under the assumption that another is true (under regular GSTE acceptance conditions). These two operations — deciding whether one specification implies another and verifying under an assumption — are the fundamental building blocks of compositional verification and any higher-level reasoning about model-checking results, so the algorithms presented here are key steps to using GSTE in a broader verification framework. Preliminary experimental results applying our algorithms to real, industrial circuits and specifications show that our algorithms are useful in practice.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aagaard, M., Jones, R.B., Seger, C.-J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: 35th Design Automation Conference, pp. 538–541. ACM/IEEE (1998)
Amla, N., Allen Emerson, E., Namjoshi, K.S.: Efficient decompositional modelchecking for regular timing diagrams. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 67–81. Springer, Heidelberg (1999)
Bentley, B.: High level validation of next generation microprocessors. In: International Workshop on High-Level Design, Validation, and Test, IEEE, Los Alamitos (2002)
Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 454–464. Springer, Heidelberg (2001)
Clarke, E.M., Allen Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Hu, A.J., Casas, J., Yang, J.: Efficient generation of monitor circuits for GSTE assertion graphs. In: International Conference on Computer-Aided Design, IEEE/ACM (2003) (to appear)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by ∀-automata. In: Symposium on Principles of Programming Languages, pp. 1–12. ACM, New York (1987)
Nelson, K.L., Jain, A., Bryant, R.E.: Formal verification of a superscalar execution unit. In: 34th Design Automation Conference, pp. 161–166. ACM/IEEE (1997)
Oliveira, M.T., Hu, A.J.: High-level specification and automatic generation of IP interface monitors. In: 39th Design Automation Conference, pp. 129–134. ACM/IEEE (2002)
Pandey, M., Raimi, R., Beatty, D.L., Bryant, R.E.: Formal verification of PowerPC arrays using symbolic trajecory evaluation. In: 33rd Design Automation Conference, pp. 649–654. ACM/IEEE (1996)
Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Raymond, P.: Recognizing regular expressions by means of dataflow networks. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 336–347. Springer, Heidelberg (1996)
Seawright, A., Brewer, F.: High-level symbolic construction techniques for high performance sequential synthesis. In: 30th Design Automation Conference, pp. 424–428. ACM/IEEE (1993)
Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6(2), 147–190 (1995)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science, pp. 332–344. IEEE Computer Society, Los Alamitos (1986)
Yang, J., Goel, A.: GSTE through a case study. In: International Conference on Computer-Aided Design, pp. 534–541. IEEE/ACM (2002)
Yang, J., Seger, C.-J.H.: Introduction to generalized symbolic trajectory evaluation. In: International Conference on Computer Design, pp. 360–365. IEEE, Los Alamitos (2001)
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, pp. 70–87. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hu, A.J., Casas, J., Yang, J. (2003). Reasoning about GSTE Assertion Graphs. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive