Global Sources
電子工程專輯
 
電子工程專輯 > 測試與測量
 
 
測試與測量  

形式驗證在IP軟核VMI介面電路設計中的應用

上網時間: 2003年11月17日     打印版  Bookmark and Share  字型大小:  

關鍵字:IP  Soft Core  SoC  Formal Verification  形式驗證 

形式驗證屬於靜態分析方法,它不需要人為提供時脈基準、測試向量和激勵訊號,而是利用數學分析方法給出完備的模擬向量,因而大幅提高了模擬速度,對於數百萬閘級的設計,傳統驗證需要十幾天,而利用形式工具驗證只要數小時。本文介紹形式驗證在IP軟核-VMI介面電路設計中的應用。

目前,隨著IC設計向大型系統單晶片(SoC)設計轉移,內部和第三方IP整合的廣泛應用,已經使系統單晶片的體積和功耗減少,可靠性、穩定性和抗干擾性大為提高,而且訊號的傳輸延遲降低,系統可以執行在更高頻率上。但由於晶片中不同功能的模組越來越多,測試程式越來越複雜,測試向量越來越深,系統的驗證與測試已成為了制約設計周期和品質的瓶頸。

IP軟核由HDL語言寫成,可讀性好,易於開發,其良好的再使用性能,可大幅提高設計效率及設計品質,縮短產品的開發周期,使得極大規模(ULSI)的SoC設計效率大為提高。IP軟核的驗證是IP軟核開發中至關重要的一環,其驗證方式的選取對設計周期具有重要影響。形式驗證的載體是現代的等效檢驗工具,其利用先進的自動化和高效的除錯能力可減少這些瓶頸,並可縮短數個星期的驗證處理時間,因而大幅縮短產品的上市時間。

形式驗證

形式驗證是利用形式的技術,包括數學概念、技巧及一定的演算法,在形式上對兩個角度不同、抽象層次不同的設計,進行功能上是否等效的檢驗[1]。

其等效驗證工具可用來比較兩個電路設計邏輯行為。這種比較確保了設計在整個設計流程中始終保持相同的行為。一個由上而下的設計流程一般從演算法或行為級模型開始,這些模型採用C、Verilog或VHDL等硬體語言進行描述,然後轉到更具體的暫存器轉換級(RTL)設計,並利用邏輯合成工具實現閘級描述。等效檢驗可識別一個導出設計與原始設計會否在功能上等效,例如RTL設計與綜合後網表,見圖1。

每次一個設計進入到一個新的設計階段,即使進行的是無功能改變的轉換,也有可能導入新的錯誤。透過比較低一級設計和高一級設計行為,形式驗證可讓我們發現、診斷和消除無意識導入的錯誤。在大規模電路的模擬中,這一點是非常有益的。

形式驗證是靜態分析方法。其驗證工具不需要人為提供時脈基準、測試向量和激勵訊號,它利用其獨特的數學分析方法,給出完備的模擬向量,排除了人工測試的不完備性,大幅提高了模擬速度。數百萬閘級的設計,傳統驗證需要十幾天,結合靜態時序分析,利用形式工具驗證只要數小時。

Formality工具

Formality形式驗證工具利用其自身提供的演算法和程式,對被驗證的設計進行比較點測試,和向量覆蓋率測試等,大幅減少了人工干預,提高了測試效率。Formality具有以下主要性質:

(1)在時間上更快於利用激勵驅動的模擬;


(2)可進行RTL-to-RTL、RTL-to-gate和gate-to-gate驗證;


(3)提供診斷功能來對兩個設計功能不一致的地方進行查錯和隔離;


(4)可讀的文件格式有可綜合的VHDL、Verilog及Synopsys的.db格式等;


(5)進行智慧的層次化驗證;


(6)使用Synopsys Design Compiler製程庫;


(7)提供GUI和fm_shell兩種介面;


(8)進行大範圍的設計調度和調整的驗證,包括管道調時和再編碼有限狀態機;


(9)提供schematic views和單獨的‘cone of logic’以定位設計差異所在。

設計實例

1 輸入驗證對象

這裡的輸入為兩個設計,其一是VMI(Video Module Interface)介面模組,它是我們設計由Verilog語言編寫的IP軟核,以.v格式文件輸入,作為reference(ref);另一為其綜合後的網表文件,可以.v或.db的格式,我們採用.db的格式輸入,作為implementation(impl)。我們的任務是透過形式的方法來驗證這兩個模組是否功能等效。

輸入腳本文件:% formality -f run.f

腳本文件的內容如下:

2 設置等效檢驗對象

這裡我們設置VMI模組為top_design,進行包括其子模組在內的全部的比較驗證,見上述腳本的/4/5/8/9。也可以只設置其子模組,如控制模組,暫存器模組等。

Formality有其智慧的層次化測試體系,即可將其驗證的各模組按層次測試,也可根據需要,進行黑盒子等效,用平面化處理,將測試對象作為整體。即在局部範圍被認為不等效的訊號埠,從整體來看是等效的,這一點能被正確檢測。如圖2可見模組的邊界測試點最佳化[2][4]的情況。

3 比較點檢驗

比較點的類型有net、port、dff和latch等,輸入% match命令,Formality自動進行比較點的檢驗,可進行命名規則檢查,當然是在功能等效的基礎上,如果名稱不同,也可進行訊號分析檢查。比較點檢驗的原理是工具利用如下的分割程式[3] [5],產生試錯向量:

=================================


While (unprocessed partition with size > 2 still exits) {


pick a partition;


search for a test vector that sets opposite values at


some reference and implementation latches;


if (found such test vector) {


simulate the test vector;


create two new partitions, one containing latches


with 0 values and the other with 1 values;


} else {


mark partition as processed and cannot be divided;


}


}


=========================================


對ref和impl的兩個比較點總是輸入相反的值進行測試。Formality在比較時,會產生256個試錯向量。對failing points進行failing patterns測試,統計錯誤覆蓋率。

4 功能等效驗證

輸入%verify 命令,進行功能等效驗證,又稱為等效檢驗。它又包括一致性驗證和等價驗證,一致性驗證是測試具有確定有效訊號的比較點的功能等效性,等價驗證除了包含前一種驗證外,還判斷其不定態是否等效。

5 驗證結果

驗證結果顯示:60個Port和495個DFF共555個比較點都經過了驗證。

本文小結

利用Formality工具對IP軟核進行形式驗證可大幅加速驗證速度,其完備的試錯向量的運用,既可節省人力,又可去除人工測試的不完備性,極大提高了驗證的可靠度。如何提高設計效率,縮短IP軟核的開發周期是業界現面臨的重要課題,運用形式驗證無疑為這一領域開闢出一條新的思路。

作者:吳鈴鈴、周干民、何偉


合肥產業大學微電子設計研究所


Email: wulingling@hfut.edu.cn

參考文獻


[1] D. Brand, "Verification of large synthesized designs," in ICCAD, 1993, pp. 534 - 537.


[2] S.M.Reddy, W.Kunz and D.K.Pradhan, "Novel verification framework combining structural andOBDD methods in asynthesis environment," in DAC 1995, pp. 414 - 419.


[3] A.Kuehlmann and F.Krohm, "Equivalence Checking Using Cuts and Heaps," in DAC 1997, pp. 263 - 268.


[4] C.A.J.van Eijk and J.A.G.Jess, "Detection of Equivalent State Variables in Finite State Machine Verification," in IWLS, 1995.


[5] S-Y.Huang, K-T.Cheng, K-C.Chen and U.Glaeser, "An ATPG-Based Framework for Verifying Sequential Equivalence," in ITC, 1996, pp. 865 - 874.





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


EE人生人氣排行
 
返回頁首