Exploiting Incrementality in SAT-based Search for Multiple Equivalence-Preserving Transformations in Combinational Circuits

This paper introduces an approach to effectively exploit incremental SAT in order to search for multiple equivalence-preserving transformations of combinational circuits. Typical applications such as redundancy removal with observability and external care conditions, adequate abstractions and other optimizations used in a state-of-the-art SAT-based model checker, can reap benefits from the proposed strategies. Our techniques exploit SAT incrementality, by iteratively refining the set of candidate transformations with a counter-example driven analysis, until an unsatisfiable point is reached. The key point of our technique is the ability to address satisfiable instances first, where SAT solvers are generally much faster than with unsatisfiable runs. We also discuss partitioning and problem reduction issues, that are fundamental in order to provide a scalable approach. Experimental results show the effectiveness of the proposed strategies.