The synthesis of cyclic dependencies with boolean satisfiability

The accepted wisdom is that combinational circuits must have acyclic (i.e., feed-forward) topologies. Yet simple examples suggest that this is incorrect. In fact, introducing cycles (i.e., feedback) into combinational designs can lead to significant savings in area and in delay. Prior work described methodologies for synthesizing cyclic circuits with Sum-Of-Product (SOP) and Binary-Decision Diagram (BDD)-based formulations. Recently, techniques for analyzing and mapping cyclic circuits based on Boolean satisfiability (SAT) were proposed. This article presents a SAT-based methodology for synthesizing cyclic dependencies. The strategy is to generate cyclic functional dependencies through a technique called Craig interpolation. Given a choice of different functional dependencies, a branch-and-bound search is performed to pick the best one. Experiments on benchmark circuits demonstrate the effectiveness of the approach.