Technical Reports

The ICICS/CS Reading Room

UBC CS TR-99-01 Summary

A Light-Weight Framework for Hardware Verification, February 24, 1999 Christoph Kern, Tarik Ono-Tesfaye and Mark R. Greenstreet, 15 pages

We present a deductive verification framework that combines deductive reasoning, general purpose decision procedures, and domain-specific reasoning. We address the integration of formal as well as informal domain-specific reasoning, which is encapsulated in the form of user-defined inference rules. To demonstrate our approach, we describe the verification of a SRT divider where a transistor-level implementation with timing is shown to be a refinement of its high-level specification.

If you have any questions or comments regarding this page please send mail to