在電路上實現可滿足性解法器以及其在函數相依性分析與矛盾抽取證明上之應用

在本論文的第一部分，基於驗證邊界(Justification Frontiers)，我們設計了擁有利用問題內含電路結構能力的電路可滿足性解法器。裝備驗證邊界技巧的演繹技術可以不需在電路上實作而以在句型上(Clauses)實作取代，同時還能夠保持完整的電路結構。以DPLL演算法為骨幹，我們的可滿足性解法器成功的包含了決定、演繹、診斷以及證明儲存引擎中最新的方法。我們也在解法器參數上下了很大的功夫去調整以達到整體的最佳效能。實驗結果顯示，我們的解法器至少可能夠目前世界上最佳的解法器披敵，甚至在某些例子上還遠勝於它們。在電路結構上的靈活性使得我們的可滿足性解法器能為未來研究廣義可解法性問題開拓道路。函數性依賴(Functional Dependency)與於如何改寫布林函數f成為一個依賴於一組基底函數{g1, …, gn}的函數h使得f = h(g1, …, gn)的問題有緊密的關連性。函數性依賴在電子設計自動化領域中扮演了重要的角色，從邏輯合成到正規驗證都有其應用之處。先前探索函數性依賴的方法乃基於二元決策樹(BDDs)的使用，然而二元決策樹在處理大型電路設計的能力上卻不足夠。本論文的第二部分提出了一個嶄新的方法，此方法大量運用了現代可滿足性解法器(SAT Solvers)的優秀能力。經由此法以及微量可滿足性解法，函數性依賴的偵測問題能夠很有效率的被解決。若問題中的依賴性函數存在，我們接下來可使用克瑞格內插法(Craig Interpolation)進一步的得到此函數。我們所建議方法的優點如下:(1)僅需使用少量的記憶體即可有效率的解決函數性依賴的偵測問題，因而可以解決大型電路設計的問題；(2)對於處理大量基底函數擁有完整的能力，因而只要依賴性函數存在，我們必能得到它；(3)對於多種面向限制的大型邏輯優化問題擁有潛在性的應用。實驗結果顯示我們所提出的方法效能遠勝過先前的方法，而且對於最多可到二十萬邏輯閘的大型ITC以及ISCAS電路的處理能力表現上也相當的好。

關鍵字

滿足性問題；電路資訊；驗證邊界；矛盾證明；函數性依賴；克瑞格內插法

並列摘要

In the first part of the thesis, we have devised a circuit SAT solver with the ability to exploit inherent circuit structure properties for circuit oriented problems based on the concept of justification frontiers. With J-clauses, an extension of J-gates [1], the deduction equipped with justification frontiers can be done on clauses instead of gates while preserving the circuit structure. With DPLL algorithm as the backbone, our solver incorporates the newest techniques for decision, deduction, diagnosis, and proof engines. Large efforts have been paid for tuning the parameters to achieve the best performance for all the benchmark suits. The experimental results shows that our SAT solver is at least competitive with state-of-art ones and superior to them for some benchmark suits. With the great flexibility on the circuit structure, our solver can serve as a solid foundation for the general SAT research in the future. Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions {g1, …, gn}, i.e. f = h(g1, …, gn). It plays an important role in many aspects of electronics design automation (EDA), ranging from logic synthesis to formal verification. Prior approaches to the exploration of functional dependency are based on binary decision diagrams (BDDs), which may not be easily scalable to large designs. This second part of the thesis proposes a novel reformulation that extensively exploits the capability of modern satisfiability (SAT) solvers. Thereby, functional dependency is detected effectively through incremental SAT solving and the dependency function h, if exists, is obtained through Craig interpolation. The main strengths of the proposed approach include: (1) fast detection of functional dependency with small memory consumption and thus scalable to large designs, (2) a full capacity to handle a large set of base functions and thus discovering dependency whenever exists, and (3) potential application to large-scale logic optimization with different design constraints. Experimental results show the proposed method is far superior to prior work and scales well in dealing with the largest ISCAS89 and ITC99 benchmark circuits with up to 200K gates.

並列關鍵字

Boolean Satisfiability ； Circuit Information ； Justification Frontier ； Refutation Proof ； Functional Dependency ； Craig Interpolation

參考文獻

[1] C.-A. Wu, T.-H. Lin, C.-C. Lee, C.-Y. Huang. “QuteSAT: A Robust Circuit-based SAT Solver for Complex Circuit Structure”. In Design Automation and Test in Europe (DATE) Conference, pp.1313-1319, 2007.

[2] C.-C. Lee, J.-H. R. Jiang, C.-Y. Huang, and A. Mishchenko. "Scalable Exploration of Functional Dependency by Interpolation and Incremental SAT Solving". In Proc. International Workshop of Logic Synthesis (IWLS), 2007

[3] S. A. Cook. “The Complexity of Theorem Proving Procedures”. In Proc. Third Annual ACM Symposium on the Theory of Computing, pp. 151-158, 1971

[4] S. H. Gerez. “Algorithms for VLSI Design Automation”. John Wiley & Sons, 1999.

[5] E. M. Clarke, O. Grumberg, D. A. Peled. “Model Checking”. MIT Press, 1999.

國際替代計量

在電路上實現可滿足性解法器以及其在函數相依性分析與矛盾抽取證明上之應用

全文下載

主題瀏覽