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

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

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

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

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

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

形式化驗(yàn)證的優(yōu)點(diǎn)

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

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

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

除了初始設(shè)置和 property 開發(fā)，驗(yàn)證過程大部分是全自動(dòng)的。

RTL 一旦就緒就可以開始驗(yàn)證，適合敏捷過程。

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

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

新思科技 VC Formal 解決方案在 RISC-V 驗(yàn)證中的應(yīng)用

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

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

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

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

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

結(jié)語

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