The synthesis of cyclic dependencies with boolean satisfiability

John D. Backes, Marc D. Riedel

Research output: Contribution to journalArticlepeer-review

8 Scopus citations


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.

Original languageEnglish (US)
Article number44
JournalACM Transactions on Design Automation of Electronic Systems
Issue number4
StatePublished - Oct 1 2012


  • Boolean satisfiability
  • Circuit verification
  • Cyclic circuits
  • Logic design
  • Logic synthesis


Dive into the research topics of 'The synthesis of cyclic dependencies with boolean satisfiability'. Together they form a unique fingerprint.

Cite this