Chip123 科技應用創新平台

標題: SoC 環境中的 SystemVerilog 斷言 [打印本頁]

作者: masonchung 時間: 2008-12-9 02:11 PM
標題: SoC 環境中的 SystemVerilog 斷言
Bindesh Patel，技術行銷經理，Springsoft公司

驗證工具與方法兩者都在演變並經歷了革命性的變化，並且在追隨摩爾定律方面，兩者都同樣重要。藉由取得第三方的矽智財權 (IP)——這是開發團隊內部採用的一種各個擊破法（divide and conquer approach）——和增加更多設計人員來實現複雜的 SOC 設計。另一方面，驗證必須把大型設計當作一個整體來對待。這個重擔落在底層的驗證工具與相關方法的肩上，它們必須能夠“模擬”該設計的模型，這經常是在不同的抽象級來進行的。幸運的是，基於斷言的驗證（assertion-based）實現了一種革命性的方法變革，它藉由為驗證環境添加觀察能力（結果檢查）和測試（實際測試的開發），從而化解了上述日益沉重的負擔。

結果檢查方法
傳統上，有幾種方法可以用來確定模擬模型的行為是否符合預期，其中一些方法檢查模擬期間的正確性，而另一些則作為後模擬的批次處理（post-simulation batch process）過程。以下是一些例子：

• 對照參考模型（模擬運行時）進行檢查。參考模型通常處於更高的抽象級，與設計模型平行運作，並且工作狀況的比較是即時發生的。
• 與預期工作狀況比較（後模擬）。它假設已在先前保存了“黃金（golden）”結果，最可能是來自另一次模擬運行，並有可能是來自更高抽象級的模型模擬。
• 斷言（後模擬運行時或模擬運行時）。斷言是一些代碼片段，它們簡潔地表達了所期望的行為或不期望的行為，並且經常是以 SystemVerilog Assertions (SVA) 或 PSL 等特定的語言來撰寫的。模擬器把這些描述與模型一起讀取進來，並在運行時執行檢查。當以批次處理方式部署時，後模擬檢查器（Post-simulation checker）的效率非常高。

斷言介紹
斷言提供了一種設計規格的簡潔描述，該規格與 RTL 設計實現是分離的。可利用 Verilog、VHDL 或 C 等傳統語言來為斷言編碼，並且這種狀況也已持續若干年了。但是傳統語言可能需要很多行的代碼以及艱難的編程“軟體技巧”。例如，由於某個斷言可能並且經常地跨越多個時鐘週期，因此Verilog“叉形（fork）”區塊的外顯式使用（explicit use），需要描述一項在所有時鐘週期都必須要檢查的斷言。像是SVA 等特定語言就是被設計成可以更簡潔的方式來描述這一類的斷言。

撰寫斷言
與利用硬體描述語言 (HDL) 來編碼的設計相同的是，斷言的最佳描述方式是階層式（hierarchica）的。這可提升編碼的容易性、理解性、再使用性（reuse）等等。
• 位於最低級別的是設計信號的布林運算式，它們成為各個序列的建構區塊“元件”（building-block "components"）。
• 然後是序列，它們是布林運算式列表，而這些布林運算式則是按時間遞增的線性順序排列。
• 序列之上是屬性（Property），它們以各種方式把序列結合起來。
• 位於最高級別的是指令（例如斷言），它們指出要對屬性做些什麼。

以下的例子說明了這種階層式建構區塊的方法。
sequence c_l;
@(posedge clock) (bus_mode == ‘INCA) && PC_load;
endsequence

property e_INC;
@(posedge clock) e_l |-> e_r;
endproperty

CF_COVER: cover property (add_overflow);
INCPC: assert property (e_INC);

高效率的斷言方法
對斷言的檢查可以是動態的，也可以是靜態的（形式上的），這次的討論則將側重於動態的（模擬）檢查。多數商用模擬器皆已經可以支援或接近支援標準的斷言語言。模擬器在簡單的斷言檢查方面一般很好用，但“支援”資料（除錯與分析工作所需的資料）的運行時擷取可能會嚴重地影響模擬器的性能。斷言的時序（temporal）本質可能會產生並行的多次嘗試與線程，這會顯著地增加模擬工作的運行時間與記憶體用量，來擷取在稍後進行除錯與分析工作時所需的支援資料。把大部分工作轉移到除錯系統（而它又可被優化，以便只計算相關資料），就可減輕運行時負擔。這樣，除錯系統自動依照需求產生支援資料，並且模擬器能以更高的效率執行檢查。理想情況下，除錯系統還會對照模擬期間捕獲的信號資料來檢查斷言，因此模擬器不需要為了支援斷言檢查而執行額外的工作。

在斷言開發過程中，當斷言在撰寫之際，就可以即時而快速地檢查斷言，這種能力也是很有用的。替代方法是在斷言代碼每次有小的變化後，反復進行模擬，這可能非常耗時。

在基於斷言的驗證環境中除錯
由於斷言失敗會為除錯會帶來許多挑戰，因此除錯系統需要包含以下的能力：
• 斷言源碼除錯，並且具有在屬性、序列、事件和設計方案之間的追蹤能力；
• 斷言組件的導航，以及先進的搜尋與過濾；
• 把來自模擬器的斷言結果擷取到資料庫中，以便後模擬的除錯；
• 根據擷取到的信號資料對斷言進行離線檢查，即不依賴模擬器；
• 以波形呈現的斷言視覺化，及在源碼上下文內的斷言視覺化；
• 適當地處理局部變數，使得工程師能迅速看到自己正在除錯的特定嘗試或線程的局部變數的值；
• 標籤機制（tagging mechanism），使工程師能迅速跳到影響某個斷言的設計信號。

斷言除錯
一旦設計描述、斷言源碼以及信號和斷言結果被載入到除錯器中，現代除錯器中的所有標準能力均可應用到除錯斷言源碼和結果。

斷言代碼內部以及斷言代碼和設計代碼之間的追蹤是一項關鍵要求。在除錯某個失敗時，工程師需要能從斷言指令敘述跳至屬性描述，然後跳至序列描述等等，沿著階層一直跳到設計信號。這就創造出了一個直覺式的過程，可以迅速地沿著斷言的建構區塊階層上下追蹤，該階層的對齊方式就是工程師對斷言的思考和編碼方式。

傳統的除錯視圖必須延伸到可與斷言一起工作。

利用適用於斷言的記法（notation），在傳統的波形視圖中顯示斷言檢查結果。一些先進的除錯工具包括若干機制，以便在源碼上下文內實現結果的視覺化。

儘管傳統的除錯視圖為基於斷言的方法提供了一些價值，但仍需要全新的能力來滿足斷言的特殊要求。在基於斷言的驗證環境中，在斷言失效點開始除錯是很常見的。在波形視圖中目測失效是不切實際的。電子試算表等更靈活的視圖使工程師能對相關資料進行客製化和排序，以便迅速地找出失效點。這張表格式視圖可有效充當某個斷言驅動的流程的“駕駛艙（cockpit）”。

自動化
現在，我們已說明了源碼追蹤、波形等傳統的除錯能力如何應用於斷言。除了這些基本要求以外，還有許多機會來實現自動化領域的源源不絕的創新，以便因應斷言的獨特性質，以及工程師在除錯斷言失效時所面臨到的挑戰。對斷言失效進行除錯涉及到對結構、邏輯和時間資訊的分析。工程師必須從源碼跳至波形來獲得正確的資料，然後再以人工的方式來計算屬性敘述中的各個值。這個過程很耗時，易出錯，並且包含許多人工步驟。

為了實現斷言失效追蹤與根本原因識別（root-cause identification）的自動化，先進的除錯器均包含分析引擎，以便根據需要，利用追蹤檔中已有的資料來計算屬性敘述中的相關值。除錯器根據源碼來推斷斷言的行為。一旦資料計算完畢，引擎就能自動隨著時間的變化，從失效追蹤至根源（記住：它已瞭解斷言的行為）。就本質而言，引擎自動完成了目前工程師在除錯斷言失效時人工處理的各項任務。
斷言層次的最低級別一般由設計信號的布林運算式組成。分析引擎可能還會分析運算式與子運算式，並自動呈現它們的“值”（“真”或“假”）。迅速檢查出哪個運算式為假的能力可幫助工程師以快得多的速度到達導致失效的設計信號。一旦根源被隔離，就能用標準的和先進的除錯技巧，在設計方案內部追蹤信號。

SpringSoft 公司的 Verdi Assertion Analyzer 自動完成斷言失效的根源分析。

結論
在驗證環境中加進可觀察性及測試，斷言和斷言語言提供了一種簡潔的機制，以便檢查出不希望得到的設計行為。對斷言的檢查可以是動態的，也可以是靜態的（形式上）。動態檢查或者是藉由模擬器完成，或者是藉由後模擬斷言檢查引擎完成，使工程師能迅速地借助斷言來增強自己的驗證流程。幸運的是，先進的除錯器（例如 SpringSoft 公司的 Verdi™ Automated Debug System）已獲得增強，以協助工程師採用基於斷言的方法，這類方法利用了 SVA 等特定的語言。它們還提供經過調整以便適應斷言除錯的分析引擎，後者簡化並加快了確定斷言失效根本原因位置的過程，不論是它在斷言代碼中，還是在設計方案中。

歡迎光臨 Chip123 科技應用創新平台 (http://free.vireal.world/chip123_website/innoingbbs/)