使用形式驗證技術作為片上系統 （SoC） 設計的主流技術，終于成為消除驗證差距的公認方法。最近的一項調查表明，26% 的芯片設計項目現在使用基于斷言的正式驗證 （ABV）。然而，這種經典模擬的替代方法的承諾需要很多年才能開花結果，而且仍然只有高級驗證環境才能包含它。為什么會這樣？到目前為止，我們可以從它的使用中學到什么，以便將其提供給整個 SoC 工程社區？

SoC 塊驗證碰壁

自問世以來，SoC 設備一直是開發團隊的驗證噩夢。雖然現在驗證完整的 SoC 最好留給仿真和快速原型設計系統來完成，但即使是這些設備上的較大塊也已經超出了純仿真環境。

仿真、更快的模擬器、關鍵測試的驗證知識產權 （VIP） 以及通用驗證方法 （UVM） 的出現都有助于緩解這種情況。盡管如此，驗證要求仍超過了基于模擬的環境中的可用處理時間。

形式驗證通過使用針對特定需求的自動化“應用程序”有助于改進塊驗證，否則需要大量的模擬工作。檢查標準通信協議的正確操作、確保關鍵連接和寄存器操作、分析域重置時的正確啟動序列以及許多其他任務現在都由這些解決方案處理。

然而，我們才剛剛開始挖掘形式驗證的真正威力。它的許多使用問題已被消除，使我們處于可能是全新驗證時代的最前沿，因為該技術已部署用于核心驗證。

形式驗證：如果這么好，今天在哪里？

首先，快速回顧一下形式驗證技術，為什么它有可能創造這種根本性轉變，以及今天是什么阻止了它。

硬件仿真的工作原理是通過一系列有意義的狀態循環一個硬件描述語言 （HDL） 代碼塊來演示其操作。此狀態序列由輸入激勵（設備輸入上的一組事件的 HDL 描述）驅動，旨在探索正確的狀態以識別操作問題。

這種方法引出了一個問題：如果我們知道代碼塊可以進入的所有狀態以及狀態間轉換，那么我們不能簡單地詢問有關代碼操作的問題以確保其正確嗎？這將避免必須編寫許多行刺激來嘗試使代碼塊進入正確的信息承載狀態。這是形式驗證工具使用的方法。

這種基本方法可以轉變為許多有用的應用程序。例如，如果可以根據設計代碼的一個方面和要檢查的驗證場景自動創建要問的問題，則可以創建用于驗證目的的自動化應用程序。這將不需要用戶編寫問題。如果正式工具可以用最少的輸入演示特定的狀態序列（例如狀態機操作），那么設計工程師就可以理解他或她的代碼如何執行，從而揭示可能的錯誤。

當工程師自己提出問題時，形式驗證的真正威力才得以發揮。這需要使用斷言編寫問題或屬性，并在稱為基于斷言的驗證或 ABV 的過程中應用于設計。

當然，這種高級描述掩蓋了 ABV 的問題，包括存儲這么多信息的工具的容量和性能要求已經通過最新技術得到解決。

兩個問題仍然是 ABV 廣泛使用的障礙：

斷言的創作，通常使用 SystemVerilog 標準語法，可能很復雜且難以可視化

對驗證進度或覆蓋率的理解很難與其他驗證方法的理解和對比

盡管在這兩個方面都取得了進步，但還需要更多的努力來降低學習曲線，從而使 ABV 得以普遍擴散。

ABV 應用程序

在驗證過程中應用 ABV 有兩種常用方法。首先是檢查特定的極端案例類型的問題，這些問題通常需要花費大量精力來構建模擬測試平臺來分析問題。第二個是對塊進行更一般的檢查，無論是結合模擬還是獨立檢查。

形式驗證的第一個使用模型很有價值，可以在驗證計劃中減少合理的百分比。第二個模型有可能改變特征驗證過程，節省大量時間和資源支出，同時增加發現設計中每個錯誤的整體潛力。已經有一些行業部門在第二種模式中廣泛使用 ABV。其中包括汽車和航空電子產品，其中高質量和可靠性是一個因素。

在組合仿真-形式驗證流程中，如圖 1 所示，通常使用仿真進行一般操作分析并“感受”設計的行為和性能。此外，還有一些功能更適合模擬，例如數學數據處理或信號處理。然而，形式驗證非常適合控制或數據傳輸種類的功能，如有限狀態機、數據通信和協議檢查。此外，確保某些類型的驗證場景，例如安全檢查（例如，某項活動是否會發生），也是該技術的最佳選擇。這些代碼和場景示例通常需要很高比例的驗證資源。

斷言創作改進

與 UVM 推動模擬測試臺創建的分層方法相同，新技術正在出現，將抽象引入斷言創作。這些抽象通過掩蓋斷言細節來降低復雜性，同時允許工程師考慮驗證任務而不是斷言的個別特征。

例如，OneSpin 解決方案的 Operational Assertions 是一個 SystemVerilog 庫，它允許正式測試以類似事務時序圖的方式表示，與驗證工程師廣泛認可的高級 UVM 序列不同。Breker Verification Systems 的基于圖形的測試序列，現在由 Accellera Portable Stimulus 標準委員會考慮，是另一種抽象形式，也可以應用于斷言創作。

這些技術在簡化形式測試應用的同時，具有提供可識別且更自然的輸入方案的優勢，允許工程師通過消除一些形式驗證之謎來與正在進行的驗證過程相關聯。

常見的覆蓋模型

簡化斷言只是難題的一部分。該過程的另一端是整理來自各種來源的覆蓋率信息，以了解總體驗證進度，無論使用何種工具。模擬過程仍然主要集中在一種或另一種代碼覆蓋上，并包含一些功能覆蓋。形式驗證覆蓋側重于斷言（所謂的“斷言覆蓋”），無論它們是否被執行，它們是通過還是失敗，或者確實它們通過一個警告（例如，有界證明，例如“代碼在一定數量的時鐘周期內通過”）。該信息可以反饋給驗證計劃系統以提供一些有用的數據。

然而，測量正式的覆蓋率，確定由特定斷言測試的實際代碼，是領先的形式驗證供應商感興趣的領域。已經提出了在精度和所需執行資源方面都不同的方案。關鍵是能夠將這些正式模型與模擬模型進行比較，以提供綜合的、有意義的覆蓋率評估。Accellera 統一覆蓋互操作性標準 （UCIS） 委員會專注于這一目標，并提出了可以將兩者進行比較的方法。在這方面需要做更多的工作，但很明顯，一些形式驗證供應商擁有允許計算合理的進度度量的解決方案。

模擬風格調試

以對以仿真為中心的工程師有意義的方式調試形式驗證代碼，在很大程度上已被許多形式驗證供應商解決。大多數工具可以在斷言失敗的情況下輸出“見證”。也就是說，導致斷言失敗的仿真波形形式的一系列事件。事實上，包括 OneSpin 在內的一些供應商可以輸出模擬測試，允許在模擬器中重現故障以供進一步研究。

破解主流ABV代碼

很明顯，ABV 的使用開始成為主流。ARM 和 Oracle 都宣布了 ABV 在其環境中的全部功能，并指出它現在在他們的項目中被大量使用。

解決 Assertion Authoring、Collated Coverage 和 Simulation-centric Debug 這三條腿的問題，并將其與對形式驗證擅長的設計領域和場景的清晰理解相結合，將推動這種方法成為 SoC 驗證的主流。一旦發生這種情況，將對未來的設計質量和開發進度產生巨大影響。

審核編輯：郭婷