A Satisfiability Based Method to Analyze Combinationality of Cyclic Circuits

The combinationality of cyclic circuits is important, both for converting undesirable cyclic circuits into their acyclic counterparts, and for synthesizing cyclic circuits to harness their benefits in area and timing. This paper introduces a novel methodology that employs computational Boolean algebra to model cyclic circuits and reformulates the combinationality issue as a satisfiability (SAT) problem. In experimental evaluations encompassing thousands of cyclic circuits with millions of gates, the proposed technique demonstrated remarkable efficiency, requiring merely approximately 2 seconds of CPU time to find all cyclic circuits and ascertain their combinationality, showing its viability for practical applications.