Generating dynamic verification tools for generalized symbolic trajectory evaluation (GSTE)
Kelvin Ng · cIRcle (University of British Columbia) · 2009
Formal and dynamic (simulation, emulation, etc.) verification techniques are both needed to deal with the overall challenge of verification. Unfortunately, the same specification does not always work with both techniques. 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 thesis, I propose a modified version of GSTE specifications and 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 monitor circuits suitable for conventional dynamic verification. I also investigate the construction from the monitor circuits into testbench generator circuits. I implemented the proposed constructions to demonstrate that my approach is practical and efficient.