請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/62162
標題: | MeowSAT: 基於多理論積極整合技術之詞級可滿足性解法器 MeowSAT: A Word-Level Satisfiability Solver Based on Eager Integration of Theories |
作者: | Yu-Yun Dai 戴伃芸 |
指導教授: | 黃鐘揚(Chung-Yang Huang) |
關鍵字: | 正規驗證,可滿足性問題,可滿足性模理論,詞級可滿足性解法器,線性整數算術, Formal Verification,Satisfiability Problem,Satisfiability Modulo Theories,Word-level Satisfiability Solvers,Linear Integer Arithmetic, |
出版年 : | 2013 |
學位: | 碩士 |
摘要: | 作為當代正規驗證的核心引擎,布林階層的可滿足性解法器已有長足的發展。然而,為了在維持高階資訊下驗證暫存器轉移階層的設計,專門針對位元向量邏輯運算的高效率詞級可滿足性解法器有其發展的必要性。
因此,本論文針對位元向量邏輯運算的問題提出了一套詞級可滿足性解法器的演算法及其實作方法。此解法器積極地整合兩個不同的解法器:其一專門處理布林階層的滿足性問題,另一個則針對線性算術部分的問題。其中,一個原創的純粹詞級解法器被實作來處理線性算術限制,並同時處理等式與不等式。相較於其他的解法器,本論文提出的解法器能以處理線性限制的方式來處理算術運算元,而不是將其展開為單一位元邏輯閘的組合。實驗結果顯示,本論文所提出的解法器設計和實作方法能夠與現今一流的解法器有相近的效能,並能更有效的處理包含大量算術運算元的問題。 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. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/62162 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-102-1.pdf 目前未授權公開取用 | 850.16 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。