Treffer: Reasoning about GSTE assertion graphs

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 temporallogic 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 V-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.