《片上多核處理器驗證理論與關鍵技術》是依託中國人民解放軍國防科技大學，由郭陽擔任項目負責人的重點項目。
基本介紹
- 中文名：片上多核處理器驗證理論與關鍵技術
- 項目類別：重點項目
- 項目負責人：郭陽
- 依託單位：中國人民解放軍國防科技大學
中文摘要,結題摘要,
中文摘要
針對片上多核處理器驗證中設計規模大、驗證效率低、完備性不足、存儲結構與互連網路驗證複雜、矽後驗證困難等突出問題，研究突破片上多核處理器高層次建模與多視圖協同驗證方法、面向事務層與系統層的高效形式驗證引擎最佳化方法、基於SMT的片上網路可驗證性綜合、基於二維抽象的存儲一致性協定驗證、事務級模型與RTL描述的等價性驗證、半形式化的全晶片模擬驗證、矽後驗證輔助技術等理論與關鍵技術，建立高層次、可擴展的片上多核處理器高層次驗證理論方法體系，實現支持片上多核處理器驗證的系列工具原型，有效提高片上多核處理器驗證效率、完備性和可信性，並將研究成果直接套用於銀河飛騰系列多核CPU與DSP的驗證實踐。.所研究建立的模型、理論框架、方法在驗證科學領域達到國際領先水平，為我國自主高性能微處理器的可持續發展奠定堅實基礎。
結題摘要
針對片上多核處理器驗證中設計規模大、驗證效率低、完備性不足、存儲結構與互連網路驗證複雜、矽後驗證困難等突出問題，研究突破片上多核處理器高層次建模與多視圖協同驗證方法、面向事務層與系統層的高效形式驗證引擎最佳化方法、基於SMT 的片上網路可驗證性綜合、基於二維抽象的存儲一致性協定驗證、事務級模型與RTL 描述的等價性驗證、半形式化的全晶片模擬驗證、矽後驗證輔助技術等理論與關鍵技術，建立可擴展的片上多核處理器高層次驗證理論方法體系，實現支持片上多 核處理器驗證的系列工具原型，有效提高片上多核處理器驗證效率、完備性和可信性。在項目執行期間取得多項創新成果，包括：多核處理器體系結構事務級建模方法和多視圖協同驗證方法，極小SMT不可滿足子式求解算法，對偶綜合中自動推導前提斷言方法，參數化協定的狀態空間化簡方法，基於模擬與機器學習的系統級等價性驗證方法等。在IEEE TCAD、Journal of Supercomputing、ACM TODAES等國際期刊和本領域重要的國際會議上發表論文55篇，其中SCI期刊發表論文15篇，EI論文34篇。培養研究生44名，申請國家發明專利12項。理論研究成果有力支撐了飛騰系列CPU和DSP微處理器的驗證實踐。
