The Analysis of Cyclic Circuits with Boolean Satisfiability

J. Backes, B. Fett, M. Riedel

Proceedings of the International Conference on Computer-Aided Design, San Jose, CA. 2008

The accepted wisdom is that combinational circuits must have acyclic (i.e., loop-free or feed-forward) topologies. And yet simple examples suggest that this need not be so. In previous work, we advocated the design of cyclic combinational circuits (i.e., circuits with loops or feedback paths). We proposed a methodology for synthesizing such circuits and demonstrated that it produces significant improvements in area and in delay. The analysis method that we used to validate cyclic circuits was based on binary decision diagrams. In this paper, we propose a much more efficient technique for analysis based on Boolean satisfiability (SAT).