A light-weight framework for hardware verification

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.