Open Collections

Generating dynamic verification tools for generalized symbolic trajectory evaluation (GSTE)

University of British Columbia

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.

Thesis/Dissertation

application/pdf

2009-11-25

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.

http://hdl.handle.net/2429/15772

Computer Science

University of British Columbia

UBCV

DSpace