A SAT-based implication engine for efficient ATPG, equivalence checking, and optimization of netlists
Paul Tafertshofer, Andreas Ganz, M. Henftling · 1997
This paper presents a flexible and efficient approach to evaluating implications as well as deriving indirect implications in logic circuits. Evaluation and derivation of implications are essential in ATPG, equivalence checking, and netlist optimization. Contrary to other methods, our approach is based on a graph model of a circuit's clause description called implication graph. It combines both the flexibility of SAT-based techniques and high efficiency of structure based methods. As the proposed algorithms operate only on the implication graph, they are independent of the chosen logic. Evaluation of implications and computation of indirect implications are performed by simple and efficient graph algorithms. Experimental results for various applications relying on implication demonstrate the effectiveness of our approach. 1 Introduction Recently, substantial progress has been achieved in the fields of Boolean equivalence checking and optimization of netlists. Techniques for deriving ...