Generating Monitor Circuits for Simulation-Friendly GSTE Assertion Graphs Kelvin Ng, Alan J. Hu, and Jin Yang IEEE International Conference on Computer Design, IEEE Computer Society Press, 2004, pp. 488-492. 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 conventional GSTE specifications (to access the formal verification tool flow) as well as into completely non-symbolic monitor circuits suitable for 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.