The completeness of a hardware inference system

Abstract

Symbolic trajectory evaluation (STE) is a method for efficient circuit verification [1]. In [2] a set of inference rules was introduced for combining STE results. These inference rules were also proven sound. In this paper we show that, with one additional inference rule, the inference system is complete. Here, complete means that any formula A ⇒ C, that is valid in every model satisfying some collection 9 of STE assertions, can be derived from Φ by a finite applications of the inference rules. The completeness proof is based on the method of model construction- given Φ, a most general circuit model (in which every assertion in Φ holds) can be generated.