Synthesis and verification of cyclic combinational circuits

Prior works have demonstrated opportunities for achieving more minimized combinational circuits by introducing combinational loops during the synthesis. However, they achieved this by using a branch-and-bound technique to explore possible cyclic dependencies of circuits, which may not scale well for complex designs. Instead of using exploration, this paper proposes a formal algorithm using logic implication to identify cyclifiable structure candidates directly, or to create them aggressively in circuits. Additionally, we also propose a SAT-based algorithm to validate whether the formed loops are combinational or not. 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 algorithm, our validation algorithm produces speedups ranging from 2 to 2350 times.