針對暫存器轉移階層驗證而專門設計之可滿足性解法器

Engineering a Word-Level Satisfiability Solver for RTL Design Verification

饒瑞晞(Ruey-Shi Rau)

指導教授 ： 黃鐘揚

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

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

摘要

現代的數位硬體設計多半從暫存器轉移階層開始描述，再經由一連串的自動化操作直到實體電路設計完成。而由於早期發現設計錯誤所需的成本遠較後期發現為低廉，因此暫存器轉移階層的驗證至關重要。
可滿足性解法器為正規驗證中重要的核心引擎。為此，本論文提出一專為暫存器轉移階層驗證而設計之可滿足性解法器。此解法器基於Davis-Putnam-Logemann-Loveland演算法，配合位元向量階層的電路描述、各種位元向量邏輯閘的蘊涵關係、以及專為各種位元向量邏輯閘特別設計的矛盾分析。相較於其他的解法器，我們的解法器不僅保留了電路結構的相關資訊，更由於我們並未將位元向量階層的邏輯閘展開為單一位元邏輯閘的集合，更多暫存器轉移階層的資訊因而得以被保留，且可應用於解題過程之中。實驗結果顯示，我們的解法器效能足以和當今一流的解法器相匹敵。

關鍵字

驗證 ； 可滿足性問題 ； 可滿足性解法器 ； 暫存器轉移階層 ； DPLL

並列摘要

Modern digital hardware design begins from register-transfer-level (RTL) description. Then, the RTL description passes through a series of design automation procedures until the physical layout is completed. Since the cost of design errors is much lower if they are found in earlier design stages, the verification on RTL is very important.
The satisfiability solver is one of the essential core engines for formal verification. Therefore, this thesis proposed a word-level satisfiability solver for RTL design verification, QuteWSat. QuteWSat combines David-Putnam-Logemann-Loveland algorithm, word-level circuit description, implication procedures and conflict analysis procedures for each type of word-level logic gates. Compared with other satisfiability solvers, QuteWSat preserves the structural information about the circuit, and since it does not expand word-level logic gates into bit-level logic gates, some RTL information can be preserved and utilized in the solving process. The experimental results show that the performance of QuteWSat is comparable to that of a state-of-the-art solver.

並列關鍵字

Verification ； Satisfiability Problem ； Satisfiability Solver ； Register-Transfer-Level ； RTL ； DPLL

參考文獻

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

[3] S. Hassoun and T. Sasao, Logic Synthesis and Verification. Kluwer Academic Publishers, 2001.

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

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

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