江介宏Jiang, Jie-Hong臺灣大學:電子工程學研究所陳一心Chen, I-HsinI-HsinChen2010-07-142018-07-102010-07-142018-07-102009U0001-1908200900510800http://ntur.lib.ntu.edu.tw//handle/246246/189190　近年來在邏輯合成與驗證的領域中，內插法的應用與日俱增，相關範疇包括函數相依、二元分解、亞氏分解等。本研究係利用內插法針對多層次電路之節點計算邏輯無關項。傳統上，內插可藉由可滿足性問題求解器產生之反證求得，並可利用改寫反證之結構對內插大小進行調整。但我們在研究過程發現，大部分狀況中，調整可滿足性問題求解器產生反證後所求得之內插並無太大的改變，內插法的效能因而受限。本論文中，我們提出利用可滿足性問題求解之演算法來計算邏輯無關項，並發展出一套針對可滿足性問題求解器改變內插大小的技巧，包括調整初始變數優先序及改變布林初始值，同時利用電路結構簡化問題模型以加快求解速度。實驗結果顯示，該改變內插大小的方法讓求解邏輯無關項之演算法在可接受的時間內，較未使用該方法時求出更多的邏輯無關項。In recent years, there have been a variety of applications of interpolation in logic synthesis and verification, such as functional dependency, bi-decomposition, and Ashenhurst decomposition. The goal of this research is to compute don’t-cares for a given node in a multi-level network by using interpolation. Traditionally, an interpolant can be derived from a refutation proof given by a SAT solver, and its onset can be adjusted via rewriting the structure of the refutation proof. However, in most cases, the interpolant derived by the refutation proof generated by a SAT solver can not be adjusted too much. As a result, the application of interpolation is limited. In this thesis, we propose SAT-based don’t-care computation algorithms via interpolation. In addition, a set of techniques has been developed for a SAT solver to adjust the solution space of the interpolant. The methods include setting the initial variable activities and altering the Boolean initial values. The circuit structure has also been utilized to simplify the problem to accelerate SAT solving. Experiments show that the algorithms can get more don’t-cares while applying the interpolation sizing method to the algorithms.Acknowledgements i要 iibstract iiiontents ivist of Figures viist of Tables viiihapter 1 Introduction 1.1 The Origin of Don’t-Cares 1.2 Previous Work 3.3 Our Contributions 5.4 Organization of the Thesis 6hapter 2 Preliminaries 7.1 Boolean Network and Function 7.2 Satisfiability Problem and Solver 8.3 Resolution and Refutation Proof 9.4 Craig Interpolation Theorem 10.4.1 Interpolant Strengthen 12.5 Circuit to CNF Conversion 14hapter 3 Don’t-Care Computation Algorithms 15.1 CDC Computation Method 1 (CDCC1) 16.2 CDC Computation Method 2 (CDCC2) 18.3 CNF Simplification 20.4 Adjustable Interpolation 21.4.1 Swap Rules 21.4.2 Initial Variable Activities 26.4.3 Boolean Initial Values 28.5 Verification 28.5.1 Combinational Equivalence Checking 28.5.2 Absorbing Checking 29hapter 4 Experimental Results 30.1 Variable Decision Order 30.2 Adjustable Interpolation on CDCC1 33.3 Adjustable Interpolation on CDCC2 40hapter 5 Conclusions and Future Work 46ibliography 472664599 bytesapplication/pdfen-US內插法邏輯網路邏輯無關項可滿足性問題求解可調整內插Craig interpolationlogic networkSAT solvingadjustable interpolantthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/189190/1/ntu-98-R95943159-1.pdf