Tightly integrate dynamic verification with formal verification: a GSTE based approach

GSTE (generalized symbolic trajectory evaluation) is a high capacity formal verification technology that has been successfully applied to verifying complex Intel designs with tens of thousands of state elements. In this paper, we extend the use of GSTE by developing a dynamic checker that verifies a GSTE specification against a scalar simulation trace. Unlike previous approaches, both the formal checker and the dynamic checker work directly on a GSTE specification without the need for an intermediate monitor circuit. Our approach also offers a straight forward way to measure the quality (coverage) of a specification. The dynamic checker has been used in the real-life microprocessor design verification.