多年來，設(shè)計(jì)重用方法為半導(dǎo)體 IP （SIP） 創(chuàng)造了一個(gè)市場(chǎng)，現(xiàn)在有了正式的技術(shù)，就需要斷言 IP （AIP）。其中，每個(gè)AIP都是硬件設(shè)計(jì)中用于檢測(cè)被測(cè)設(shè)計(jì)（DUT）中的協(xié)議和功能違規(guī)的可重用和可配置驗(yàn)證組件。LUBIS EDA 專注于正式服務(wù)和工具，因此我收到了有關(guān)他們開發(fā)這些 AIP 和檢測(cè)高風(fēng)險(xiǎn) IP 中極端情況錯(cuò)誤的方法的最新信息。

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

基于仿真的驗(yàn)證基于形式的驗(yàn)證

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

屬性生成器流

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

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

總結(jié)

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

生成的斷言 IP （AIP） 涵蓋了所有可能的場(chǎng)景和刺激，以保證設(shè)計(jì)無錯(cuò)誤。這種方法對(duì)于幫助您驗(yàn)證邏輯塊甚至復(fù)雜的 IP 核也非常有用。

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