之前的作品展現出我們有很大的機會，可以透過在電路合成過程中加入組合反饋迴路 (Combinational Feedback Loops) 來實現更加最小化的組合電路。
然而，他們實現這項技術的方式是藉由分支界定 (branch-and-bound) 的方法探索電路中可能存在的循環依賴關係，但是這樣的方法可能不足以應付複雜的電路設計。
有別於這樣的探索方式，本文提出了一個正規的邏輯推論的演算法，藉由合併電路節點的方法來直接識別，或者更積極的創造出迴路化的電路架構。
此外，為了驗證所形成迴路是否為組合電路，我們也提出了一個以可滿足性問題為基底 (SAT-based) 的演算法來有效率地做驗證。
我們藉由在IWLS 2005 的測試電路上所進行的實驗結果，來呈現我們所提出的識別演算法的有效性和可擴展性。
與目前最新的演算法比較起來，我們的驗證演算法平均加速了354.94倍。

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.

[1] M. Abadir, J. Ferguson, and T. Kirkland, “Logic design verification
via test generation,” IEEE Trans. Computer-Aided Design of Integrated
Circuits and Systems, vol. 7, no. 1, pp. 138–148, 1988.
[2] J. Backes, B. Fett, and M. D. Riedel, “The analysis of cyclic circuits
with Boolean satisfiability,” in Proc. International Conference on
Computer-Aided Design, 2008, pp. 143–148.
[3] J. Backes and M. D. Riedel, “The synthesis of cyclic dependencies
with Craig interpolation,” in Proc. International Workshop on Logic
and Synthesis, 2009.
[4] J. Backes and M. D. Riedel, “Reduction of interpolants for logic synthesis,”
in Proc. International Conference on Computer-Aided Design,
2010, pp. 602–609.
[5] J. Backes and M. D. Riedel, “The synthesis of cyclic dependencies with
Boolean satisfiability,” ACM Trans. Des. Autom. Electron. Syst., vol. 17,
pp. 44:1–44:24, 2012.
[6] Berkeley Logic Synthesis and Verificaiton Group. ABC: A System
for Sequential Synthesis and Verification. [Online]. Available:
http://www.eecs.berkeley.edu/~alanmi/abc
[7] Y.-C. Chen and C.-Y. Wang, “Fast detection of node mergers using
logic implications,” in Proc. International Conference on Computer-
Aided Design, 2009, pp. 785–788.
[8] Y.-C. Chen and C.-Y. Wang, “Fast node merging with don’t cares using
logic implications,” IEEE Trans. Computer-Aided Design of Integrated
Circuits and Systems, vol. 29, no. 11, pp. 1827–1832, 2010.
[9] E. Craig, “Mathematical techniques in electronics and engineering
analysis,” in Proc. of the IEEE, vol. 52, no. 11, pp. 1390–1390, 1964.
[10] S. Edwards, “Making cyclic circuits acyclic,” in Proc. Design Automation
Conference, 2003, pp. 159–162.
[11] L. Hellerman, “A catalog of three-variable or-invert and and-invert
logical circuits,” IEEE Trans. Electronic Computers, vol. EC-12, no. 3,
pp. 198–223, 1963.
[12] Y.-C. Hsu, S. Sun, and D.-C. Du, “Finding the longest simple path
in cyclic combinational circuits,” in Proc. International Conference on
Computer Design, 1998, pp. 530–535.
[13] IWLS 2005 Benchmarks. [Online]. Available: http://iwls.org/iwls2005/
benchmarks.html
[14] J.-H. Jiang, A. Mishchenko, and R. Brayton, “On breakable cyclic
definitions,” in Proc. International Conference on Computer Aided
Design, 2004, pp. 411–418.
[15] W. H. Kautz, “The necessity of closed circuit loops in minimal
combinational circuits,” IEEE Trans. Computers, vol. C-19, no. 2, pp.
162–164, 1970.
[16] T. Kirkland and M. Mercer, “A topological search algorithm for ATPG,”
in Proc. Design Automation Conference, 1987, pp. 502–508.
[17] W. Kunz and D. Pradhan, “Recursive learning: a new implication
technique for efficient solutions to CAD problems-test, verification,
and optimization,” IEEE Trans. Computer-Aided Design of Integrated
Circuits and Systems, vol. 13, no. 9, pp. 1143–1158, 1994.
[18] S. Malik, “Analysis of cyclic combinational circuits,” IEEE Trans.
Computer-Aided Design of Integrated Circuits and Systems, vol. 13,
no. 7, pp. 950–956, 1994.
[19] A. Mishchenko, S. Chatterjee, and R. Brayton, “DAG-aware AIG
rewriting: a fresh look at combinational logic synthesis,” in Proc. Design
Automation Conference, 2006, pp. 532–535.
[20] O. Neiroukh, S. Edwards, and X. Song, “Transforming cyclic circuits
into acyclic equivalents,” IEEE Trans. Computer-Aided Design of Integrated
Circuits and Systems, vol. 27, no. 10, pp. 1775–1787, 2008.
[21] A. Raghunathan, P. Ashar, and S. Malik, “Test generation for cyclic
combinational circuits,” in Proc. International Conference on VLSI
Design, 1995, pp. 104–109.
[22] M. D. Riedel and J. Bruck, “The synthesis of cyclic combinational
circuits,” in Proc. Design Automation Conference, 2003, pp. 163–168.
[23] M. D. Riedel and J. Bruck, “Cyclic combinational circuits: Analysis
for synthesis,” in Proc. International Workshop on Logic and Synthesis,
2003, pp. 105–112.
[24] M. D. Riedel and J. Bruck, “Timing analysis of cyclic combinational
circuits,” in Proc. International Workshop on Logic and Synthesis, 2004,
pp. 69–77.
[25] R. L. Rivest, “The necessity of feedback in minimal monotone combinational
circuits,” IEEE Trans. Computers, vol. C-26, no. 6, pp. 606–607,
1977.
[26] M. Schulz and E. Auth, “Advanced automatic test pattern generation
and redundancy identification techniques,” in Proc. International Fault-
Tolerant Computing Symposium, 1988, pp. 30–35.
[27] T. Shiple, G. Berry, and H. Touati, “Constructive analysis of cyclic
circuits,” in Proc. European Design and Test Conference, 1996, pp.
328–333.
[28] L. Stok, “False loops through resource sharing,” in Proc. International
Conference on Computer-Aided Design, 1992, pp. 345–348.