[發明專利]集成電路驗證方法及其系統

有效

• 申請號: 200910244172.2
• 申請日: 2009-12-30
• 公開（公告）號: CN101794330A
• 公開（公告）日: 2010-08-04
• 發明（設計）人: 張弢;呂濤;李曉維
• 申請（專利權）人: 中國科學院計算技術研究所
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 北京律誠同業知識產權代理有限公司 11006
• 代理人: 祁建國;梁揮

技術領域

本發明涉及大規模集成電路驗證領域，尤其涉及集成電路驗證方法及其系 統。

背景技術

隨著集成電路產業的迅速發展，設計的多樣性和復雜性程度也越來越高， 而傳統功能驗證方法處理的設計規模和效率的增長落后于開發規模的增長，使 得其面臨的困難越來越大。

集成電路復雜性增長給功能驗證帶來的難題包括兩個方面：第一設計內部 功能邏輯、接口協議、例外處理等等復雜度急劇增加，憑借人工經驗或已有方 法難于處理；第二集成電路結構里包含的寄存器數目增加，造成仿真的速度越 來越慢，使得形式化驗證方法更加難以處理。為了解決或緩解上述兩個問題， 集成電路功能驗證方法需要盡量減少需要的人工專家知識，并且生成較短的測 試向量，以驅動仿真驗證特定的功能屬性。

另外，在現有集成電路驗證流程中，設計的功能覆蓋率的增加并不為線性， 尤其對于設計的難達屬性或者狀態，往往耗費大量的驗證成本而收效甚微。針 對集成電路中難達屬性或者狀態的驗證，是一個急需解決的問題。已有的集成 電路的功能驗證方法主要分為模擬驗證和形式化驗證兩大類方法。

模擬驗證方法主要通過給設計輸入測試向量進行仿真，并且將仿真的結果 和一個功能正確的黃金模型(Golden?Model)進行對比，以驗證設計在不同的 輸入激勵情況下的功能正確性。模擬驗證方法能夠快速的驗證一些常見的設計 屬性，但是對于難以到達的邊緣屬性，難于在有限時間內進行覆蓋和驗證。雖 然可以通過人工手工寫測試向量來驗證特定功能點，但需要耗費大量的人力時 間，并且測試向量難以在不同設計間重用，不能夠作為主要的驗證手段。

形式化驗證方法中，主要是模型檢驗(Model?Checking)方法，比較適合于 對設計的邊緣屬性進行驗證。在這類方法中，集成電路設計被抽象為一個有限 狀態模型，目標屬性則被描述為一個時態邏輯公式，驗證的過程為遍歷有限狀 態模型中的可達狀態，從而證明集成電路設計滿足目標屬性；或者給出一個狀 態序列形式的反例，以證明目標屬性不可滿足。模型檢驗具有規范化、易于自 動化、完全的特點，但其中狀態空間大小隨設計中寄存器數目指數增長(2^n)， 造成“狀態爆炸”；這也是困擾模型檢驗方法在大規模工業設計上得到應用的 根本問題。

通過對模擬驗證和形式化驗證方法分別的優缺點和適應場景的分析，可以 發現一種提高驗證效率和驗證可處理設計規模的方法：將形式化驗證和模擬驗 證方法結合起來，在原始設計上進行一定程度的抽象，在抽象模型上用形式化 驗證方法獲取部分設計信息，然后用這些信息引導模擬仿真生成較短的仿真向 量，從而快速、準確的驗證到目標的設計邊緣屬性。通過抽象能夠減少形式化 方法計算的代價，同時獲得的設計信息能夠幫助提高對目標屬性進行模擬驗證 的效率。

采取這種優化的驗證方法，一個問題在于如何對電路進行抽象，才能夠使 獲得的抽象模型較小、且包含較準確的設計信息。最簡單直觀的方法是借助工 程師對集成電路設計的理解，人工提取部分與目標最相關的邏輯作為抽象模 型。這種方法對于中小設計效果較好，但對于復雜設計則效果得不到保證，并 且需要大量專家時間，不適合自動化驗證的需求。另一種方法則基于現代集成 電路設計模塊化的思想，提取和目標狀態對應的信號關系密切的設計模塊作為 抽象模型。但如果模塊較大，則導致抽象模型過于復雜，并且這種方法抽象的 粒度較大，不夠理想。還有采用數據挖掘方法，在集成電路設計中各個寄存器 位之間挖掘關系，將關系密切的寄存器位加入抽象模型。該種方法在寄存器位 (bit)級上進行，并不適合寄存器傳輸級功能驗證的需要。