A Light-Weight Framework for Hardware Verification

ID
TR-99-01
Authors
Christoph Kern, Tarik Ono-Tesfaye and Mark R. Greenstreet
Publishing date
February 24, 1999
Length
15 pages
Abstract
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.