基于SAT的有界模型檢測及其應用研究.pdf

1、無論在計算機系統(tǒng)硬件設計方面還是在軟件設計方面，隨著設計規(guī)模越來越復雜和龐大，會產生越來越多的設計缺陷和錯誤等。用一些傳統(tǒng)的方法往往是代價很高，但還難以檢測出它們。形式化驗證的優(yōu)點是在一個設計或系統(tǒng)的研制周期的前期進行。在研制周期的早期進行分析和驗證，可大大降低返工的成本，提高效率?；谶@些原因，有界模型檢測(Bounded Model Checking簡稱BMC)作為一種重要的形式化驗證的方法，它的相關技術的研究和應用在當前具有相當重

2、要的價值和意義。 有界模型檢測是通過把有限狀態(tài)機(FSM)和LTL邏輯驗證規(guī)范否定形式編碼成SAT實例，再由各種SAT工具來求解，以獲得反例。該方法相比基于OBDD技術的模型檢測，進一步減輕的狀態(tài)空間爆炸問題，且給出的反例是最短的。 因為BMC較晚出現(xiàn)，它的很多相關的技術不完善、相關的應用也不普遍。本文圍繞BMC的相關技術和應用進行了一定的研究。主要工作如下： BMC編碼技術的優(yōu)化可生成規(guī)模小易于求解的SAT實例

3、，對提高有界模型檢測的效率至關重要，近年其是BMC研究中一個熱點問題。本文結合FSM狀態(tài)轉移的特性和線性時序邏輯的語義，在現(xiàn)有的編碼基礎上，對有界模型檢測中對驗證G(p)和G(p→F(q))這兩個很重要很常用的模態(tài)算子轉換公式進行了優(yōu)化，給出了簡潔高效的遞推公式；證明了遞推公式和原公式的邏輯關系；基于遞推公式設計了編碼算法。通過實驗比較分析，基于遞推公式編碼算法在生成SAT實例規(guī)模和求解效率方面，都優(yōu)于現(xiàn)有的兩個主流的編碼算法。所給出的

4、方法和思想對有界模型檢測的其他模態(tài)算子編碼的優(yōu)化，有直接的參考價值。 SAT工具是BMC的后端求解工具。SAT問題的研究對包括BMC在內的許多領域都很有意義。局部搜索方法是求解SAT實例的一類重要的方法。本文提出用初始概率的方法對局部搜索算法中的變量的初始隨機指派進行適當?shù)募s束，用該方法對目前的一些重要的SAT問題的局部搜索算法進行改進，通過對不同結構、不同規(guī)模的SAT問題的實例測試表明，改進后的這些局部搜索算法的效率有了較大的