RISC-V 設(shè)計(jì)中，架構(gòu)一致性驗(yàn)證與實(shí)現(xiàn)驗(yàn)證缺一不可但二者存在本質(zhì)區(qū)別，而具備架構(gòu)一致性驗(yàn)證經(jīng)驗(yàn)的工程師寥寥無(wú)幾。RISC-V 雖賦予設(shè)計(jì)高度靈活性，卻也埋下了生態(tài)系統(tǒng)碎片化的隱患。從數(shù)學(xué)角度而言，對(duì)所有指令組合進(jìn)行窮盡測(cè)試根本無(wú)法實(shí)現(xiàn)，因此工程師們正逐步擺脫單純的 “暴力測(cè)試” 模式。驗(yàn)證工作涉及多個(gè)專業(yè)領(lǐng)域，每個(gè)領(lǐng)域都至關(guān)重要且復(fù)雜度與日俱增。RISC-V 更是新增了架構(gòu)一致性這一驗(yàn)證維度 —— 直到近期，該領(lǐng)域也僅由少數(shù)企業(yè)閉門(mén)研究。

企業(yè)采用 RISC-V 的核心訴求之一，是提升芯片的性能或優(yōu)化功耗特性。但目前尚未形成統(tǒng)一標(biāo)準(zhǔn)的是，如何有效量化這些收益？如何在兼顧特定應(yīng)用場(chǎng)景目標(biāo)的前提下，對(duì)架構(gòu)特性進(jìn)行取舍，同時(shí)不損害軟件的可移植性？

RISC-V 國(guó)際基金會(huì)（RVI）正評(píng)估自身的參與邊界：在定義 RISC-V 內(nèi)核的標(biāo)準(zhǔn)上，基金會(huì)是否對(duì)社區(qū)負(fù)有責(zé)任？又該如何判定一款設(shè)計(jì)實(shí)現(xiàn)是否符合相關(guān)規(guī)范？即便不開(kāi)展全流程的驗(yàn)證工作，這一問(wèn)題也難以解答。

行業(yè)內(nèi)的諸多困惑，部分源于功能驗(yàn)證領(lǐng)域從未對(duì)“驗(yàn)證完整性” 給出明確定義。若將驗(yàn)證完整性理解為所有可能性的交叉組合，很快便會(huì)陷入無(wú)法解決的困境。盡管如此，行業(yè)仍能持續(xù)推出可用的產(chǎn)品，這正是得益于工程師們的專業(yè)判斷 —— 他們能確定驗(yàn)證的核心重點(diǎn)，并設(shè)計(jì)出高投入產(chǎn)出比的驗(yàn)證流程。

架構(gòu)一致性驗(yàn)證是多數(shù)工程師已生疏的技能，而整個(gè)行業(yè)必須加速補(bǔ)位。西門(mén)子 EDA 解決方案管理總監(jiān)弗拉迪斯拉夫?帕爾菲表示：“架構(gòu)一致性驗(yàn)證與實(shí)現(xiàn)驗(yàn)證的區(qū)別是根本性的，而人們常將二者混為一談，這讓驗(yàn)證工程師們倍感困擾。架構(gòu)一致性驗(yàn)證要回答的是：你所設(shè)計(jì)的產(chǎn)品是否真的是一款 RISC-V 內(nèi)核？需要驗(yàn)證其是否按規(guī)范執(zhí)行指令、正確處理異常、精準(zhǔn)實(shí)現(xiàn)內(nèi)存模型等，本質(zhì)是驗(yàn)證設(shè)計(jì)是否嚴(yán)格遵循官方規(guī)范實(shí)現(xiàn)了 RISC-V 的標(biāo)準(zhǔn)特性。而實(shí)現(xiàn)驗(yàn)證則聚焦于確保特定設(shè)計(jì)在實(shí)際場(chǎng)景中可正常工作，現(xiàn)實(shí)中，設(shè)計(jì)往往會(huì)以各種意想不到的方式出現(xiàn)故障。這一環(huán)節(jié)需要關(guān)注所有微架構(gòu)細(xì)節(jié)，比如流水線實(shí)現(xiàn)、緩存一致性、分支預(yù)測(cè)，以及那些往往在研發(fā)截止日期、工程師熬夜攻堅(jiān)時(shí)才會(huì)暴露的特殊邊緣場(chǎng)景?！?/p>

盡管這兩項(xiàng)工作看似相似，但其實(shí)現(xiàn)方法截然不同，在部分企業(yè)中，定義和執(zhí)行這兩項(xiàng)工作的責(zé)任甚至分屬不同團(tuán)隊(duì)或機(jī)構(gòu)。布雷克驗(yàn)證系統(tǒng)公司首席執(zhí)行官戴夫?克爾夫指出：“二者雖有共通之處，但細(xì)微的差異決定了驗(yàn)證方法也必須做出相應(yīng)調(diào)整。如今，RISC-V 內(nèi)核廠商正面臨與 ARM、英特爾等企業(yè)相同的問(wèn)題，為解決這些問(wèn)題，他們也在投入巨資研發(fā)新的驗(yàn)證流程?！?/p>

RISC-V 國(guó)際基金會(huì)已著手推進(jìn)相關(guān)工作。布雷克驗(yàn)證系統(tǒng)創(chuàng)始人兼首席技術(shù)官阿德南?哈米德稱：“基金會(huì)正開(kāi)展認(rèn)證相關(guān)工作。認(rèn)證被視為架構(gòu)驗(yàn)證的一小部分，但隨著 RISC-V 擴(kuò)展指令集的不斷增加，這一工作的難度和規(guī)模也在持續(xù)擴(kuò)大。其覆蓋范圍極廣且并非固定不變，新的特性還在不斷被加入。整個(gè)行業(yè)正攜手打造一套覆蓋率可追溯的流程，核心是梳理官方規(guī)范中的規(guī)范性規(guī)則 —— 即逐節(jié)分析規(guī)范，標(biāo)記出需要驗(yàn)證的條款，這是第一步。隨后提取這些條款并進(jìn)行分類，明確需要覆蓋的設(shè)計(jì)自由度，這是流程的組織環(huán)節(jié)。接下來(lái)還需設(shè)計(jì)測(cè)試流程并確定落地方式，而整個(gè)過(guò)程都需要實(shí)現(xiàn)從規(guī)范性規(guī)則到原始規(guī)范的全程可追溯?！?/p>

軟件兼容性

RISC-V 及其他任何處理器的成功，都與其周邊的生態(tài)系統(tǒng)緊密相關(guān)。阿爾泰瑞斯產(chǎn)品管理與營(yíng)銷總監(jiān)阿什利?史蒂文斯表示：“當(dāng)前 RISC-V 的標(biāo)準(zhǔn)化工作高度聚焦架構(gòu)一致性，確保設(shè)計(jì)中所有軟件可見(jiàn)的特性，都符合指令集架構(gòu)（ISA）和平臺(tái)規(guī)范的定義。架構(gòu)一致性測(cè)試套件會(huì)對(duì)指令、控制狀態(tài)寄存器（CSRs）、特權(quán)模式、中斷行為、內(nèi)存模型，以及其他軟件可見(jiàn)的組件進(jìn)行驗(yàn)證 —— 若中斷控制器、IOMMU（輸入輸出內(nèi)存管理單元）屬于軟件交互范疇，也會(huì)納入驗(yàn)證范圍。在社區(qū)、企業(yè)和標(biāo)準(zhǔn)組織的共同貢獻(xiàn)下，這些測(cè)試套件正不斷完善，為功能完整性驗(yàn)證提供了堅(jiān)實(shí)的基礎(chǔ)。而功能完整性的驗(yàn)證，主要通過(guò)指令集架構(gòu)級(jí)的覆蓋率指標(biāo)，或與黃金參考模型的差分測(cè)試來(lái)實(shí)現(xiàn)?！?/p>

并非所有企業(yè)都關(guān)注軟件兼容性。新思科技戰(zhàn)略項(xiàng)目與系統(tǒng)解決方案執(zhí)行董事弗蘭克?希爾梅斯特稱：“大型廠商或許無(wú)需過(guò)度擔(dān)憂標(biāo)準(zhǔn)的開(kāi)放性和互操作性，因?yàn)樗麄儞碛型暾纳鷳B(tài)體系。這類廠商的 RISC-V 設(shè)計(jì)僅服務(wù)于自身需求，無(wú)需證明其內(nèi)核在架構(gòu)層面能正確解析指令集架構(gòu)和相關(guān)配置文件，也無(wú)需保證軟件能跨不同內(nèi)核在這些配置文件上運(yùn)行。這與為追求開(kāi)放性而進(jìn)行的設(shè)計(jì)截然不同。RISC-V 國(guó)際基金會(huì)則希望打造類似其他領(lǐng)域的一致性檢測(cè)機(jī)制，而這一機(jī)制的核心目的，就是實(shí)現(xiàn)軟件的互操作性：只要通過(guò)某一配置文件的一致性檢測(cè)，軟件就能在所有支持該配置文件的 RISC-V 內(nèi)核上運(yùn)行?！?/p>

但 RISC-V 的特性讓這一目標(biāo)的實(shí)現(xiàn)充滿挑戰(zhàn)。布雷克驗(yàn)證系統(tǒng)的克爾夫表示：“RISC-V 的阿喀琉斯之踵，恰恰是其最大的優(yōu)勢(shì) —— 開(kāi)放指令集架構(gòu)帶來(lái)的靈活性。工程師們?cè)诶斫獠粩嘌葸M(jìn)的指令集架構(gòu)規(guī)范過(guò)程中，這種寶貴的靈活性可能會(huì)導(dǎo)致不同廠商的器件出現(xiàn)兼容性問(wèn)題。而兼容性缺失會(huì)降低軟件棧在不同器件間的可移植性，進(jìn)而產(chǎn)生巨大的工程開(kāi)發(fā)成本。”

這也是為何需要對(duì) RISC-V 的設(shè)計(jì)邊界進(jìn)行約束。新思科技設(shè)計(jì)驗(yàn)證解決方案產(chǎn)品經(jīng)理艾米?薩頓稱：“開(kāi)放性和可擴(kuò)展性是 RISC-V 的設(shè)計(jì)初衷和核心理念，因此并不存在統(tǒng)一的 RISC-V 定義。配置文件的推出，本是為了提升軟件可移植性，但絕不會(huì)出現(xiàn)因設(shè)計(jì)偏離指令集架構(gòu)，就被判定為非 RISC-V 內(nèi)核的情況。我們的 RISC-V 驗(yàn)證解決方案已定義了指令集架構(gòu)覆蓋率，且支持配置和擴(kuò)展，客戶可直接復(fù)用相關(guān)代碼 —— 這套方案包含逾 10 萬(wàn)行 SystemVerilog 代碼?？蛻艋诖?，可將精力集中在編寫(xiě)與自身設(shè)計(jì)相關(guān)的、更具針對(duì)性的覆蓋率驗(yàn)證代碼?！?/p>

標(biāo)準(zhǔn)仍是兼容性的核心支撐。微芯科技 FPGA 事業(yè)部技術(shù)院士皮埃爾?塞爾萬(wàn)表示：“架構(gòu)一致性驗(yàn)證與實(shí)現(xiàn)驗(yàn)證雖獨(dú)立開(kāi)展，但都是保障 IP 驗(yàn)證完整性的核心環(huán)節(jié)。架構(gòu)一致性驗(yàn)證通常通過(guò)遵循所有相關(guān)標(biāo)準(zhǔn)和規(guī)范實(shí)現(xiàn)，黃金參考模型則被用于確保所有相關(guān)擴(kuò)展指令集的指令集架構(gòu)一致性。同時(shí)，所有標(biāo)準(zhǔn)總線、對(duì)應(yīng)的接口，以及其他標(biāo)準(zhǔn)化模塊，都會(huì)納入驗(yàn)證范圍。”

歸根結(jié)底，一致性的判定標(biāo)準(zhǔn)，是某一測(cè)試集的結(jié)果與黃金參考模型的比對(duì)結(jié)果?？藸柗蜓a(bǔ)充道：“RISC-V 國(guó)際基金會(huì)正與哈維穆德學(xué)院合作，開(kāi)發(fā)一系列相對(duì)基礎(chǔ)的測(cè)試用例。這些用例可完成大部分非特權(quán)模式測(cè)試，但在特權(quán)模式測(cè)試中，自動(dòng)化實(shí)現(xiàn)的難度會(huì)大幅提升，只能手動(dòng)編寫(xiě)用例。對(duì)于基金會(huì)無(wú)力開(kāi)發(fā)、且無(wú)法從其他開(kāi)源方案中獲取的測(cè)試用例，我們正接手開(kāi)發(fā)。這類測(cè)試用例針對(duì)的是更復(fù)雜的特性，手動(dòng)編寫(xiě)難度極高，而我們可通過(guò)測(cè)試綜合工具自動(dòng)生成?！?/p>

從架構(gòu)一致性驗(yàn)證到實(shí)現(xiàn)驗(yàn)證

阿克西姆賽斯公司首席執(zhí)行官阿希什?達(dá)爾巴里表示：“實(shí)現(xiàn)一致性驗(yàn)證面臨兩大核心挑戰(zhàn)：一是確保內(nèi)核能正常工作，二是確保內(nèi)核在所有場(chǎng)景下都能正確工作。基于仿真的單元測(cè)試和一致性測(cè)試套件，只能驗(yàn)證內(nèi)核‘能否正常工作’這一基礎(chǔ)問(wèn)題 —— 即測(cè)試用例通過(guò)即可，但并不適用于驗(yàn)證‘全場(chǎng)景正確工作’的完整一致性，比如無(wú)法驗(yàn)證所有指令的任意組合，在任意執(zhí)行時(shí)機(jī)下，針對(duì)所有操作數(shù)都能正確運(yùn)行。形式化驗(yàn)證技術(shù)是這類窮盡分析的理想選擇，借助形式化模型檢測(cè)工具驗(yàn)證關(guān)鍵不變量，該技術(shù)已在這類場(chǎng)景中取得了成功應(yīng)用。這一方法的優(yōu)勢(shì)在于，除了能發(fā)現(xiàn)功能缺陷，還能檢測(cè)出死鎖、活鎖問(wèn)題，以及各類安全、可靠性隱患。缺陷修復(fù)后，可重新運(yùn)行不變量驗(yàn)證，通過(guò)窮盡性證明確認(rèn)缺陷已被徹底解決。作為六維覆蓋率的重要組成部分，場(chǎng)景覆蓋率能為架構(gòu)師和驗(yàn)證工程師提供基于證明的場(chǎng)景分析視角，帶來(lái)更深入的設(shè)計(jì)洞察?！?/p>

即便如此，要對(duì)設(shè)計(jì)的可用性形成完全的信心，仍存在諸多挑戰(zhàn)。西門(mén)子 EDA 的帕爾菲稱：“覆蓋率指標(biāo)就像驗(yàn)證儀表盤(pán)上的各類儀表，每一項(xiàng)都能反映關(guān)鍵信息，但單獨(dú)一項(xiàng)都無(wú)法呈現(xiàn)完整的驗(yàn)證狀態(tài)。代碼覆蓋率反映哪些邏輯被執(zhí)行過(guò)，功能覆蓋率反映哪些場(chǎng)景被測(cè)試過(guò)，斷言覆蓋率則確認(rèn)執(zhí)行過(guò)程中特定屬性是否始終成立。每一項(xiàng)指標(biāo)都能揭示部分真相，但問(wèn)題在于，這些指標(biāo)往往相互獨(dú)立，無(wú)法形成聯(lián)動(dòng)。比如，代碼覆蓋率表現(xiàn)優(yōu)異，卻可能完全遺漏 RISC-V 指令流水線中的關(guān)鍵邊緣場(chǎng)景；功能場(chǎng)景的驗(yàn)證全部完成，卻可能從未對(duì)認(rèn)證所需的核心架構(gòu)一致性要點(diǎn)進(jìn)行壓力測(cè)試?！?/p>

通過(guò)運(yùn)行設(shè)計(jì)獲取覆蓋率信息的流程，數(shù)十年來(lái)基本沒(méi)有變化。微芯科技的塞爾萬(wàn)表示：“行業(yè)普遍采用大規(guī)模的壓力測(cè)試，針對(duì)指定的擴(kuò)展指令集持續(xù)輸入數(shù)千條隨機(jī)指令。同時(shí)，會(huì)搭建多個(gè)測(cè)試平臺(tái)，驗(yàn)證設(shè)計(jì)實(shí)現(xiàn)的功能完整性?！?/p>

測(cè)試的執(zhí)行速度越快，驗(yàn)證效率越高。新思科技的薩頓稱：“我們緩解驗(yàn)證周期壓力的方法之一，是采用硬件輔助驗(yàn)證技術(shù)提升測(cè)試執(zhí)行速度，而覆蓋率分析是其中的關(guān)鍵環(huán)節(jié) —— 它能讓工程師明確驗(yàn)證的重點(diǎn)。驗(yàn)證并非單純的暴力測(cè)試、運(yùn)行海量周期即可，盡管這確實(shí)是應(yīng)對(duì) 10^18 量級(jí)驗(yàn)證周期挑戰(zhàn)的方法之一?！?/p>

如今，越來(lái)越多的驗(yàn)證引擎被用于提升測(cè)試速度。新思科技的希爾梅斯特表示：“行業(yè)的目標(biāo)是實(shí)現(xiàn)全驗(yàn)證流程的協(xié)同部署，即整合各類驗(yàn)證引擎的能力。這一流程從虛擬平臺(tái)架構(gòu)設(shè)計(jì)開(kāi)始，延伸至硬件輔助驗(yàn)證和驗(yàn)證 IP—— 驗(yàn)證 IP 對(duì)接口驗(yàn)證尤為重要，測(cè)試生成工具也正融入這一體系。首先是架構(gòu)覆蓋率驗(yàn)證，比如指令、特權(quán)模式、通斷、異常等場(chǎng)景，需通過(guò)覆蓋組實(shí)現(xiàn)，通常在仿真環(huán)境中運(yùn)行；隨后是場(chǎng)景級(jí)驗(yàn)證，復(fù)雜度會(huì)進(jìn)一步提升，而形式化驗(yàn)證技術(shù)能在這類問(wèn)題的部分場(chǎng)景中發(fā)揮優(yōu)勢(shì)?！?/p>

測(cè)試綜合技術(shù)的核心能力之一，是支持為各類執(zhí)行引擎生成測(cè)試用例。布雷克驗(yàn)證系統(tǒng)的哈米德稱：“測(cè)試用例需要能適配仿真、硬件仿真、FPGA 驗(yàn)證和硅后驗(yàn)證等多種場(chǎng)景，既包括事務(wù)級(jí)測(cè)試用例，也包括可在內(nèi)核上運(yùn)行的軟件測(cè)試用例。在不同的驗(yàn)證層級(jí)，能實(shí)現(xiàn)的覆蓋率會(huì)呈數(shù)量級(jí)提升：仿真環(huán)境中可完成 10^4 量級(jí)的用例測(cè)試，硬件仿真中可達(dá) 10^6 量級(jí)，硅后驗(yàn)證中則能實(shí)現(xiàn) 10^8 量級(jí)，甚至 10^9 量級(jí)的硅后驗(yàn)證用例測(cè)試也具備可行性。”

企業(yè)無(wú)法承擔(dān)重復(fù)驗(yàn)證的成本。阿爾泰瑞斯的史蒂文斯表示：“實(shí)現(xiàn)驗(yàn)證是工程師投入精力最多的環(huán)節(jié)，涵蓋微架構(gòu)邊緣場(chǎng)景、時(shí)序交互、緩存一致性、執(zhí)行順序、安全特性，以及軟件不可見(jiàn)的硬件間協(xié)議接口等內(nèi)容。要實(shí)現(xiàn)實(shí)現(xiàn)驗(yàn)證的完整性，需要結(jié)合仿真、硬件仿真、UVM 驗(yàn)證環(huán)境、覆蓋率驅(qū)動(dòng)的測(cè)試，同時(shí)越來(lái)越多地采用形式化驗(yàn)證技術(shù)。與能直接映射為指令級(jí)覆蓋率的架構(gòu)驗(yàn)證不同，實(shí)現(xiàn)驗(yàn)證的完整性更難量化，其驗(yàn)證重點(diǎn)高度依賴于各設(shè)計(jì)的具體結(jié)構(gòu)和接口?！?/p>

覆蓋率指標(biāo)是驗(yàn)證工作推進(jìn)的重要依據(jù)。微芯科技的塞爾萬(wàn)稱：“覆蓋率指標(biāo)是評(píng)估設(shè)計(jì)驗(yàn)證質(zhì)量的核心，功能覆蓋率需與結(jié)構(gòu)性覆蓋率指標(biāo)相互補(bǔ)充，后者包括語(yǔ)句覆蓋率、分支覆蓋率、條件覆蓋率、翻轉(zhuǎn)覆蓋率和有限狀態(tài)機(jī)覆蓋率等。對(duì)于 MIV_RV32 這類高度可配置的嵌入式 IP 核，提取覆蓋率指標(biāo)的難度更高，通常需要通過(guò)大量的測(cè)試運(yùn)行才能滿足覆蓋率要求。目前，工具廠商正持續(xù)升級(jí)產(chǎn)品，以實(shí)現(xiàn)從高度可配置的設(shè)計(jì)中提取覆蓋率指標(biāo)?！?/p>

定義覆蓋率指標(biāo)，需要資深工程師的專業(yè)判斷。哈米德表示：“微架構(gòu)中哪些部分值得做覆蓋率驗(yàn)證？哪些隊(duì)列存在溢出風(fēng)險(xiǎn)？這類工作的實(shí)現(xiàn)成本不菲，且目前尚無(wú)自動(dòng)化工具能完成?？蛻粜枰鹨皇崂聿?biāo)記需要覆蓋的點(diǎn)，這一問(wèn)題的解決成本很高，但至少我們能明確問(wèn)題所在，只要投入足夠的時(shí)間和資金，就能推進(jìn)解決。比如我們會(huì)發(fā)現(xiàn)，某一系統(tǒng)中的 Q5 隊(duì)列從未出現(xiàn)過(guò)溢出 —— 這種情況是否可能發(fā)生？是否存在觸發(fā)路徑？若存在，需要哪些場(chǎng)景？從全局來(lái)看，這類信息往往是未知的，即便是架構(gòu)師也無(wú)法給出答案。我們?nèi)狈ψ銐虻脑O(shè)計(jì)細(xì)節(jié)來(lái)判斷這類場(chǎng)景是否存在，因此只能通過(guò)工程判斷，確定需要確定性驗(yàn)證的場(chǎng)景，其余則采用隨機(jī)驗(yàn)證。但這一方法僅針對(duì)單一場(chǎng)景，而場(chǎng)景的執(zhí)行順序不同，也可能導(dǎo)致硬件出現(xiàn)不同的問(wèn)題?！?/p>

實(shí)現(xiàn)驗(yàn)證完整性，需要理解不同類型覆蓋率之間的關(guān)聯(lián)。帕爾菲表示：“僅知道 RTL 代碼中第 247 行被執(zhí)行過(guò)，遠(yuǎn)遠(yuǎn)不夠。我們需要知道這一行代碼是否在所有關(guān)鍵條件下都被執(zhí)行過(guò)、其相關(guān)斷言是否觸發(fā)正常、測(cè)試計(jì)劃是否原本就計(jì)劃驗(yàn)證該場(chǎng)景、以及該場(chǎng)景是否對(duì)應(yīng)特定的架構(gòu)要求。所有覆蓋率數(shù)據(jù)需要實(shí)現(xiàn)統(tǒng)一整合，同時(shí)保留相互間的關(guān)聯(lián)、維持設(shè)計(jì)的層級(jí)結(jié)構(gòu)、保證全程可追溯。試想一下，若能將仿真、硬件仿真、形式化驗(yàn)證等所有驗(yàn)證引擎的覆蓋率數(shù)據(jù)進(jìn)行智能融合，同時(shí)保留設(shè)計(jì)結(jié)構(gòu)、追蹤各測(cè)試用例對(duì)覆蓋率的貢獻(xiàn)，最重要的是能清晰呈現(xiàn)驗(yàn)證缺口 —— 這將大幅提升驗(yàn)證效率?！?/p>

驗(yàn)證缺口

除了設(shè)計(jì)實(shí)現(xiàn)中的覆蓋率漏洞，當(dāng)前整個(gè)驗(yàn)證理念也存在諸多覆蓋缺口，行業(yè)正逐步推進(jìn)這些缺口的填補(bǔ)工作。

史蒂文斯表示：“RISC-V 生態(tài)的一大核心缺口，是除核心指令集架構(gòu)外，缺乏標(biāo)準(zhǔn)化的硬件接口?？蓴U(kuò)展的片上系統(tǒng)集成，依賴于處理器與系統(tǒng)其他組件（包括互連架構(gòu)）之間可預(yù)測(cè)、可互操作、可驗(yàn)證的接口連接，而這正是實(shí)現(xiàn)驗(yàn)證的核心價(jià)值所在。盡管許多 RISC-V 開(kāi)發(fā)者會(huì)采用 AMBA CHI 等現(xiàn)有接口，但這類規(guī)范的篇幅已超千頁(yè)，其中大部分內(nèi)容對(duì)典型的 RISC-V 系統(tǒng)而言并無(wú)必要。真正能為社區(qū)帶來(lái)價(jià)值的，是一套面向 RISC-V 的精簡(jiǎn)接口子集，或一套貼合實(shí)際應(yīng)用場(chǎng)景的輕量化接口標(biāo)準(zhǔn)。這類標(biāo)準(zhǔn)化工作，將大幅減少重復(fù)的驗(yàn)證工作、提升覆蓋率的一致性，并加速多廠商產(chǎn)品間的互操作性。”

部分驗(yàn)證缺口還超出了功能驗(yàn)證的范疇。帕爾菲分享道：“我近期與一位工程師交流，他剛完成一款車(chē)用 RISC-V 內(nèi)核的流片。該內(nèi)核通過(guò)了所有架構(gòu)驗(yàn)證測(cè)試，但在軟件調(diào)試開(kāi)展三個(gè)月后，工程師發(fā)現(xiàn)其分支預(yù)測(cè)的準(zhǔn)確率如同拋硬幣一般低。從技術(shù)角度看，該內(nèi)核的設(shè)計(jì)是合規(guī)的，但從功能角度看，毫無(wú)實(shí)用價(jià)值，廠商承諾的性能指標(biāo)完全無(wú)法實(shí)現(xiàn)。而目前全球范圍內(nèi)，沒(méi)有任何一套測(cè)試套件能檢測(cè)出這類問(wèn)題 —— 因?yàn)樾阅茯?yàn)證尚未成為 RISC-V 生態(tài)的標(biāo)準(zhǔn)化內(nèi)容，每家企業(yè)都在搭建自己的定制化基礎(chǔ)設(shè)施，來(lái)回答‘這款產(chǎn)品的實(shí)際運(yùn)行速度是否達(dá)標(biāo)’這一問(wèn)題?！?/p>

但追求高性能，又會(huì)引發(fā)新的問(wèn)題?？藸柗虮硎荆骸皩?duì)于部分設(shè)計(jì)，提升時(shí)鐘頻率以優(yōu)化性能時(shí)，設(shè)計(jì)中的部分區(qū)域會(huì)成為熱功耗熱點(diǎn)，這一問(wèn)題需要重點(diǎn)關(guān)注。我們可通過(guò)運(yùn)行實(shí)際工作負(fù)載和合成工作負(fù)載，檢測(cè)熱功耗熱點(diǎn)的觸發(fā)情況，這一測(cè)試也會(huì)為功耗分析提供依據(jù)。汽車(chē)、數(shù)據(jù)中心等領(lǐng)域的企業(yè)對(duì)這一問(wèn)題高度關(guān)注，他們需要通過(guò)調(diào)節(jié)時(shí)鐘頻率，模擬并驗(yàn)證熱功耗熱點(diǎn)的觸發(fā)場(chǎng)景，同時(shí)認(rèn)證產(chǎn)品能否承受相應(yīng)的熱阻和功耗壓力?！?/p>

與其他部分應(yīng)用領(lǐng)域一樣，汽車(chē)領(lǐng)域?yàn)?RISC-V 驗(yàn)證增加了新的維度。帕爾菲稱：“若為汽車(chē)或工業(yè)應(yīng)用設(shè)計(jì) RISC-V，工程師將面臨功能安全和可靠性驗(yàn)證的全新挑戰(zhàn)。ISO 26262 汽車(chē)功能安全標(biāo)準(zhǔn)并不關(guān)心產(chǎn)品是否通過(guò)了指令集架構(gòu)測(cè)試，而是要求驗(yàn)證故障注入、錯(cuò)誤處理機(jī)制的有效性，以及功能安全機(jī)制的運(yùn)行表現(xiàn)?，F(xiàn)有測(cè)試套件的設(shè)計(jì)并未考慮這些要求，因此企業(yè)需要從零開(kāi)始搭建相關(guān)驗(yàn)證體系?！?/p>

其他驗(yàn)證技術(shù)的應(yīng)用價(jià)值

形式化驗(yàn)證技術(shù)提供了一套互補(bǔ)的能力，在 RISC-V 驗(yàn)證中占據(jù)重要地位。帕爾菲表示：“早期的 RISC-V 相關(guān)探討中，就已提及形式化驗(yàn)證方法，當(dāng)時(shí)業(yè)內(nèi)還抱有樂(lè)觀的設(shè)想：‘RISC-V 是開(kāi)放規(guī)范，我們可通過(guò)形式化驗(yàn)證，將整個(gè)內(nèi)核與指令集架構(gòu)進(jìn)行比對(duì)，從而證明設(shè)計(jì)的正確性?！@一設(shè)想在理論上十分完美，但在實(shí)際落地中難度極大?！?/p>

盡管如此，形式化驗(yàn)證仍能發(fā)揮重要作用。史蒂文斯表示：“形式化驗(yàn)證正成為解決方案中越來(lái)越重要的部分，在架構(gòu)一致性驗(yàn)證中表現(xiàn)尤為突出 —— 能確保指令集架構(gòu)的各項(xiàng)屬性在所有合法指令序列中都成立；同時(shí)，在實(shí)現(xiàn)驗(yàn)證中，該技術(shù)也能有效保障硬件協(xié)議的正確性。但形式化驗(yàn)證無(wú)法替代動(dòng)態(tài)驗(yàn)證和系統(tǒng)級(jí)驗(yàn)證，尤其是在涉及完整片上系統(tǒng)行為和實(shí)際工作負(fù)載的場(chǎng)景中。在實(shí)際應(yīng)用中，形式化驗(yàn)證主要發(fā)揮互補(bǔ)作用：通過(guò)窮盡驗(yàn)證解決深度邊緣場(chǎng)景的正確性問(wèn)題，而仿真和硬件仿真則負(fù)責(zé)實(shí)現(xiàn)端到端的完整性驗(yàn)證?！?/p>

目前，形式化驗(yàn)證技術(shù)已得到廣泛應(yīng)用。塞爾萬(wàn)表示：“形式化驗(yàn)證的落地，為在限定范圍內(nèi)對(duì)設(shè)計(jì)有效性進(jìn)行窮盡測(cè)試提供了方法，從源頭提升了代碼質(zhì)量。靜態(tài)形式化工具被廣泛用于早期的缺陷發(fā)現(xiàn)和修復(fù)，從而最大限度縮短后續(xù)的驗(yàn)證周期。形式化驗(yàn)證是我們研發(fā)流程的重要組成部分，通過(guò)持續(xù)的驗(yàn)證實(shí)踐，其在高可靠性嵌入式 IP 產(chǎn)品的研發(fā)中，將持續(xù)發(fā)揮重要價(jià)值?！?/p>

人工智能的新能力也可被充分利用。芯智體公司首席執(zhí)行官威廉?王表示：“RISC-V 是智能體式人工智能在驗(yàn)證領(lǐng)域的絕佳應(yīng)用場(chǎng)景。我們已成功將智能體式人工智能應(yīng)用于形式化驗(yàn)證，尤其是處理器設(shè)計(jì)以控制類信號(hào)為主，非常適合形式化推理和符號(hào)化探索 —— 這與 AI 加速器形成鮮明對(duì)比，AI 加速器的設(shè)計(jì)以數(shù)據(jù)中心式流程為主，難以單純通過(guò)形式化技術(shù)實(shí)現(xiàn)驗(yàn)證。隨著 RISC-V 的普及，人工智能驅(qū)動(dòng)的形式化驗(yàn)證方法，將大幅加速架構(gòu)一致性驗(yàn)證和實(shí)現(xiàn)驗(yàn)證的進(jìn)程，為日益復(fù)雜、高度可配置的設(shè)計(jì)，提供可擴(kuò)展的正確性和覆蓋率驗(yàn)證方案。

原文：

https://semiengineering.com/does-your-risc-v-core-meet-with-the-standard

EETOP創(chuàng)芯大講堂芯片課程推薦