Abstract
Prior works showed great opportunities to achieve more minimized combinational circuits by introducing combinational feedback loops during the synthesis process. However, they achieved this by exploring possible cyclic dependencies of circuits in a branch-and-bound manner, which may not scale well for complex designs. Instead of exploration, this paper proposes a formal algorithm using logic implication to directly identify, or more aggressively create cyclifiable structure candidates in circuits by merging nodes. Additionally, to validate whether the formed loops are combinational, we also propose an efficient SAT-based algorithm. The effectiveness and scalability of the identification and validation algorithms are demonstrated in the experimental results performed on a set of IWLS 2005 benchmarks. As compared to the state-of-the-art, the validation algorithm has an average speedup of 354.94 times.