| Summary: | 碩士 === 國立臺灣大學 === 電子工程學研究所 === 101 === 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.
|
|---|
