介紹

功能覆蓋、激勵生成和運行管理是當今功能驗證的三大相互關聯的任務。其中，功能覆蓋率可以說是最重要的，主要是因為覆蓋率收斂是tape的主要標準。覆蓋率衡量標準提供了關鍵的反饋。如圖1所示，覆蓋率模型應包括端到端功能覆蓋、主要接口的事務覆蓋、關鍵RTL結構的結構覆蓋和基本代碼覆蓋。

基于斷言的方法有助于發現bug，反饋回歸環境的質量。這種方法不僅可以由驗證實現，設計可以通過以斷言的形式描述他們對設計內部操作的深入行為來提供check。

斷言和功能覆蓋實際上是同一枚硬幣的兩面。兩者都在寄存器傳輸水平（RTL）設計中提供詳細的觀察點。

指南

遵循指南可以使設計更容易。首先，將斷言放在RTL代碼中，以便它們可以與RTL代碼一起管理、更新和重復使用。接下來，通過適當的注釋將斷言與RTL分開；一些公司建議將ifdef/endif放在斷言周圍，以便將它們排除在實現流程中的工具之外。

斷言不必復雜。事實上，根據我的經驗，簡單的斷言通常和復雜的斷言一樣有用，包括捕捉復雜的bug。在接下來的部分中，我將探索如何將SystemVerilog 斷言屬性和覆蓋屬性置于在設計上。

首先，用于表示特殊信息的寄存器應遵守預定義的合法值（gray_code、odd_parity、even_parity、one-hot）。例如，下面的寄存器聲明要求bus_state是one_hot編碼的，int_mask中的單個位是相互排斥的，hdl_cmd將只具有合法值。設計或者驗證可以捕獲它們，以確保它們被功能驗證所涵蓋。

接下來，當寄存器用作計數器時，它們應該相應地存在概念（最小、最大、范圍、值、遞減、遞增、上溢出、下溢出等）。例如，在下面的寄存器聲明中，我們希望確保hdr_adr在1到26的范圍內。對于bus_cnt，它不應該下溢和溢出。對于計數器來說，了解他們是否達到了高水位可能很有趣。驗證團隊可以進行更多的覆蓋分析，但需要知道這些計數器的位置，這些指針通常可以在覆蓋屬性中找到。

接下來，當寄存器用作計數器時，它們應該相應地運行（即與最小、最大、范圍、值、遞減、增量、增量、下流、溢出等的所有參數一致）。例如，在下面的寄存器聲明中，我們希望確保hdr_adr在1到26的范圍內。對于bus_cnt，它不應該下溢和上溢。對于計數器來說，了解他們是否達到了高水位也可能很有趣。驗證團隊可以進行更多的覆蓋率分析。

此外，重要的控制寄存器（狀態、地址和狀態）應正確復位，并且不應具有X或Z狀態。

在RTL開發期間定期進行檢查。例如，在下面的示例中，當斷言cmd_write時，將發生DMA傳輸。然而，用戶沒有檢查cmd_ready。他假設當cmd_write被采樣時，命令處理已經準備就緒。

下面的第一個斷言屬性有助于確保在斷言cmd_write時，信號cmd_ready為真。第二個斷言屬性確保xdma傳輸將在cmd_write之后發生。另一個覆蓋率屬性可以評估成功的DMA傳輸。

當綜合指令與case語句一起使用時，確保假設對指定的case語句成立，并報告任何潛在的仿真/綜合不匹配。對于full_case指令，至少有一個case項為真，對于parall_case指令，最多有一個case項為真。例如，在下面的示例中，帶有“X”賦值的默認分支用于幫助綜合優化。永遠不應該達到它。可以添加斷言屬性來檢查此場景。然后，可以使用仿真和形式驗證來驗證它永遠不會被執行。與此同時，我們可以有一個覆蓋率屬性，可以獲取一些關鍵但罕見的條件。我們希望確保它們已經通過仿真進行了檢查和覆蓋。

有時候，只有一個分支變量應該是真。例如，在下面的示例中，應始終斷言其中一個信號（s0、s1或s2）。我們可以用one_hot屬性來驗證這一點。同樣，覆蓋屬性可用于捕獲控制信號上的臨界值變化，例如當pkg_type從`CTRL更改為3'b111時。控制語句為定義這些覆蓋屬性提供了一個特別好的位置，因為所有控制信號和參數都在本地可用。

當設計團隊集成所有SoC模塊進行芯片級仿真時，這些模塊通常無法相互通信。為了及早發現這些模塊間通信問題，添加了協議監視器來檢查片上總線和標準接口。在仿真過程中，協議監視器確保模塊與其外部接口正確通信。通過收集統計數據和覆蓋信息，這些監視器衡量驗證環境的有效性。

隨著模塊的復雜性增加，內部通信方案也越來越復雜。斷言對于驗證這些模塊內接口很有用。

覆蓋率和數據流統計對內部接口和外部接口一樣重要。此類信息證實了通過接口的數據流，并突出了任何潛在的“瓶頸”。

例如，在下面的數據傳輸波形中，我想確保數據有效信號斷言足夠長的時間（兩到四個周期），并且當斷言有效時數據總線是穩定的。

接下來，在下面的握手數據傳輸波形中，我想確保數據有效信號的斷言時間足夠長，以便在斷言有效時數據總線是穩定的，并且每個有效的斷言后都有一個ack。

計算資源、系統片上總線、互連、buffer和存儲器是邏輯結構，通常由仲裁和復雜的控制邏輯共享和控制。在為設計創建驗證環境時，團隊傾向于首先關注整體規格。相反，它們不會強調這些資源控制邏輯的邊界情況。我看到許多回歸環境在這些關鍵場景提供的覆蓋率非常低。因此，有問題的場景沒有被發現，包括重新流片成本高昂的故障。

在仲裁資源共享的控制器中，根據優先級、權重或credit方案生成request和grant信號。我想確保仲裁方案正確，資源（總線、互連、內存）一次只由一個master處理，并在再次分配之前取消分配。最好用參考模型方法檢查這種類型的結構。可以利用Accellera OVL庫中的仲裁檢查器。預定義的仲裁包括優先權、公平或輪訓、FIFO和LRU。

ovl_arbiter檢查器可以在RTL代碼中實例化。它確保不應在沒有請求的情況下發放grant，并且在一個周期內只聲明一項grant，并在請求后[min_cks:max_cks]指定的時間窗口內grant。除了檢查仲裁方案外，仲裁員checker還有一套全面的cover point和cover group，如cover_req_granted、cover_req_aborted、time_to_grant、concurrent_requests等。還可以添加額外的斷言屬性，以確保request和grant信號表現良好。例如，仲裁checker假設請求將保留，直到它被grant。我們可以為每個通道生成斷言屬性，如下所示。

總線橋、dma控制器和路由器等數據傳輸設備將數據包從一個接口傳輸到另一個接口。在系統級仿真環境中，數據完整性錯誤不容易觀察到。只有當損壞的數據到達scoreboard時，它們才會被檢測到，或者在仿真結束時被標記為丟失。使用斷言屬性，可以沿著數據傳輸路徑檢查它們。它們不應該丟失或損壞，如有必要，我們還可以確保它們遵循先入先出規格，沒有任何更改。與其手動創建數據完整性斷言，不如利用Accellera OVL庫中的fifo斷言檢查器。fifo檢查器確保模塊中事務通過模塊的數據傳輸不會損壞。對于具有多個輸入和輸出端口的模塊，例如N-to-M總線矩陣，可以使用OVL多端口fifo檢查器。同樣，fifo檢查器還有一套全面的cover point和cover group，如cover_enqueues、cover_dequeues、cover_fifo_full、cover_fifo_empty、cover_simultaneous_enq_deq等。它們可用于評估設備的數據流。也可以添加其他斷言屬性。

出于驗證目的，我們將有限狀態機（FSM）分為兩類：接口FSM和計算FSM。接口FSM使用具有明確timing要求的I/O信號。接口FSM的例子有總線控制器、握手FSM等。計算FSM不涉及具有明確定義的timing要求的信號。重要的是不要根據FSM的RTL編寫屬性。如果設計師誤解了需求或在編寫RTL時犯了錯誤，FSM將是錯誤的。

通常，接口FSM的規范來自協議文檔和波形圖。斷言屬性應來自原始規范。他們將確保FSM在時間段內正確采樣輸入信號，并在輸出時序規范內斷言響應信號。通常，計算FSM的規范來自控制流圖，這在工程文檔和標準規范中很常見。為了提高性能和/或簡化實現，流程圖可能會被劃分、扁平化、重新管道化成多個FSM。我們可以捕獲具有斷言屬性的流程圖行為創建了一個“可執行”規范。

斷言屬性可用于捕獲流程圖中的控制決策、狀態跳變和操作序列。在下面的示例中，流程圖來自原始規范。

結論

在覆蓋率驅動的驗證方法中，捕獲錯誤和衡量進度的能力同樣重要。幸運的是可以利用用斷言捕獲錯誤以及在設計中提供深入的結構覆蓋。通過使用覆蓋屬性和斷言庫，你可以以很少的增量努力完成這項工作。

最好的建議：在為設計開發斷言時考慮覆蓋范圍。這是在回歸環境中實現全面的錯誤檢測能力和結構覆蓋率的第一步。

審核編輯：劉清