從擁抱趨勢、暢想未來，到解決問題、交付產品，RISC-V 芯片已被廣泛使用。據咨詢機構 Semico Research 測算，截止 2024 年底全球 RISC-V 核的累積使用量已達 500 億顆——地球上人均 6 顆。從“RISC-V 將無處不在”到“RISC-V，就現在”，RISC-V 已幾乎覆蓋所有應用。當前，RISC-V 已成功躋身世界主流處理器市場，不再局限于低功耗小設備，而是明確向智能汽車、工業、5G基站、端側AI 乃至數據中心等高價值領域縱深推進。

RISC-V 遠超常規的，獨特的驗證挑戰

在半導體和系統設計中，驗證的目標是證明我們計劃構建的產品能夠實現預期的各項功能，并且永遠不會出現任何異常行為。智能化的今天，電子設備的復雜性正在迅速增加，對于錯誤的容忍度卻在不斷降低，存在缺陷的產品輕則導致召回，嚴重的甚至可能導致致命事故。因此對于芯片而言，從設計到交付，驗證是過程中關鍵的一環，對于驗證的要求也越來越高。

對于 RISC-V 來說，驗證還有一些遠超常規的，獨特的驗證挑戰。

RISC-V 是指令集架構而不是芯片架構本身。RISC-V 指令集架構由一個精簡的基礎指令集和一系列可選的標準擴展組成，設計者可以像搭積木一樣選擇指令集。除此之外，設計者還可以添加專用指令完成自定義拓展，用來優化特定應用（如 AI 加速、加密、DSP 等）。當設計者使用 RISC-V ISA 進行架構設計時，首先就要進行 ISA（指令集架構）的合規性完備測試。

RISC-V 的開源、開放以及靈活性吸引了大量廠商和開源社區開發專屬的微架構內核或者 IP 模塊。這些微架構可以實現相同的基礎 ISA 和標準擴展，但在控制路徑和數據路徑中，有許多實現選擇。不同的選擇，在性能、功耗和復雜性方面也可能存在差異，這導致了復雜的微架構驗證需求，每一個不同的 RISC-V 微架構內核和 IP 都需要自己的微架構驗證來驗證處理器的內部實現細節。設計者的自定義拓展甚至可能顯著改變處理器的行為（比如改變了流水線中的內容、ALU 中的沖突、緩存系統問題或者加載存儲內容），每一項自定義拓展都會使驗證難度加倍，添加的所有內容必須完全重新驗證，不僅要保證功能正確，還要確保它們保持系統一致性。

形式化驗證的優點

形式化驗證的核心是通過數學證明，窮舉所有可能的設計行為。經過多年的發展，現在形式化驗證已經與仿真、硬件加速和硬件原型設計并駕齊驅，隨著設計復雜度提高和驗證難度提高，發展形式化驗證已經勢在必行。

形式化驗證擁有許多優點：

在設計早期就能發現潛在的錯誤和漏洞，可以為設計團隊節省大量時間和精力。

除了初始設置和 property 開發，驗證過程大部分是全自動的。

RTL 一旦就緒就可以開始驗證，適合敏捷過程。

發現 property 反例的速度比動態驗證快得多。

值得信賴，形式化驗證窮舉所有可能，擁有 100% 確定性。

新思科技 VC Formal 解決方案在 RISC-V 驗證中的應用

新思科技推出的新一代形式化驗證解決方案 VC Formal 是業內領先的形式化驗證工具，與 Synopsys VCS、Verdi、VC SpyGlass、VC Z01X 故障模擬及其他新思科技設計與驗證解決方案協同工作。VC Formal 擁有出色的容量、速度和靈活性，可驗證某些最艱巨的設計挑戰，比如關鍵模塊的 bug-free 驗證。VC formal 結合統一的 VCS 編譯和 Verdi 調試可幫助用戶減少遷移投入，快速調試遇到的問題，并通過支持 VCS UNR 解決方案實現更快的覆蓋收斂。

VC Formal 解決方案包括一整套 APP：屬性驗證 (FPV)、自動提取屬性 (AEP)、覆蓋分析器 (FCA)、連接性檢查 (CC)、時序等效性檢查 (SEQ)、寄存器驗證 (FRV)、測試平臺分析儀 (FTA)、形式導航器 (Navigator) 以及用于驗證標準總線協議的一組斷言 IP (AIP）等。

VC Formal 解決方案可完美應用于 RICS-V 內核與 IP 模塊的驗證。在 RISC-V 內核與模塊的驗證中，所有能夠通過 SVA 的方式描述出來的控制邏輯，都可以通過 FPV（屬性斷言驗證）來做檢查。針對運算邏輯，DPV（數據通路驗證）主要提供 C model 和 RTL 的等價性檢查。SEQ（等價性檢查）可以保證 RTL 階段引入門控時鐘前后，兩份 RTL 的功能一致性。寄存器驗證（FRV）從形式上驗證 RISC-V CSR 的行為，如 “只讀”“讀/寫”“復位值” 等屬性，無需再通過定向測試驗證。FSV（安全檢查）可以保證安全數據不會發生傳播泄漏或者被篡改，保障數據完整性。

新思科技提供完整的、高性能、優化后的斷言 IP 庫，可用于驗證標準總線協議如 AMBA 協議，兼容 VC Formal 形式化驗證以及 VCS 仿真。用戶可直接調用該 IP 庫，無需從零構建斷言 IP，大幅縮短驗證啟動時間。

其中，RISC-V ISA 斷言 IP 可以用在 ISA（指令集架構）的合規性完備測試中。它可以形式化測試所有可能的 RISC-V 指令場景，驗證指令執行控制路徑和基本 ISA 數據路徑，并可用于多種配置和內核。

結語

開放的 RISC-V 正在為計算產業帶來創新活力，從設計到交付，完善的驗證至關重要。新思科技在 RISC-V 驗證領域處于領先地位，持續推動 RISC-V 技術標準化與工具鏈整合，為 RISC-V 產業落地提供了堅實支撐，攜手全球開發者加速 RISC-V 的創新發展與生態繁榮。