Reasoning about GSTE Assertion Graphs

Alan J. Hu, Jeremy Casas, and Jin Yang

12th IFIP WG10.5 Advanced Research Working Conference on
Correct Hardware Design and Verification Methods (CHARME),
LNCS Volume 2860, Springer, 2003, pp. 170-184.

{\it 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 {\it assertion graphs}, a variety of
$\forall$-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.