《RTL電路的混合可滿足性求解和模型檢驗》是依託清華大學，由吳為民擔任項目負責人的面上項目。
基本介紹
- 中文名：RTL電路的混合可滿足性求解和模型檢驗
- 依託單位：清華大學
- 項目負責人：吳為民
- 項目類別：面上項目
- 批准號：60673034
- 申請代碼：F0209
- 負責人職稱：副教授
- 研究期限：2007-01-01 至 2009-12-31
- 支持經費：25（萬元）
項目摘要
本課題的研究目的是：在暫存器傳輸級（RTL）電路上研究和實現一種可行、高效的模型檢驗(MC)方法。這種方法是通過對混合可滿足性問題（HSAT）的求解和套用來實現的。.本課題主要包含兩個方面的研究內容：.1．.混合可滿足性求解器的研究。這是一個同時包含有字（word）和位（bit）變數的、具有多種約束形式的混合可滿足性問題。我們將在基於ATPG和基於擴展DPLL兩種途徑上研究解決HSAT問題的有效方法。變數決策和約束傳播是其中的核心技術。.2．.基於HSAT的RTL模型檢驗技術的研究。其研究內容涉及：時序展開、從驗證性質到HSAT問題的轉換、HSAT求解、以及如何提高驗證的完備性等問題。歸納推理和無界模型檢驗(UMC)是提高驗證完備性的主要技術。.以上的兩方面研究內容緊密相聯，是解決RTL模型檢驗問題的最關鍵技術。
