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

SystemVerilog可以提供基於聲明的高效驗證方法

上網時間: 2005年06月23日     打印版  Bookmark and Share  字型大小:  

關鍵字:聲明  驗證  系統級晶片  缺陷  模擬 

功能日益複雜、規模日益龐大的系統級晶片(SoC)元件正在給晶片驗證人員不斷施加壓力。生成一個沒有重大缺陷的設計是一項非常艱鉅的挑戰。基於聲明的驗證(ABV)是目前最佳解決方案之一,它能透過設計工程師的經驗知識和自動驗證方法在投片前對設計進行重點測試。本文將對這一方法作一簡要介紹,並論述SystemVerilog語言是如何孕育出如此高效並被廣泛使用的聲明和ABV。

聲明是表達設計者意圖的語句,以可執行的形式表達。理想情況下,設計工程師透過編程方式獲得RTL程式碼中的聲明。聲明可以為SoC開發過程提供許多幫助:

* 透過記錄設計者意圖可以使RTL程式碼變得更具有可讀性,並且更容易被再使用;


* 聲明將提取要求書或規範中的要素,因此可以與明確的RTL實現進行交叉檢查;


* 在有合適的聲明語言或指令條件下,聲明可以利用相對簡單的聲明語句捕獲複雜的瞬間行為


* 由於增加了模擬價值,實現了形式屬性分析,因此聲明可以增強驗證效果;


* 聲明可以透過檢查設計協議是否得到正確滿足來推進驗證IP(VIP)的

圖1:模擬與形式驗證整合後
可以用來驗證設計
在聲明方面的特性。

開發;

在模擬過程中,聲明可以非常高效地查出缺陷根源。與在晶片輸出時才檢測到模擬測試故障相比,聲明出故障時一般更容易分析和修補缺陷。在缺陷觸發時間和大型SoC輸出點可檢測缺陷時間之間,可能經過了數千個模擬周期。聲明在晶片級模擬中能盡早捕獲缺陷,並可將故障隔離到指定模塊,然後交給校正設計工程師進行診斷和修改。

形式屬性分析提供了一種不經過模擬使用聲明的途徑。聲明被認為是激勵約束方面的假設,以及被證明為正確(‘安全’)或用表明聲明如何失敗的‘反例’證明為錯誤的屬性。沒有通過證實,意味著聲明與設計之間存在著不一致性,即在聲明規範中存在可能由於要求的誤譯引起的RTL設計缺陷或錯誤。不管是哪種方式,設計工程師都能解決這樣的問題,並重新執行形式分析來獲得驗證。完全驗證可以保證聲明永遠不出問題,但對於大型設計或複雜聲明來說完全驗證幾乎是不可能做到的。在這種情況下,有限範圍的驗證多少可以提高驗證信心。

圖1是一種典型的ABV流程,其中的模擬、形式屬性分析或二者都是用來驗證聲明和設計的。模擬和形式屬性分析方法都能產生不同形式的聲明覆蓋。聲明覆蓋至少會報告模擬中哪些聲明失敗、哪些聲明成功通過,又有哪些聲明被形式分析所證實。更先進的覆蓋計測方法還能提供哪些聲明是‘溜’過去的,因為它們實際上沒有得到很好的測試。一個常見的例子是,FIFO溢出聲明通過了模擬測試,原因卻是FIFO從來沒有被填滿過。

採用ABV縮短開發時間

ABV是目前的一種主流技術,事實證明ABV可以改善驗證品質,縮短開發時間。儘管如此,但不是所有的設計人員都已經採納ABV,原因有多個。

第一個挑戰是教育的簡單化。編寫高品質的聲明要求設計與驗證工程師從特殊的RTL實現角度考慮設計的重要行為。例如,FIFO應該具有永不溢出(滿時還能寫入)或永不取空(空時還能讀)的聲明。這些聲明可以應用到所有FIFO,而不管它們是用鎖存器、觸發器、暫存器單元還是記憶體實現的。

第二個挑戰是決定如何定義聲明。VHDL擁有一個內建的聲明指令,不過該指令功能相當有限(例如沒有臨時序列)。而Verilog-1995和Verilog-2001沒有這樣的指令,因此必須使用某些外部方法。確切地說,業界存在許多種不同的屬性語言、語言擴展、基於附註的RTL內方法以及聲明檢查元件庫,而且其中有許多是針對特殊供應商的。對於新的聲明用戶來說,很難作出選擇。

第三,ABV的推廣使用深受來自聲明和形式分析學術界的觀點影響。他們認為所有的設計行為必須以屬性(或聲明)的形式捕捉到,設計正確性應該只被形式分析所證明,不需要模擬。雖然從理論上講是對的,但完全沒有實用性。因為很難用聲明捕獲所有類型的設計行為;有些行為用過程測試平台程式碼規定顯得更自然貼切。另外,形式引擎的能力限制意味著不可能為任意的大型設計證實任意複雜的聲明。

ABV的最大價值在於整合了模擬與形式分析的驗證流程中。例如,形式分析可能被用於50-500K閘的模組、功能單元(1-2M閘)級的模擬與形式分析的整合以及全晶片級的模擬。另外,混合形式驗證的先進技術實際上已經實現了在單個工具中融合模擬與形式分析的最佳要素。只要在整個驗證流程中可以使用相同的聲明,開發人員就能在完整性和效率方面體會到ABV的巨大優勢。

用SystemVerilog實現ABV

SystemVerilog語言標準及其諸多優勢使聲明和ABV的採用變得非常方便。SystemVerilog包含很多豐富的聲明指令,這些指令可以實現複雜設計行為的快速定義,即使是包含多訊號的重疊型臨時序列的行為也能實現。如圖2所示,SystemVerilog聲明性能包括:

* 基本的布爾表達式


* 具有特殊或任意時延的序列


* 在正常表達式上做到匹配

圖2:SystemVerilog可以提供寬
範圍的聲明指令。


* 在規定條件下可以使聲明失效


* 功能覆蓋點的定義

SystemVerilog聲明可以根據相關設計在RTL程式碼中定義。例如,針對if和else分支定義的不同聲明可以只在相應分支啟動時才進行評估。這樣可以極大地簡化聲明規範,因為啟動/失效條件可以來源於RTL程式碼,無需在聲明中重新定義。SystemVerilog聲明也可以在獨立的文件中定義,然後‘加進’RTL程式碼。大多數時候設計工程師在RTL中定義聲明,而驗證工程師在測試平台程式碼或其它獨立文件中增加額外的聲明。

SystemVerilog提供了非常豐富的基於聲明的函數,包括:


* 在指定時間採樣的$fell、$rose和$past


* 向量分析函數,如$onehot和$countones


* 嚴重級別系統函數,如$fatal、$error、$warning和$info,用於分類聲明錯誤並採取適當的措施


*聲明控制系統任務,如$asserton、$assertoff和$assertkill。針對層次結構中的單個聲明或所有聲明,這些函數可以在初始化或模擬過程中的任意時間點使聲明失效。

下面是一個SystemVerilog聲明的例子


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


property p_handshake;


int v_data;


@ (posedge clk) disable iff (!reset_n)


($rose(req), v_data=data) |=>


ack ##[*1:5] data_out==v_data;


endproperty : p_handshake


?


ap_handshake : assert property (p_handshake) else


$fatal;


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

上述程式碼採用聲明屬性指示定義聲明。該聲明參考屬性p_handshake對特殊序列進行檢查。它在時脈的上升沿對所有訊號進行取樣,只要重置訊號有效,它就使聲明失效。如果設計不在重置狀態,屬性就尋找req上升沿(被證實),並把數據值存進本地變量v_data中。然後屬性會檢查ack是否在下個周期得到證實,該事件發生在data_out和被存v_data相等後的1到5個周期內。如果這個序列發生,聲明就獲得成功通過。如果req一直未被證實,那麼聲明將輪空通過。如果req被證實,但不是在指定順序之後,那麼聲明失敗。

SystemVerilog聲明可以執行於模擬和形式屬性分析內,目前已獲得許多EDA供應商的支持。因此SystemVerilog只需一次性滿足定義聲明的關鍵要求,就能保證多家供應商的多個工具採納這些聲明。另外,SystemVerilog聲明可以對應任何RTL設計,包括SystemVerilog、老版Verilog甚至VHDL。

SystemVerilog聲明還能滿足ABV的教育方面要求。目前已經出版了多本解釋SystemVerilog語法的書藉,它們提供了許多使用這些聲明捕獲傾向性設計行為的實際案例。其中有本英文版、書名為《SystemVerilog assertions Handbook》將在2005年9月份在日本上市。

最後,SystemVerilog能夠很好地用來為公共類型行為定義聲明檢查器。例如,新思曾為一些通用設計元件(如FIFO、記憶體、狀態機、互斥訊號和請示-確認握手等)提供了50多個SystemVerilog檢查器的單元庫。該庫為初次使用聲明者提供了良好的學習途徑,可以縮短訓練時程。

本文小結

除了其它一些功能外,SystemVerilog以聲明的形式提供了豐富的指令集來捕獲預料之中的設計行為。近年來在一些最重要的EDA語言標準的強大支持下,有更多的設計與驗證工程師願意定義聲明並使用ABV。這樣做後,他們可以在更短的時間內更徹底地驗證SoC設計,進而以高品質產品打開市場之門。

作者:Ben Cohen


VHDLCohen出版社

Thomas L.Anderson


新思科技驗證部門技術行銷總監





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


EE人生人氣排行
 
返回頁首