《基於下一代驗證引擎的事務級形式驗證方法的研究》是依託清華大學，由邊計年擔任項目負責人的面上項目。
基本介紹
- 中文名：基於下一代驗證引擎的事務級形式驗證方法的研究
- 依託單位：清華大學
- 項目負責人：邊計年
- 項目類別：面上項目
- 負責人職稱：教授
- 批准號：60876030
- 研究期限：2009-01-01 至 2011-12-31
- 申請代碼：F0402
- 支持經費：32（萬元）
項目摘要
驗證已成為積體電路設計的瓶頸，為了縮小驗證與設計之間的差距，高層次的建模和驗證顯得越來越重要。研究內容主要是把SAT和SMT的方法引入到國際最前沿的更高層次的事務級模型（TLM），研究高效的事務級自動形式驗證方法。研究工作主要分為三點：1. 從理論和方法上研究滿足TLM的SAT問題和SMT問題。2.以SystemC驗證庫SCV為基礎，研究使用下一代驗證引擎- - 字位混合SAT求解器和可滿足性模理論（SMT）中的先進技術進行事務級驗證的相關算法，該算法包括隨機化、定界模型檢驗、抽象細化等技術點。3.研究開發包含傳輸層、協定層、用戶層的三層結構TLM驗證平台，便於進行自動的數據檢查、事務檢查、基於斷言的驗證以及基於時態邏輯的性質檢驗。以上工作緊密相關，其中前兩步工作是第三步工作的基礎。本項目的研究成果將對事務級的驗證產生重要影響。
