SAT-based combinational and sequential dependency computation

Abstract

We present an algorithm for computing both functional dependency and unateness of combinational and sequential Boolean functions represented as logic networks. The algorithm uses SAT-based techniques from Combinational Equivalence Checking (CEC) and Automatic Test Pattern Generation (ATPG) to compute the dependency matrix of multi-output Boolean functions. Additionally, the classical dependency definitions are extended to sequential functions and a fast approximation is presented to efficiently yield a sequential dependency matrix. Extensive experiments show the applicability of the methods and the improved robustness compared to existing approaches.