SystemC/C++ 設計的驗證要求

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

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

圖 1. SystemC/C++ 高層次設計流程

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

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

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

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

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

適用于 SystemC/C++ 設計的360 DV 簡介

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

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

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

圖 2. SVA 配合 SystemC/C++ 設計使用

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

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

自動形式化 SystemC/C++ 設計評估

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

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

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

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

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

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

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

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

簡單的 ANSI C 斷言和全時、并發 SystemVerilog 斷言 (SVA)，均可配合 SystemC/C++ 設計使用。這種斷言描述的靈活性允許復用其他設計的現有斷言，或將其用作模板，以減少與新格式相關的學習開銷。它還支持一致的綜合前和綜合后流程，相同的斷言（如果編寫時考慮到流程）可以在 SystemC/C++ 業界標準模型及其 RTL 綜合后的衍生模型上復用。此外，針對 RTL 環境創建的驗證知識產權 (VIP) 斷言集，例如總線協議驗證器，可以在 SystemC/C++ 代碼上復用。

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

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