多年來，設計重用方法為半導體 IP （SIP） 創造了一個市場，現在有了正式的技術，就需要斷言 IP （AIP）。其中，每個AIP都是硬件設計中用于檢測被測設計（DUT）中的協議和功能違規的可重用和可配置驗證組件。LUBIS EDA 專注于正式服務和工具，因此我收到了有關他們開發這些 AIP 和檢測高風險 IP 中極端情況錯誤的方法的最新信息。

在詳細介紹 LUBIS EDA 使用的方法之前，讓我們先回顧一下基于仿真的驗證與形式驗證有何不同。通過仿真，工程師正在編寫激勵來覆蓋設計的所有已知狀態，希望覆蓋范圍足夠高。通過形式化驗證，形式化工具可以找出設計中從輸入到輸出的所有可能路徑。

基于仿真的驗證基于形式的驗證

LUBIS EDA 使用的一種方法是其內部屬性生成器，它在電子系統級 （ESL） 而不是寄存器傳輸級 （RTL） 上工作。這使他們能夠提供更快、更高質量和更高效的驗證服務。屬性生成器使您能夠在幾分鐘內從抽象模型轉換為 AIP，這是驗證效率的巨大飛躍。該流程如下所示：首先，抽象模型由屬性生成器解析和分析，然后將形式驗證 IP 創建為系統驗證斷言 （SVA）。這些斷言檢查您的設計意圖并提供功能行為的完整覆蓋。

屬性生成器流

ESL 級別的抽象模型是用 C++ 或 SystemC 編寫的，可以模擬以驗證其行為，屬性生成器會讀取該代碼并為你生成 AIP。然后，通過大型語言模型 （LLM） 支持的細化步驟將斷言綁定到您的 RTL 設計，以更快地獲得結果。斷言是人類可讀的，并且是按構造更正的，因此您不需要有專門的斷言評審會話。在此流中運行您最喜歡的正式工具，然后查找任何失敗。

應用這種 AIP 方法的一個示例是加密哈希函數，例如 SHA-512。下面顯示了左側的 C++ 模型和右側生成的涵蓋模型部分的屬性。

總結

這種方法如何使形式驗證更加高效？驗證工程師可以通過手動編寫斷言來應用形式化方法。手動編寫形式斷言需要時間、容易出錯并且需要專業知識，因此自動執行此步驟可以節省您的工程時間和精力。

生成的斷言 IP （AIP） 涵蓋了所有可能的場景和刺激，以保證設計無錯誤。這種方法對于幫助您驗證邏輯塊甚至復雜的 IP 核也非常有用。

您的項目是否面臨巨大的時間壓力，您想利用這種高效方法的優勢嗎？那么您應該考慮 LUBIS EDA 的咨詢服務，以實現一流的 SoC 設計質量。如果您想自己執行項目，還有一些形式驗證課程可以幫助您更快地工作。LUBIS EDA 的網站也有許多關于使用形式驗證技術的有用博客文章。