檢測功能性(functionality) 和組合性(combinationality) 是處理迴路化組合電路的兩大議題。在所有輸入組合下，如果電路所有輸出端的值皆為固定且唯一，則此電路便是組合電路。而在驗證電路功能性之前，我們必須先檢測組合電路在經過迴路化之後，是否仍保有組合性。此篇論文提出兩階段驗證演算法，驗證迴路化電路的組合性。我們利用IWLS 2005之測試電路進行實驗，演示整個驗證方法之效能。與目前最新的驗證方法比較之後，我們的演算法平均加速超過4000倍以上。

Functionality and combinationality are two main issues that have to be dealt with in cyclic combinational circuits, which are combinational circuits containing loops.
Cyclic circuits are combinational if nodes within the circuits are denite values under all input assignments. For a cyclied circuit, we have to check whether it is combinational or not. Thus, this paper proposes an ecient two-stage algorithm to verify the combinationality of cyclic circuits. A set of cyclied IWLS 2005 benchmarks are
performed to demonstrate the eciency of the proposed algorithm. Compared to the state-of-the-art algorithm, our approach has a speedup of about 4000 times on average.

中文摘要
Abstract
Acknowledgement
Contents
List of Tables
List of Figures
1 Introduction
2 Preliminaries
3 The Algorithm
3.1 Combinationality
3.2 Self-conflict Side Inputs
3.3 Loop Backtracking
3.4 Proposed Flow
4 Experimental Results
5 Conclusion

[1] 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.
[2] J. Backes and M. D. Riedel, “The synthesis of cyclic dependencies with Craig interpolation,” in Proc. International Workshop on Logic and Synthesis, 2009, pp. 24–30.
[3] 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.
[4] Berkeley Logic Synthesis and Verificaiton Group. ABC: A System for Sequential Synthesis and Verification. [Online]. Available: http://www.eecs.berkeley.edu/∼alanmi/abc
[5] J.-H. Chen, “Making combinational circuit cyclic by identifying opportunities for introducing loops,” Master thesis, National Tsing Hua University, Taiwan,2013
[6] Y.-C. Chen and C.-Y. Wang, “Fast detection of node mergers using logic impli- cations,” in Proc. International Conference on Computer-Aided Design, 2009, pp. 785–788.
[7] 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.
[8] E. Craig, “Mathematical techniques in electronics and engineering analysis,” in Proc. of the IEEE, vol. 52, no. 11, pp. 1390–1390, 1964.
[9] S. Edwards, “Making cyclic circuits acyclic,” in Proc. Design Automation Con- ference, 2003, pp. 159–162.
[10] IWLS 2005 Benchmarks. [Online]. Available: http://iwls.org/iwls2005/benchmarks.html
[11] D. B. Johnson, “Finding all the elementary circuits of a directed graph,” SIAM J. Comput., vol. 4, no. 1, pp. 77–84, 1975.
[12] 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.
[13] O. Neiroukh, S. Edwards, and X. Song, “Transforming cyclic circuits into acyclic equivalents,” IEEE Trans. Computer-Aided Design of Integrated Cir- cuits and Systems, vol. 27, no. 10, pp. 1775–1787, 2008.
[14] M. D. Riedel and J. Bruck, “The synthesis of cyclic combinational circuits,” in Proc. Design Automation Conference, 2003, pp. 163–168.
[15] M. D. Riedel and J. Bruck, “Cyclic combinational circuits: Analysis for syn- thesis,” in Proc. International Workshop on Logic and Synthesis, 2003, pp.
105–112.
[16] M. D. Riedel and J. Bruck, “Timing analysis of cyclic combinational circuits,”in Proc. International Workshop on Logic and Synthesis, 2004, pp. 69–77.
[17] R. L. Rivest, “The necessity of feedback in minimal monotone combinational circuits,” IEEE Trans. Computers, vol. C-26, no. 6, pp. 606–607, 1977.
[18] G. S. Tseitin, “On the complexity of derivation in propositional calculus,” in Automation of Reasoning. Springer, 1983, pp. 466–483.