Generating monitor circuits for simulation-friendly GSTE assertion graphs

Formal and dynamic (simulation, emulation, etc.) verification techniques are both needed to deal with the overall challenge of verification. Ideally, the same specification/testbench would work with both formal and dynamic techniques, with the same semantics in both. Unfortunately, this is typically not the case. In particular, generalized symbolic trajectory evaluation (GSTE) is a powerful formal verification technique developed by Intel and successfully used on next-generation microprocessor designs, but the specification formalism for GSTE relies on "symbolic constants", which intrinsically exploit the underlying formal verification engine and cannot be reasonably handled via non-symbolic means. In this paper, we propose a modified version of GSTE specifications, and we present efficient, automatic constructions to convert from the new simulation-friendly GSTE specifications into the conventional GSTE specifications (to access the formal verification tool flow) as well as into completely non-symbolic monitor circuits suitable for the conventional dynamic verification. We demonstrate empirically that our simulation-friendly specification style is expressive enough for almost all real GSTE specifications, that our monitor construction is linear-size, and that our monitor construction imposes minimal overhead over a previously published monitor construction that was not fully non-symbolic.