《EDA形式驗證中可滿足性(SAT)問題的算法研究》是依託復旦大學，由荊明娥擔任項目負責人的面上項目。
基本介紹
- 中文名：EDA形式驗證中可滿足性(SAT)問題的算法研究
- 依託單位：復旦大學
- 項目類別：面上項目
- 項目負責人：荊明娥
- 批准號：60773125
- 申請代碼：F0209
- 負責人職稱：副研究員
- 研究期限：2008-01-01 至 2010-12-31
- 支持經費：27（萬元）
項目摘要
隨著積體電路設計規模和複雜性的增加，驗證成為設計的瓶頸。而依靠測試向量的模擬驗證方法遠遠不能滿足大規模設計驗證的需求。具有完備特性的形式化方法成為驗證的一個重要選擇，但目前只能在用戶不斷的干預下解決小規模的驗證問題。在本項目中，我們將針對積體電路驗證問題規模大的特點和EDA驗證工具自動化的需求，研究形式化驗證中的核心問題-SAT算法。首先，研究SAT問題的變數類型和高效預處理方法，建立一個能夠產生多米諾骨牌效應的不斷簡化的，結合多種預處理技術的高效預處理器，目的是在初始階段減小問題的規模和難度。其次，在求解過程中，通過研究學習子句的空間有效性，及時動態地刪除冗餘學習子句來控制問題規模的增加，避免解決器因為記憶體爆炸而得不到解。最後，我們將利用SAT解決器解決大規模設計驗證過程中的等價性驗證和模型檢驗問題。
