Generalized Symbolic Trajectory Evaluation

Jin Yang

Abstract

Symbolic trajectory evaluation (STE) is a lattice-based model checking technology based on a form of symbolic simulation. It offers an alternative to `classical' symbolic model checking that, within its domain of applicability, often is easier to use and less sensitive to state explosion. In particular, STE has shown great potential in verifying medium to large scale hardware design with a high degree of automation, and have been in active use in Intel, IBM and Motorola. The main criticism, however, is the limited expressiveness of its specification language, i.e. it only allows properties over finite time intervals.

In this talk, we present a theory of generalized STE (GSTE). The most important contribution of this work is the generalization of STE-style model checking to all $\omega$-regular properties while maintaining the same space efficiency and comparable time efficiency. We first present a specification language called {\it assertion graphs} as a generalization of the STE specification language. We propose three levels of semantics for assertion graphs, each of which defines an expressiveness class for specifications. We then gradually generalize the STE-style model checking algorithm and develop a simulation based model checking algorithm for each of the three expressiveness classes with increasing time complexities. Finally, we clarify the role of abstract interpretation in the (G)STE theory and show how to model check assertion graphs using abstraction. At the end, we demonstrate the strength and practicality of GSTE through a case study of memory verification.