Introduction to generalized symbolic trajectory evaluation

Symbolic trajectory evaluation (STE) is a lattice-based model checking technology that uses a form of symbolic simulation. It offers an alternative to ʹclassicalʹ symbolic model checking that, within its domain of applicability, often is much easier to use and much less sensitive to state explosion. The limitation of STE, however, is that it can only express and verify properties over finite time intervals. In this paper, we present a generalized STE (GSTE) that extends STE style model checking to properties over infinite time intervals. We further strengthen the power of GSTE by introducing a form of backward symbolic simulation. It can be shown that these extensions together with a notion of fairness give STE the power to verify all (omega)-regular properties. The generalization also gives one the power to choose and adjust the level of model abstraction in a verification effort. We shall use a large-scale industrial memory design to demonstrate the strength and practicality of GSTE.