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 simulationfriendly GSTE specifications into conventional GSTE specifications (to access the formal verification tool flow) as well ...

• Type: Conference
• Year: 2004
• Where: ICCD
• Authors: Kelvin Ng, Alan J. Hu, Jin Yang
• Keywords: Hardware, ICCD 2004, Monitor Circuits, Monitor Construction, Symbolic Trajectory Evaluation