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.
CITATION STYLE
Zhu, Z., & Seger, C. J. (1994). The completeness of a hardware inference system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 818 LNCS, pp. 286–298). Springer Verlag. https://doi.org/10.1007/3-540-58179-0_62
Mendeley helps you to discover research relevant for your work.