Global Sources
電子工程專輯
 
電子工程專輯 > EDA/IP
 
 
EDA/IP  

什麼是形式驗證?

上網時間: 2010年08月09日     打印版  Bookmark and Share  字型大小:  

關鍵字:corner-case  RTL  ABV  形式驗證  RTL 

在目前複雜的數位設計開發過程中,功能驗證十分重要。雖然硬體的複雜度仍遵循摩爾定律持續成長,但是驗證的複雜性更具挑戰。事實上,隨著硬體複雜性隨時間呈雙指數成長,驗證複雜性理論上也呈指數成長。驗證已被公認為是設計過程中的主要瓶頸:高達70%的設計開發時間和資源花在功能驗證上。Collett International Research認為,即使在驗證上花費如此巨大的精力和資源,功能性缺陷仍是晶片重新投片的頭號原因。

功能性驗證挑戰

邊際情形(corner-case)的缺陷是模擬偽像,由於以模擬為基礎的驗證具有非窮盡的固有特性,因此邊際情形無法被檢測到。事實上,不管你用多少時間模擬,也不管你的測試平台和產生器有多麼智慧,透過模擬驗證設計意圖對於最小電路以外的所有電路來說都是不完整的。基本的模擬偽像可以被分成三類:窮盡型、可控型和可觀察型,如表1所示。

表1:模擬與形式驗證的比較。
表1:模擬與形式驗證的比較。

形式驗證是一個系統性的過程,將使用數學推理來驗證設計意圖(指標)在實現(RTL)中是否得以貫徹。形式驗證可以克服所有3種模擬挑戰(表1),因為形式驗證能夠從演算法上窮盡檢查所有隨時間可能變化的輸入值。換句話說,沒有必要顯示如何激勵設計或製作多種條件來實現較高的可觀察性。

雖然從理論上講,模擬測試平台的輸入埠針對待驗證設計(DUV)具有較高的可控性,但測試平台對內部點的可控性一般較差。為了使用基於模擬的方法識別設計錯誤,以下條件必須保持:

* 必須產生正確的輸入激勵,以啟動(也就是感應化)設計中某個點的缺陷

* 必須產生正確的輸入激勵,以便將源自缺陷的所有效果傳送到輸出埠

在使用基於模擬的驗證時,需要規劃設計中需要驗證的對象:

* 定義需要測試的各種輸入條件

* 製作功能性覆蓋模型(確定是否做了足夠的模擬)

* 搭建測試平台(檢查器,測試樁,產生器等)

* 製作特定的直接測試

* 成年累月的模擬

現實中,工程師一直在反覆做著這些事:執行測試、除錯故障、再次模擬回歸組、觀察各種覆蓋率指標,以及調整激勵(例如操控輸入產生器)以覆蓋以前未覆蓋的設計部份。

圖1:彈性緩衝記憶體架構圖。
圖1:彈性緩衝記憶體架構圖。


1 • 2 Next Page Last Page



投票數:   加入我的最愛
我來評論 - 什麼是形式驗證?
評論:  
*  您還能輸入[0]個字
*驗證碼:
 
論壇熱門主題 熱門下載
 •   將邁入40歲的你...存款多少了  •  深入電容觸控技術就從這個問題開始
 •  我有一個數位電源的專利...  •  磷酸鋰鐵電池一問
 •   關於設備商公司的工程師(廠商)薪資前景  •  計算諧振轉換器的同步整流MOSFET功耗損失
 •   Touch sensor & MEMS controller  •  針對智慧電表PLC通訊應用的線路驅動器
 •   下週 深圳 llC 2012 關於PCB免費工具的研討會  •  邏輯閘的應用


EE人生人氣排行
 
返回頁首