Abstract
Generalized symbolic trajectory evaluation (GSTE) is an extension of symbolic trajectory evaluation (STE). In GSTE, assertion graphs are used to specify properties in a special form of regular automata with antecedent and consequent pairs. This paper presents a new model characterization, called maximal models, for an assertion graph with important properties. Besides their own theoretical significance, maximal models are used to show the implication of two assertion graphs in GSTE. We show that, contrary to the general belief, an assertion graph may have more than one maximal model. We present a provable algorithm to find all maximal models of a linear assertion graph. We devise an algorithm for finding a maximal model for an arbitrary assertion graph.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Yang, J., Seger, C.: Generalized Symbolic Trajectory Evaluation. Technical Report, Intel (2002)
Yang, J., Seger, C.: Introduction to Generalized Symbolic Trajectory Evaluation. IEEE Trans on VLSI Systems 11(3), 345–353 (2003)
Hu, A.J., Casas, J., Yang, J.: Efficient Generation of Monitor Circuits for GSTE Assertion Graphs. In: IEEE/ACM International Conference on Computer-Aided Design, pp. 154–159 (2003)
Hu, A.J., Casas, J., Yang, J.: Reasoning about GSTE Assertion Graphs. In: 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), pp. 170–184 (2003)
Seger, C., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6(2), 147–190 (1995)
Yang, G., Yang, J., Song, X.: Formal Verification by Generalized Symbolic Trajectory Evaluation. Technical Report, Portland State University (2004)
Chou, C.-T.: The mathematical foundation of synmbolic trajectory evaluation. In: Proc. Computer-aided Verifucation(CAV), pp. 196–207 (1999)
Bentley, B.: High level validation of next generation microprocessors. In: Proc. IEEE High Level Design Validation and Test Workshop (HLDVT), pp. 31–35 (2002)
Aagaard, M., Jones, R.B., Seger, C.: Combining thereom proving and trajectoy evaluaton in an industrial environment. In: 35th Design Automation Conferece, pp. 538–541. ACM/IEEE (1998)
Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In: Computer-Aided Verification: 13th International Conferece, pp. 454–464.
Nelson, K.L., Jain, A., Bryant, R.E.: Formal verification of a superscalar execution unit. In: 34th Design Automation Conferece, ACM/IEEE, pp. 161–167 (1997)
Pandey, M., Raimi, R., Beatty, D.L., Bryant, R.E.: Formal verification of PowerPC arrays using symbolic trajectory evluation. In: 33rd Design Automation Confer-ence, pp. 649–654. ACM/IEEE (1996)
Clarke, E.M., Allen Emerson, E.: Design and synthesis of synchronization skele-tons using branching time temporal logic. In: Kozen, D. (ed.) Workshop, on Logics of Programs, May, pp. 52–71 (1981)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The automata-Theorotic Approach. Princeton University Press, Princeton (1994)
Yang, G., Yang, J., Hung, W.N.N., Song, X.: Implication of assertion graphs in GSTE,ASPDAC, pp. 1060–1063 (2005)
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
Yang, G., Yang, J., Song, X., Xie, F. (2006). Maximal Models of Assertion Graph in GSTE. In: Cai, JY., Cooper, S.B., Li, A. (eds) Theory and Applications of Models of Computation. TAMC 2006. Lecture Notes in Computer Science, vol 3959. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11750321_64
Download citation
DOI: https://doi.org/10.1007/11750321_64
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34021-8
Online ISBN: 978-3-540-34022-5
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
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.
