MeowSAT: 基於多理論積極整合技術之詞級可滿足性解法器

MeowSAT: A Word-Level Satisfiability Solver Based on Eager Integration of Theories

戴伃芸(Yu-Yun Dai)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2013年)

https://doi.org/10.6342/NTU.2013.02340

摘要

作為當代正規驗證的核心引擎，布林階層的可滿足性解法器已有長足的發展。然而，為了在維持高階資訊下驗證暫存器轉移階層的設計，專門針對位元向量邏輯運算的高效率詞級可滿足性解法器有其發展的必要性。
因此，本論文針對位元向量邏輯運算的問題提出了一套詞級可滿足性解法器的演算法及其實作方法。此解法器積極地整合兩個不同的解法器：其一專門處理布林階層的滿足性問題，另一個則針對線性算術部分的問題。其中，一個原創的純粹詞級解法器被實作來處理線性算術限制，並同時處理等式與不等式。相較於其他的解法器，本論文提出的解法器能以處理線性限制的方式來處理算術運算元，而不是將其展開為單一位元邏輯閘的組合。實驗結果顯示，本論文所提出的解法器設計和實作方法能夠與現今一流的解法器有相近的效能，並能更有效的處理包含大量算術運算元的問題。

關鍵字

正規驗證 ； 可滿足性問題 ； 可滿足性模理論 ； 詞級可滿足性解法器 ； 線性整數算術

並列摘要

As the core engines for formal verification, Boolean satisfiability solvers have been developed very well. However, to verify register-transfer-level designs without dismissing high level information, efficient word-level satisfiability solvers, which process logic operations over bit-vectors, are desired.
Therefore, this thesis proposed a word-level satisfiability solver, MeowSAT, for quantifier-free logics over bit-vectors, including its algorithms and implementations. MeowSAT performs lazy approach with eager integrations between two solvers, which are responsible for pure Boolean and linear arithmetic instances respectively. Indeed, an in-house pure word-level solver is implemented to process linear integer arithmetic equality and inequality constraints. Compared with other word-level satisfiability solvers, MeowSAT manipulates arithmetic operations with the constraint solver, not by fully expanding into Boolean logic gates. The experimental results show that the performance of MeowSAT is comparable to that of state-of-the art solvers, especially for those cases with high portion of arithmetic operators.

並列關鍵字

Formal Verification ； Satisfiability Problem ； Satisfiability Modulo Theories ； Word-level Satisfiability Solvers ； Linear Integer Arithmetic

參考文獻

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

[5] IEEE Standard Verilog Hardware Description Language. IEEE Standard 1364-2001. Institute of Electrical and Electronics Engineers, 2001.

[6] IEEE Standard VHDL Language Reference Manual. IEEE Standard 1076-2002. Institute of Electrical and Electronics Engineers, 2002.

[12] M. Davis, G. Logemann and D. Loveland, “A Machine Program for Theorem-Proving”. In Communications of the ACM, vol. 5, pp. 394 – 397, 1962.

[13] J. P. Marques Silva and K. A. Sakallah, “GRASP – A New Search Algorithm for Satisfiability”. In Proc. International Conference on Computer-Aided Design, pp. 220 – 227, 1996.