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

RISC-V 遠超常規(guī)的，獨特的驗證挑戰(zhàn)

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

對于 RISC-V 來說，驗證還有一些遠超常規(guī)的，獨特的驗證挑戰(zhàn)。

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

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

形式化驗證的優(yōu)點

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

形式化驗證擁有許多優(yōu)點：

在設計早期就能發(fā)現(xiàn)潛在的錯誤和漏洞，可以為設計團隊節(jié)省大量時間和精力。

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

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

發(fā)現(xiàn) property 反例的速度比動態(tài)驗證快得多。

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

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

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

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

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

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

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

結語

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