《基於字級求解的電路錯誤自動定位方法研究》是依託中國人民解放軍國防科技大學，由張建民擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於字級求解的電路錯誤自動定位方法研究
- 項目類別：青年科學基金項目
- 項目負責人：張建民
- 依託單位：中國人民解放軍國防科技大學
中文摘要,結題摘要,
中文摘要
隨著VLSI晶片功能越來越複雜，大量的時間消耗在功能驗證上，而目前錯誤定位仍主要依賴於手工勞動，效率低下且易於引入新的錯誤，因此錯誤自動定位方法成為新的研究熱點。但是現有方法存在抽象層次低、運算複雜度高、處理電路規模有限等問題。.針對這些問題，研究基於字級求解的電路錯誤自動定位理論與方法；研究基於約束依賴圖的高層HDL程式切片算法，以抽取有效電路；研究基於等價約簡與蘊含消除的斷言精化方法，以減小斷言規模；研究融合字級不可滿足子式與Craig插值的錯誤蹤跡最佳化方法，以提高定位精度；研究基於否證分析與增量式求解的錯誤敏感向量壓縮方法，以剔除冗餘輸入；面向RTL級和行為級電路描述，設計實現錯誤自動定位的原型系統。.本項目的研究成果，能夠顯著提高VLSI晶片驗證的效率，有助於縮短設計周期，突破制約晶片驗證的瓶頸，具有重要理論意義與實際套用價值。
結題摘要
針對VLSI晶片的設計與驗證流程中，診斷與定位錯誤依賴於手工勞動且效率低下的問題，項目重點研究如何自動、高效地定位RTL級和行為級電路描述中的錯誤，通過設計與實現一系列形式化方法與技術，大大提高錯誤定位的效率與精度，從而加速晶片的設計與驗證流程。項目的主要研究成果包括： （1）針對近年來出現的許多電路錯誤定位方法，深入研究與分析了基於位級與字級的錯誤定位方法的基本原理，並對各種算法進行了評估與分析；並針對不可滿足子式能夠顯著提高錯誤定位效率與精度進行了深入分析。 （2）針對求解不可滿足子式可以顯著提高電路定位錯誤的效率，提出了悖論證明與悖論解析樹的概念，並提出一種啟發式局部搜尋算法，從布爾公式的悖論證明中求解不可滿足子式。基於實際測試集進行了實驗對比，結果表明該算法優於同類最優算法。 （3）針對布爾不可滿足子式能夠幫助自動化工具迅速定位電路錯誤，提出了求解布爾不可滿足子式的消解悖論算法。它屬於一種非完全算法，對於業界常見的3-SAT和2-SAT問題非常高效。基於隨機測試集進行了實驗對比，結果表明消解悖論算法優於其他同類算法。 （4）隨著硬體設計與驗證的抽象層次越來越高，基於一階邏輯的可滿足性模逐漸成為研究熱點。針對極小可滿足性模的不可滿足子式的求解問題，提出了基於深度優先搜尋與增量式求解的算法。與目前最優算法對比，該算法能夠有效地求解極小不可滿足子式，並且隨著公式的規模增大，算法更加高效。 （5）高速緩衝存儲器（Cache）的錯誤定位是驗證領域的研究熱點與難點，對此提出了一種面向Cache的可綜合偽隨機驗證與錯誤定位方法。與業界常用的方法對比，該方法的處理速度快約3個數量級，並且能夠精確地定位更多的功能錯誤。 （6）謂詞抽象技術是解決錯誤定位中狀態空間組合爆炸問題的重要途徑，而不可滿足子式能夠減少謂詞抽象過程中精化疊代的次數。因此將兩種最小不可滿足子式的求解算法進行了集成與對比，並深入分析了不可滿足子式在硬體謂詞抽象中的作用，以及如何加速電路的錯誤定位過程。
