SystemC/C++ 設(shè)計的驗證要求

雖然 SystemC/C++ 編程風(fēng)格已使用多年，但最近出現(xiàn)了一些特定使用模式，它們推動工程團隊采用共同的設(shè)計流程。這包括抽象算法設(shè)計代碼用作高層次綜合 (HLS) 工具的輸入，虛擬平臺模型用于早期軟件測試，可配置的知識產(chǎn)權(quán) (IP) 模塊，等等。

HLS 用于將“大部分為非時序化”的抽象 SystemC/C++ 設(shè)計表示轉(zhuǎn)換為完全時序化的寄存器傳輸級 (RTL) 設(shè)計模塊，該工具已被許多大型半導(dǎo)體和電子系統(tǒng)公司使用。作為一種快速生成具有不同微架構(gòu)的設(shè)計組件，同時快速高效地優(yōu)化算法處理數(shù)據(jù)路徑的方法， HLS 工具特別受歡迎。其在控制邏輯以及具有更詳細時序的一般元器件上的使用，也變得越來越普遍。

圖 1. SystemC/C++ 高層次設(shè)計流程

SystemC/C++ 設(shè)計的驗證主要通過如下方式進行：利用 GCC 等標準軟件編譯器編譯設(shè)計表示，并以與軟件設(shè)計類似的方式調(diào)試代碼。Open SystemC International (OSCI) SystemC C++ 類庫（現(xiàn)已標準化為 IEEE 1666-2011）引入了使用戶體驗更像 RTL 仿真的功能，但仍有許多問題讓 SystemC 代碼的驗證任務(wù)非常復(fù)雜和艱巨，包括調(diào)試、運行時性能和測試復(fù)雜性。該級別的形式化技術(shù)一直很稀少。

常見 SystemC/C++ HLS 流程所用的算法描述常常僅使用 C 或 C++ 代碼。這些描述經(jīng)過測試，以確保算法本身正確運行。SystemC 類庫函數(shù)用于提供 HLS 工具所需的極少硬件細節(jié)，例如基本時序、復(fù)位功能等。綜合工具生成 RTL 代碼，然后將其應(yīng)用于更傳統(tǒng)的設(shè)計細化流程和驗證過程。

設(shè)計驗證分為 SystemC 和 RTL 兩個級別。很明顯，工程師更愿意驗證和調(diào)試原始 SystemC 設(shè)計，而只在綜合后檢查功能等效性，類似于傳統(tǒng)的 RTL 開發(fā)過程。然而，由于缺乏有效的 SystemC/C++ 設(shè)計驗證環(huán)境，工程師們不得不采用更傳統(tǒng)的 HDL 驗證。

隨著工程師提高其設(shè)計方法的抽象級別，驗證級別自然也要相應(yīng)地提高。在 HLS 之前的算法級別，要求直接根據(jù)其規(guī)范驗證設(shè)計，而較少關(guān)注編碼細節(jié)。功能規(guī)范很容易用斷言來表示，因此，使用能夠針對設(shè)計嚴格測試斷言的形式化技術(shù)是一種自然的選擇。新的控制密集型算法，現(xiàn)在用 SystemC 編寫，僅使用仿真特別難以驗證。

西門子 EDA 的 360 DV SystemC/C++ 驗證功能旨在滿足這些要求。

適用于 SystemC/C++ 設(shè)計的360 DV 簡介

西門子 EDA 是西門子數(shù)字化工業(yè)軟件的一部分，其針對 SystemC/C++ 代碼提供的設(shè)計驗證 (DV) 解決方案是 360 DV 形式化驗證產(chǎn)品線的一部分。它支持將廣泛的形式化技術(shù)應(yīng)用于以 C++ 或 SystemC 編寫的、具有不同時序和代碼抽象級別的設(shè)計組件。

適用于 SystemC/C++ 的 360 DV-Inspect 提供了一系列自動化結(jié)構(gòu)檢查、安全檢查和激活檢查，可將這些檢查應(yīng)用于設(shè)計，而無需手動創(chuàng)建斷言。這對于高層次綜合之前的設(shè)計代碼簽核特別有用。該產(chǎn)品包含對 SystemC/C++ 設(shè)計特別有用的檢查，如下所述。

適用于 SystemC/C++ 的 360 DV-Verify 是一款基于斷言的形式化驗證工具，它功能齊全，支持針對 SystemC/C++ 設(shè)計代碼測試綜合斷言。這些斷言可以使用簡單的 C 斷言語句編寫，也可以是完整的 SystemVerilog 斷言 (SVA)，其中包含所有時間、并發(fā)結(jié)構(gòu)體。對 SystemC/C++ 設(shè)計運用時間斷言的能力是該技術(shù)的獨特功能。

圖 2. SVA 配合 SystemC/C++ 設(shè)計使用

作為 360 DV 核心的西門子 EDA 形式化技術(shù)平臺由多個證明引擎組成，這些引擎利用一系列標準和專有算法來提供深入的代碼分析。與其他解決方案相比，它始終表現(xiàn)出高收斂度，另外還提供快速、高容量的操作。該平臺可以處理一系列語言，包括支持輕松設(shè)置和使用的功能。強大的調(diào)試環(huán)境為快速跟蹤設(shè)計或測試問題提供了一條清晰的途徑。

西門子 EDA 解決方案以支持形式靈活性而著稱，可用來解決一系列問題，而且同樣適用于 SystemC/C++ 設(shè)計。這些工具可以在高度交互模式下使用，方便用戶以“假設(shè)分析”的使用方式快速查看設(shè)計如何運行。它們可以構(gòu)成完整的指標驅(qū)動驗證解決方案的基石，并為 SoC 平臺上的 IP 集成提供一種有效的驗證機制。

自動形式化 SystemC/C++ 設(shè)計評估

360 DV 中的全自動功能也可以應(yīng)用于 SystemC/C++ 硬件設(shè)計代碼。在設(shè)計過程中盡早消除錯誤可以節(jié)省下游的許多工程設(shè)計時間，尤其是設(shè)計過程從微架構(gòu)抽象級別開始時更是如此。

360 DV-Inspect 提供一系列自動化檢查，這些檢查利用形式化引擎的強大能力對設(shè)計代碼進行深入的靜態(tài)分析，而無需手動編寫斷言。這種設(shè)計檢查技術(shù)基于代碼結(jié)構(gòu)分析運行場景，以尋找潛在的錯誤，因而遠遠超越了傳統(tǒng)的代碼檢查工具。安全檢查（例如越界訪問數(shù)組或狀態(tài)機死鎖）、激活檢查以及結(jié)構(gòu)分析（包括經(jīng)典的仿真和綜合操作失配問題），全都具備。

圖 3. SystemC/C++ 代碼中的死鎖檢查

此外，DV-Inspect 提供了一些特別適用于 SystemC 代碼的檢查。例如，檢查哪些寄存器已被顯式初始化很重要。SystemC 變量在仿真中會自動初始化，但 HLS 工具會忽略這些初始化。這會導(dǎo)致難以調(diào)試的仿真綜合失配問題。DV-Inspect 還檢查尚未被初始化的寄存器及未定義的操作或多個驅(qū)動器能否在設(shè)計中傳播 X（未知）值。SystemC 仿真中不存在未知值的概念，因此需要進行形式化分析以發(fā)現(xiàn)傳播問題。 SystemC 還缺乏非阻塞賦值，因此導(dǎo)致了順序仿真語義與硬件中的并行操作之間出現(xiàn)競爭條件和失配的情況。

DV-Inspect 可以找出許多仿真或 HLS 都不會進行檢查的問題，包括特定數(shù)據(jù)類型問題（例如定點運算） 導(dǎo)致的意外行為，以及與并發(fā)相關(guān)的問題（例如競爭條件評估）。DV-Inspect 提供有價值的綜合前簽核，以節(jié)省整體開發(fā)時間和資源。

圖 4. 針對 SystemC/C++ 代碼的廣泛檢查

基于順序斷言的SystemC/C++ 驗證

360 DV-Verify 為 SystemC 和其他 SystemC/C++ 設(shè)計提供基于斷言的完整驗證解決方案。該工具接受大多數(shù) SystemC 函數(shù)，允許針對一系列代碼抽象測試斷言，從事務(wù)級模型 (TLM) 到詳細 RTL，一直到網(wǎng)表，從幾乎無時序到周期精準的完整表示。

簡單的 ANSI C 斷言和全時、并發(fā) SystemVerilog 斷言 (SVA)，均可配合 SystemC/C++ 設(shè)計使用。這種斷言描述的靈活性允許復(fù)用其他設(shè)計的現(xiàn)有斷言，或?qū)⑵溆米髂０?，以減少與新格式相關(guān)的學(xué)習(xí)開銷。它還支持一致的綜合前和綜合后流程，相同的斷言（如果編寫時考慮到流程）可以在 SystemC/C++ 業(yè)界標準模型及其 RTL 綜合后的衍生模型上復(fù)用。此外，針對 RTL 環(huán)境創(chuàng)建的驗證知識產(chǎn)權(quán) (VIP) 斷言集，例如總線協(xié)議驗證器，可以在 SystemC/C++ 代碼上復(fù)用。

這一獨特的能力支持順序斷言，后者可用于描述規(guī)范元素、預(yù)期的設(shè)計特征和要針對抽象代碼進行測試的故障條件。這樣，工程師便可在 SystemC/C++ 級別處理其業(yè)界標準設(shè)計，確保設(shè)計在綜合之前符合規(guī)范。它在可針對不同微架構(gòu)選項實施規(guī)范的級別上實現(xiàn)了全面的形式化解決方案。最后，它消除了使用綜合后的 RTL 代碼調(diào)試 SystemC/C++ 設(shè)計的間接性。

形式化技術(shù)已成為硬件設(shè)計功能驗證的關(guān)鍵組成部分。為了提高抽象級別并利用高層次綜合，許多設(shè)計人員已轉(zhuǎn)向 SystemC/C++。這種方法加快了硬件設(shè)計過程，但為了相應(yīng)地減少驗證時間，必須把重點放在 SystemC/C++ 源代碼上，而不是 HLS 后的 RTL 設(shè)計上。適用于 SystemC/C++ 的 360 DV 解決方案滿足這一需求，為高級設(shè)計提供自動化設(shè)計檢查和基于斷言的全面驗證。HLS 用戶可以充分利用先進的形式化驗證方法，西門子 EDA 解決方案使這一切成為可能。