眾所周知，驗證任務在數字IP的設計以及SoC的設計中占有重要地位。 RTL代碼和功能覆蓋率的目標是達到100％，從而最大限度地縮短獲得它的時間。最廣泛使用的方法是基于通用驗證方法（UVM）隨機約束測試（系統Verilog或 e 語言），允許在相對短的時間內構建復雜的測試，同時強調RTL代碼和跟蹤功能覆蓋。一些驗證工程師還使用正式的方法來驗證塊的專用部分，例如標準接口，從而完成IP的驗證。

本文將介紹基于正式方法的數字IP驗證的不同方法，通過定義屬性詳盡地驗證功能。正式方法具有避免開發測試臺的優點。這一新流程已在數字IP設計過程中使用，并已證明可顯著縮短驗證時間。

通用驗證流程

目前，用于驗證數字IP和片上系統（SoC）的最常用流程是基于UVM，通過使用第三方提供的驗證組件（VC）或非標準時從頭開發使用協議。然后用記分板完成測試平臺以進行自我數據檢查，斷言用于驗證設計的特定部分，覆蓋用于跟蹤功能覆蓋。在過去幾年中，正式驗證已經開始用于SoC和IP的驗證流程。在SoC中，形式驗證在SoC外圍設備和焊盤之間的連接驗證中變得非常普遍，主要是當多路復用方案由連接到減少數量的焊盤的多個外圍設備形成時，這增加了需要驗證的組合。有時，在IP驗證中，正式方法用于檢查總線協議接口和寄存器訪問策略。

現在，關注數字IP的驗證，我們可以總結如圖所示的流程1.當第一版RTL準備就緒時，良好驗證流程的第一步從驗證和測試計劃的定義開始。在這個階段，我們將定義我們想要檢查的功能和測試的框架。

下一步是開發UVM測試臺;自定義UVM塊用于檢查特定的IP功能，而第三方UVM VC則實例化并綁定在RTL上。

此時，我們可以根據驗證計劃開發UVM測試。每個驗證工程師需要牢記的第一件事是測試必須是自我檢查;必須使用記分板，檢查器和斷言自動檢查驗證計劃中列出的任何點。然后，廣泛使用覆蓋結構可以量化測試的好壞。

圖1：數字IP的通用驗證流程

有時，此流程可能包括形式驗證。在任務的某個階段，有人可能決定通過使用基于斷言的驗證IP（ABVIP）和通過編寫斷言通過有限狀態機（FSM）實現的精確功能來檢查IP的特定塊，例如總線協議接口。

我們知道，驗證任務是一個迭代過程，有兩個主要的環回：

RTL錯誤修復

功能和代碼覆蓋

每當我們發現功能規范與IP行為不匹配時，我們就會向設計人員發出可能的錯誤信號。這意味著需要修改RTL并發布新的固定版本?，F在，進行回歸自檢測試（即使最初是部分測試）也是一個關鍵點，它允許我們驗證RTL代碼沒有回歸，當然，錯誤已經修復。這種環回也可以來自形式驗證。

當開發了足夠數量的測試時，測量功能和代碼覆蓋率是一個很好的做法。像往常一樣，功能和代碼的目標是100％，但我們必須考慮到達它的時間。如果我們想要最小化時間，同時保持100％的目標，我們必須改進驗證的方法和流程。來自正式世界的一個好建議是代碼不可達性分析，它有助于發現無法訪問的RTL部分，并且可以從整體代碼覆蓋率中刪除。

一個好的經驗法則：'如果我沒有運用代碼的一部分，很可能是那里存在錯誤。'因此，我們花了很多時間才能刺激未覆蓋的代碼，但知道某個部分無法訪問可以讓我們節省時間和精力。

接下來，我們將描述一個新的流程，其主要目標是縮短用于驗證數字IP的時間。保持覆蓋目標。

新的驗證流程

正式方法是一種詳盡的驗證，當它是適用時，它使人們能夠在更短的時間內和每種可能的條件下檢查塊的功能。對于常見的動態模擬，這有時是不可行的。

目前，有幾種工具可以鏈接到正式引擎，這些工具已經足夠成熟，可以使圖1所示的驗證流程變為如圖2所示的內容。 。

主要的變化是將形式驗證作為流程的第一步。真正的第一個檢查是對死代碼和未初始化寄存器的分析。這是一項零工作任務，因為不需要額外的代碼，并且它只需要使用Formal工具編譯RTL。隨后的反饋可能非常有用，因為它可以讓我們徹底清理RTL代碼，突出顯示從未到過的部分，以及列出可能導致'X'傳播的未初始化觸發器

毫無疑問，通過使用專用的基于斷言的VIP（ABVIP），可以在短時間內完全驗證諸如微處理器總線接口之類的標準協議。 Formal流的這些驗證組件基于描述協議的斷言。驗證工程師將專注于失敗屬性的調試，而無需花時間在測試平臺和房地產開發上。通過使用UVM流，我們可以在幾天而不是幾周內完全驗證接口。

可以通過編寫自定義屬性來驗證IP的特定塊，以驗證已實現的功能。可以使用新的選項，例如引入具有與UVM 記分板相同的眾所周知的概念的Formal 記分板，但是利用了Formal引擎的強大功能。它可用于驗證FIFO，通常用于處理數據路徑流但不是算術數據路徑的每個塊（例如加法器，乘法器）。

如今，主要的EDA公司制作了基于Formal流程的工具，這些工具使用時髦的技術詞匯：'APP'。這個概念是為“特定功能”的調試提供“隨時可用”的環境。這些APP自動生成斷言，并允許驗證工程師專注于調試RTL。

最有用的APP之一是用于驗證配置寄存器的訪問策略的APP。通過Formal流程，我們可以詳盡地驗證所有寄存器，尤其是最難驗證的狀態位，因為它們通常取決于HW狀態或特殊輸入條件。通常，流程基于IPXACT，然后也可以在設計開發的其他步驟中重復使用。此外，在這種情況下，這種驗證可以節省很多時間相對于'經典'UVM隨機約束方法。

圖2：新數字IP的驗證流程

可用APP的數量正在快速增長，這將允許將驗證任務從動態移動到靜態，從而改善覆蓋范圍并縮短驗證時間。當然，正式流程有一些局限性，目前無法用于驗證所有內容;當要分析的狀態數（即“形式復雜性指數”）太大時，引擎無法收斂并徹底分析代碼。這是一項挑戰，可以通過引入新算法和計算能力在不久的將來克服這一挑戰。無論如何，我們不能聲稱正式流程將超過動態模擬，原因很簡單：使用'假設'語句會引入隱藏錯誤的風險，如果屬性成功，則有可能如果在實際應用程序中未滿足假設條件，則RTL行為將是錯誤的。這完全類似于靜態時序分析（STA）和門級仿真：如果時序約束錯誤，STA表示設計中沒有時序違規，但最終設計不適用于某些極端情況。動態模擬允許我們驗證形式'假設'語句以及STA約束。

由于這些原因，驗證流程的下一步需要進行UVM模擬，提升通過正式步驟中成功的屬性斷言，現在也可以在動態模擬中重復使用。在這個新流程中開發的測試數量將少于使用圖1所示流程開發的測試數量，因為我們可以專注于正式流程中發現的部分，并為使用它分析的部分開發有限的測試。

圖2所示流程的最后幾個步驟基本相同：我們運行不可達性分析以刪除無法訪問的代碼，然后分析代碼和功能覆蓋。

結論

使用形式驗證方法作為流程的第一步，代表了一種不同的方法，可以更好地利用正式的好處和有效性：零時間用于構建測試平臺和RTL的詳盡驗證。此外，使用這種方法的學習曲線比UVM更快;用于編寫斷言的語言是緊湊的（PSL或SVA）并且易于使用。最困難的工作是用人類語言定義最能描述我們想要證明的功能的正確屬性。轉換為SVA或PSL變得簡單易行。

在RTL驗證的早期階段使用形式化方法的主要優點是使用更清晰的代碼進入動態模擬，其中許多功能已經過徹底驗證并且修復了一些錯誤。由于正式方法允許我們縮短在驗證功能上花費的時間，因此可以大大縮短整體驗證時間。