Partial equivalence checking for combinational circuits

This paper suggests an algorithm for partial equivalence checking for combinational circuit with its specification. The algorithm is based on the intersection operations of single-root ROBDDs of multi-output sub-circuits, which depend on both the input and output variables of sub-circuits, as well as only the output variables of these sub-circuits. To provide fault detection within the sub-circuits that are parts of more complicate combinational circuit, an algorithm for generating test patterns depending on the input variables of the combinational circuit has been developed. The approach proposed eliminates the need for the necessity of employing Quantified Boolean Function (QBF) solvers or their modifications, which obviously entails more complex calculations than those associated with operations on ROBDDs. Contribution of the authors: the authors contributed equally to this article. The authors declare no conflicts of interests.

Keywords

Authors

References