UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Generating dynamic verification tools for generalized symbolic trajectory evaluation (GSTE) Ng, Kelvin Kwok Cheung

Abstract

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.

Item Media

Item Citations and Data

License

For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

Usage Statistics