Tightly integrate dynamic verification with formal verification: a GSTE based approach
Jin Seok Yang, A. Puder · Proceedings of the ASP-DAC 2005. Asia and South Pacific Design Automation Conference, 2005. · 2005
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.