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

Abstract

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

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.