來(lái)源：編譯自semiengineering

本文轉(zhuǎn)自：半導(dǎo)體行業(yè)觀察

驗(yàn)證涉及多個(gè)學(xué)科，每個(gè)學(xué)科都至關(guān)重要，而且都變得日益復(fù)雜。RISC-V 又增加了一個(gè)學(xué)科——架構(gòu)一致性——直到最近，這方面的研究還只是少數(shù)幾家公司在私下進(jìn)行。

采用 RISC-V 的一個(gè)關(guān)鍵原因是希望提升性能或功耗特性。然而，如何有效地衡量這些優(yōu)勢(shì)尚不明確。如何在不影響軟件可移植性的前提下，權(quán)衡架構(gòu)特性與這些特定應(yīng)用目標(biāo)之間的關(guān)系？

RISC-V國(guó)際組織（RVI）正在評(píng)估自身需要參與的程度。在定義RISC-V內(nèi)核方面，RVI是否對(duì)社區(qū)負(fù)有責(zé)任？如何才能確定某個(gè)實(shí)現(xiàn)符合相關(guān)規(guī)范？除非開(kāi)展全面的驗(yàn)證工作，否則這并非易事。

至少部分困惑源于功能驗(yàn)證領(lǐng)域從未對(duì)驗(yàn)證完備性做出明確定義。如果將其視為所有可能性的乘積，很快就會(huì)導(dǎo)致一個(gè)棘手的問(wèn)題。盡管如此，業(yè)界仍然能夠發(fā)布有效的產(chǎn)品，這證明了那些能夠判斷哪些因素至關(guān)重要，以及如何實(shí)現(xiàn)驗(yàn)證流程的工程師的卓越能力，從而使投入的時(shí)間和金錢(qián)獲得良好的回報(bào)。

一致性驗(yàn)證是一項(xiàng)大多數(shù)工程師已經(jīng)遺忘的驗(yàn)證技能，但業(yè)界必須迅速迎頭趕上?！凹軜?gòu)一致性驗(yàn)證和實(shí)現(xiàn)驗(yàn)證之間的區(qū)別至關(guān)重要，盡管它們經(jīng)常被混為一談，這讓驗(yàn)證工程師們感到棘手，”西門(mén)子EDA解決方案管理總監(jiān)Vladislav Palfy說(shuō)道?！凹軜?gòu)一致性驗(yàn)證旨在確認(rèn)你設(shè)計(jì)的東西是否真的是一個(gè)RISC-V內(nèi)核。你需要驗(yàn)證它是否按定義執(zhí)行指令、正確處理異常、正確實(shí)現(xiàn)內(nèi)存模型等等。它驗(yàn)證的是你是否按照官方規(guī)范使用了正確的RISC-V語(yǔ)言。另一方面，實(shí)現(xiàn)驗(yàn)證則旨在確保你的特定設(shè)計(jì)在實(shí)際應(yīng)用中能夠正常工作，而實(shí)際應(yīng)用中往往會(huì)出現(xiàn)各種各樣的問(wèn)題。我們指的是所有微架構(gòu)細(xì)節(jié)，例如流水線(xiàn)實(shí)現(xiàn)、緩存一致性、分支預(yù)測(cè)，以及那些只有在最不方便的時(shí)候才會(huì)出現(xiàn)的特殊情況，通常是在咖啡因和截止日期臨近的情況下?！?/span>

雖然這兩項(xiàng)任務(wù)聽(tīng)起來(lái)相似，但它們需要不同的方法，而且在某些情況下，定義和執(zhí)行這些任務(wù)的責(zé)任可能由不同的團(tuán)隊(duì)或組織承擔(dān)?！氨M管這兩項(xiàng)活動(dòng)有共同之處，但它們之間存在細(xì)微差別，驗(yàn)證方法也截然不同，”Breker Verification Systems 的首席執(zhí)行官 Dave Kelf 表示?！癛ISC-V 內(nèi)核供應(yīng)商現(xiàn)在正面臨著與 Arm、Intel 和其他公司相同的問(wèn)題，他們正努力解決這些問(wèn)題，并在新的驗(yàn)證流程開(kāi)發(fā)方面投入巨資。”

RVI 一直在努力完成這項(xiàng)任務(wù)的一部分?！癛VI 一直在攻克認(rèn)證難題，”Breker 的創(chuàng)始人兼首席技術(shù)官 Adnan Hamid 表示?！罢J(rèn)證原本只是架構(gòu)驗(yàn)證的一小部分，但由于擴(kuò)展功能的不斷增加，它仍然是一個(gè)日益嚴(yán)峻的問(wèn)題。其范圍非常廣泛，而且并非一成不變。他們一直在添加新的內(nèi)容。整個(gè)行業(yè)不得不共同探索一種覆蓋率可追溯性流程，這相當(dāng)于要逐節(jié)審查規(guī)范，也就是用熒光筆標(biāo)記出需要驗(yàn)證的句子。這是第一步。然后，將這些句子提取出來(lái)，進(jìn)行分類(lèi)，并確定需要覆蓋的自由度。這是組織工作。接下來(lái)，制定測(cè)試流程，并決定如何實(shí)現(xiàn)該測(cè)試流程。你需要從這些規(guī)范規(guī)則開(kāi)始，一直追溯到原始規(guī)范，實(shí)現(xiàn)全程可追溯性?！?/span>

軟件兼容性

RISC-V 以及任何其他處理器的成功都與其周?chē)纳鷳B(tài)系統(tǒng)密切相關(guān)?！澳壳?，RISC-V 的標(biāo)準(zhǔn)化工作主要集中在架構(gòu)一致性上，確保實(shí)現(xiàn)中所有軟件可見(jiàn)的部分都按照指令集架構(gòu) (ISA) 和平臺(tái)規(guī)范進(jìn)行運(yùn)行，” Arteris產(chǎn)品管理和市場(chǎng)總監(jiān) Ashley Stevens 表示?！凹軜?gòu)一致性測(cè)試套件驗(yàn)證指令、CSR、特權(quán)模式、中斷行為、內(nèi)存模型以及其他 ISA 可見(jiàn)的組件——包括中斷控制器或 IOMMU（當(dāng)它們包含在軟件契約中時(shí)）。這些測(cè)試套件在社區(qū)、公司和標(biāo)準(zhǔn)組織的貢獻(xiàn)下不斷完善，為功能完整性提供了堅(jiān)實(shí)的基準(zhǔn)。這可以通過(guò) ISA 級(jí)別的覆蓋率指標(biāo)或與參考模型的差異測(cè)試來(lái)衡量?！?/span>

并非所有人都關(guān)心軟件兼容性?！叭绻闶且患掖笮凸?yīng)商，你可能不會(huì)太在意標(biāo)準(zhǔn)的開(kāi)放性和互操作性，因?yàn)橐磺卸加赡阏瓶兀?Synopsys戰(zhàn)略項(xiàng)目和系統(tǒng)解決方案執(zhí)行總監(jiān) Frank Schirrmeister 表示?！澳阒皇菫榱俗约憾?，無(wú)需證明核心架構(gòu)是否能夠正確解讀指令集架構(gòu) (ISA) 和相關(guān)規(guī)范，從而確保軟件能夠在不同核心的平臺(tái)上運(yùn)行。這與為了開(kāi)放性而設(shè)計(jì)軟件的情況截然不同。如果你看看 RVI 組織，他們希望進(jìn)行類(lèi)似其他領(lǐng)域的合規(guī)性檢查。而合規(guī)性檢查的真正目的就是為了實(shí)現(xiàn)軟件的互操作性。如果你的軟件通過(guò)了合規(guī)性檢查，那么它就應(yīng)該能夠在不同的平臺(tái)上運(yùn)行?！?/span>

RISC-V 架構(gòu)并非易于實(shí)現(xiàn)。“RISC-V 的致命弱點(diǎn)恰恰在于其最大的優(yōu)勢(shì)——開(kāi)放指令集架構(gòu)的靈活性，”Breker 公司的 Kelf 表示?！斑@種寶貴的靈活性也可能導(dǎo)致不同來(lái)源的設(shè)備之間出現(xiàn)不兼容的情況，因?yàn)楣こ處焸冃枰斫獠粩喟l(fā)展的 ISA 規(guī)范。這種不兼容性降低了軟件棧在不同設(shè)備間的可移植性，從而導(dǎo)致顯著的工程開(kāi)銷(xiāo)?！?/span>

這就是為什么需要對(duì)問(wèn)題進(jìn)行限定?！癛ISC-V 的起源和理念在于開(kāi)放性和可擴(kuò)展性，”Synopsys 設(shè)計(jì)驗(yàn)證解決方案產(chǎn)品經(jīng)理 Aimee Sutton 表示?！癛ISC-V 沒(méi)有統(tǒng)一的定義。創(chuàng)建配置文件是為了方便軟件移植，但沒(méi)有人會(huì)因?yàn)槠x了指令集架構(gòu) (ISA) 就斷言這不是 RISC-V 內(nèi)核。我們的 RISC-V 驗(yàn)證解決方案定義了 ISA 覆蓋范圍，并使其可配置和可擴(kuò)展，以便客戶(hù)能夠充分利用這些代碼。SystemVerilog 代碼超過(guò) 10 萬(wàn)行?？蛻?hù)可以利用這些代碼，然后專(zhuān)注于編寫(xiě)更符合自身設(shè)計(jì)需求的、更有價(jià)值的覆蓋范圍?！?/span>

標(biāo)準(zhǔn)仍然是兼容性的核心?！凹軜?gòu)一致性和實(shí)現(xiàn)驗(yàn)證是獨(dú)立進(jìn)行的，但對(duì)于確保整體 IP 驗(yàn)證的完整性至關(guān)重要，”Microchip Technology FPGA 業(yè)務(wù)部門(mén)的技術(shù)專(zhuān)家 Pierre Selwan 表示?！凹軜?gòu)一致性通常是通過(guò)遵守所有相關(guān)標(biāo)準(zhǔn)和規(guī)范來(lái)實(shí)現(xiàn)的。黃金參考模型用于確保相關(guān)擴(kuò)展的 ISA 合規(guī)性。所有標(biāo)準(zhǔn)總線(xiàn)及其相應(yīng)的接口以及任何其他標(biāo)準(zhǔn)化模塊都會(huì)進(jìn)行測(cè)試。”

歸根結(jié)底，一致性意味著一組特定的測(cè)試用例已經(jīng)與黃金模型進(jìn)行了比對(duì)?！癛VI 通過(guò)哈維穆德學(xué)院開(kāi)發(fā)了一套相對(duì)簡(jiǎn)單的測(cè)試用例，”Kelf 說(shuō)?！八麄兛梢酝瓿纱蟛糠址翘貦?quán)測(cè)試，但當(dāng)涉及到特權(quán)測(cè)試時(shí)，自動(dòng)化就變得困難得多。他們必須手動(dòng)編寫(xiě)這些測(cè)試用例。對(duì)于他們認(rèn)為自己無(wú)法完成，且 RVI 無(wú)法從其他開(kāi)源解決方案中獲取的功能，我們將介入并提供所需的測(cè)試用例。這些功能將更加復(fù)雜，難以手動(dòng)編寫(xiě)，但我們可以通過(guò)我們的測(cè)試合成工具生成這些測(cè)試用例?！?/span>

從合規(guī)到實(shí)施

“建立合規(guī)性面臨兩大挑戰(zhàn)。首先，要確保核心系統(tǒng)能夠正常運(yùn)行；其次，要確保核心系統(tǒng)始終能夠正確運(yùn)行，” Axiomise首席執(zhí)行官 Ashish Darbari 表示。 “雖然基于仿真的單元測(cè)試和合規(guī)性測(cè)試套件能夠解決存在性挑戰(zhàn)（即測(cè)試通過(guò)）的問(wèn)題，但它們并非解決完全合規(guī)性問(wèn)題的理想方案，也就是說(shuō)，無(wú)論指令何時(shí)執(zhí)行，所有指令的所有交錯(cuò)組合都能對(duì)所有操作數(shù)正確運(yùn)行。形式化技術(shù)是進(jìn)行此類(lèi)詳盡分析的自然選擇，并且通過(guò)使用強(qiáng)大的不變量（這些不變量可以通過(guò)形式化模型檢測(cè)工具進(jìn)行驗(yàn)證）不斷成功地證明了這一點(diǎn)。這種方法的優(yōu)勢(shì)在于，除了發(fā)現(xiàn)功能性缺陷外，它還能捕獲死鎖、活鎖、安全性和可靠性問(wèn)題。一旦缺陷被修復(fù)，就會(huì)再次運(yùn)行不變量以獲得詳盡的證明，從而毫無(wú)疑問(wèn)地證明缺陷已被捕獲。場(chǎng)景覆蓋率（六維覆蓋率的一部分）提供了基于證明的對(duì)可能場(chǎng)景的洞察，為架構(gòu)師和驗(yàn)證工程師提供了深入的見(jiàn)解?！?/span>

然而，要完全確信某項(xiàng)功能有效并非易事?！案采w率指標(biāo)就像驗(yàn)證儀表盤(pán)上的不同儀器，每個(gè)指標(biāo)都衡量著一些重要的東西，但沒(méi)有哪個(gè)指標(biāo)能夠單獨(dú)講述完整的故事，”西門(mén)子的帕爾菲說(shuō)道?！按a覆蓋率告訴你哪些邏輯被執(zhí)行過(guò)。功能覆蓋率告訴你哪些場(chǎng)景被測(cè)試過(guò)。斷言覆蓋率確認(rèn)特定屬性在執(zhí)行過(guò)程中是否成立。每個(gè)指標(biāo)都提供了一部分真相，但關(guān)鍵在于——它們講述的都是不同的故事，而且往往是孤立存在的。你的代碼覆蓋率可能非常出色，但卻完全忽略了RISC-V指令流水線(xiàn)中的一個(gè)關(guān)鍵邊界情況。你可能完美地完成了功能場(chǎng)景的測(cè)試，但卻從未真正測(cè)試過(guò)那些對(duì)認(rèn)證至關(guān)重要的架構(gòu)合規(guī)性要點(diǎn)?！?/span>

幾十年來(lái)，用于獲取覆蓋率信息的設(shè)計(jì)測(cè)試流程基本保持不變?！拔覀儠?huì)進(jìn)行大量的壓力測(cè)試，在指定的擴(kuò)展范圍內(nèi)隨機(jī)發(fā)送數(shù)千條指令，”Microchip公司的Selwan說(shuō)道?！拔覀冞€會(huì)使用大量的測(cè)試平臺(tái)來(lái)驗(yàn)證實(shí)現(xiàn)的完整性?！?/span>

測(cè)試執(zhí)行速度越快越好?！拔覀兙徑怛?yàn)證周期挑戰(zhàn)的方法之一是使用硬件輔助驗(yàn)證來(lái)加快測(cè)試執(zhí)行速度，”Synopsys 的 Sutton 表示。“覆蓋率是其中的一部分，因?yàn)樗軒椭懔私鉁y(cè)試內(nèi)容。這并非簡(jiǎn)單地用大量測(cè)試用例進(jìn)行海量測(cè)試，但這無(wú)疑是解決我們之前提到的 10 到 18 個(gè)測(cè)試周期挑戰(zhàn)的一種方法?！?/span>

越來(lái)越多的引擎正被賦予加速驗(yàn)證的使命?！拔覀兊哪繕?biāo)是能夠部署整個(gè)驗(yàn)證流程，這意味著可以使用所有類(lèi)型的驗(yàn)證引擎，”Synopsys 的 Schirrmeister 表示?！斑@涵蓋了從虛擬平臺(tái)架構(gòu)到硬件輔助驗(yàn)證和驗(yàn)證 IP 的整個(gè)過(guò)程，其中驗(yàn)證 IP 對(duì)接口尤為重要。測(cè)試生成工具也融入其中。例如，要考察架構(gòu)覆蓋率——指令、權(quán)限、通過(guò)、異常等。為了測(cè)試這些覆蓋率，可以使用覆蓋組，這些覆蓋組可以在仿真環(huán)境中運(yùn)行。然后還要考察各種場(chǎng)景。因此，情況變得更加復(fù)雜。形式化驗(yàn)證在某些方面表現(xiàn)出色。”

測(cè)試綜合的一項(xiàng)重要功能是它可以針對(duì)多種執(zhí)行引擎?！澳阈枰軌?yàn)榉抡妗?a href="http://www.makelele.cn/analog/" target="_blank">模擬、FPGA 和芯片后測(cè)試環(huán)境綜合測(cè)試內(nèi)容，”Breker 公司的 Hamid 說(shuō)道?！斑@可能包括事務(wù)級(jí)測(cè)試，也可能包括運(yùn)行在內(nèi)核上的軟件。在每個(gè)層級(jí)，測(cè)試覆蓋率都會(huì)提高大約 102 倍。例如，你可以在仿真環(huán)境中測(cè)試10? 個(gè)用例，在模擬環(huán)境中測(cè)試 10?個(gè)用例，在芯片后測(cè)試環(huán)境中測(cè)試10? 個(gè)用例。在芯片后測(cè)試10?或 10?個(gè)用例也是合理的?！?/span>

你不能總是重復(fù)驗(yàn)證同樣的東西。“實(shí)現(xiàn)驗(yàn)證占據(jù)了工程工作的大部分精力，”Arteris 公司的 Stevens 說(shuō)。“這包括微架構(gòu)的極端情況、時(shí)序交互、一致性、順序、安全屬性以及軟件無(wú)法看到的硬件間協(xié)議接口。要實(shí)現(xiàn)完整性，需要仿真、模擬、UVM 環(huán)境、覆蓋率驅(qū)動(dòng)的測(cè)試以及越來(lái)越多地使用形式化驗(yàn)證。與自然映射到指令級(jí)覆蓋率的架構(gòu)測(cè)試不同，實(shí)現(xiàn)完整性很難量化。它很大程度上取決于每個(gè)設(shè)計(jì)的具體結(jié)構(gòu)和接口?！?/span>

覆蓋率指標(biāo)可以顯示您實(shí)現(xiàn)目標(biāo)的進(jìn)展情況?！案采w率指標(biāo)是評(píng)估設(shè)計(jì)驗(yàn)證質(zhì)量的關(guān)鍵，”Microchip 的 Selwan 表示?！肮δ芨采w率與結(jié)構(gòu)覆蓋率指標(biāo)相輔相成，例如語(yǔ)句覆蓋率、分支覆蓋率、條件覆蓋率、翻轉(zhuǎn)覆蓋率和有限狀態(tài)機(jī) (FSM) 覆蓋率。提取高度可配置的嵌入式 IP 核（例如 MIV_RV32）的覆蓋率指標(biāo)更具挑戰(zhàn)性，通常需要進(jìn)行大量測(cè)試才能滿(mǎn)足覆蓋率要求。工具供應(yīng)商目前正在努力改進(jìn)其產(chǎn)品，使其能夠從高度可配置的實(shí)現(xiàn)中提取覆蓋率指標(biāo)?！?/span>

定義這些指標(biāo)需要技術(shù)精湛的工程師?！拔⒓軜?gòu)中哪些部分值得測(cè)量覆蓋率？哪些隊(duì)列容易溢出？這項(xiàng)工作成本不低，而且我不知道有什么自動(dòng)化方法可以實(shí)現(xiàn)，”Hamid說(shuō)道?！翱蛻?hù)必須逐一標(biāo)記他們想要覆蓋的內(nèi)容。這是一個(gè)成本很高的問(wèn)題，但至少我們可以描述它，只要有足夠的時(shí)間和資金，我們就可以著手去做。現(xiàn)在我們發(fā)現(xiàn)這個(gè)系統(tǒng)中的Q5沒(méi)有發(fā)生溢出。這能實(shí)現(xiàn)嗎？它是否可行？如果可行，需要什么樣的場(chǎng)景？這些信息在全局范圍內(nèi)往往是未知的，也就是說(shuō)，沒(méi)有人知道——甚至架構(gòu)師也不知道。我們沒(méi)有足夠的細(xì)節(jié)來(lái)判斷這種情況是否可行。我們正在做出工程決策，確定哪些部分需要確定性地進(jìn)行交叉，而其他部分則隨機(jī)化。但這只是考慮個(gè)別場(chǎng)景，而這些場(chǎng)景的順序安排可能會(huì)導(dǎo)致不同的硬件問(wèn)題?！?/span>

完整性要求理解不同覆蓋類(lèi)型之間的關(guān)系?！皟H僅知道你的 RTL 代碼執(zhí)行到了第 247 行是不夠的，”P(pán)alfy 說(shuō)，“你需要知道在所有重要條件下是否都執(zhí)行到了這一行，相關(guān)的斷言是否正確觸發(fā)，你的測(cè)試計(jì)劃是否真正旨在驗(yàn)證該場(chǎng)景，以及它是否映射到特定的架構(gòu)需求。你需要將所有覆蓋數(shù)據(jù)統(tǒng)一起來(lái)，同時(shí)保持它們之間的關(guān)系、層次結(jié)構(gòu)和可追溯性。想象一下，能夠看到來(lái)自每個(gè)驗(yàn)證引擎（仿真、模擬、形式化測(cè)試）的覆蓋數(shù)據(jù)被智能地合并，同時(shí)保持設(shè)計(jì)結(jié)構(gòu)，跟蹤哪些測(cè)試貢獻(xiàn)了哪些覆蓋，最重要的是，還能顯示其中的差距?！?/span>

驗(yàn)證漏洞

除了實(shí)現(xiàn)層面的覆蓋漏洞之外，如今整個(gè)理念層面也存在覆蓋漏洞。隨著時(shí)間的推移，人們正在努力填補(bǔ)這些漏洞。

“RISC-V 生態(tài)系統(tǒng)的一大缺陷在于核心指令集架構(gòu) (ISA) 之外缺乏標(biāo)準(zhǔn)化的硬件接口，”Stevens 表示?！翱蓴U(kuò)展的片上系統(tǒng) (SoC) 集成依賴(lài)于處理器與系統(tǒng)其他部分（包括互連）之間可預(yù)測(cè)、可互操作且可驗(yàn)證的連接。正因如此，實(shí)現(xiàn)驗(yàn)證才顯得尤為重要。雖然許多 RISC-V 開(kāi)發(fā)人員采用了現(xiàn)有的接口，例如 AMBA CHI，但這些規(guī)范的篇幅已超過(guò) 1000 頁(yè)，其中很多內(nèi)容對(duì)于典型的 RISC-V 系統(tǒng)而言都是不必要的。真正能夠造福社區(qū)的是一個(gè)專(zhuān)注于 RISC-V 的子集，或者一套與實(shí)際應(yīng)用場(chǎng)景相符的精簡(jiǎn)接口標(biāo)準(zhǔn)。這樣的標(biāo)準(zhǔn)化將顯著減少重復(fù)的驗(yàn)證工作，提高覆蓋率的一致性，并加速多廠(chǎng)商之間的互操作性?！?/span>

有些差距遠(yuǎn)不止功能性問(wèn)題?！拔易罱鸵晃还こ處熈倪^(guò)，他剛為一個(gè)汽車(chē)應(yīng)用完成了RISC-V內(nèi)核的流片，”帕爾菲說(shuō)道?！斑@個(gè)內(nèi)核通過(guò)了所有架構(gòu)測(cè)試，但在軟件啟動(dòng)三個(gè)月后，他們發(fā)現(xiàn)分支預(yù)測(cè)器的準(zhǔn)確率跟拋硬幣一樣低。技術(shù)上正確，但功能上毫無(wú)用處。他們承諾的所有性能根本沒(méi)有實(shí)現(xiàn)。而且世界上沒(méi)有任何測(cè)試套件能發(fā)現(xiàn)這個(gè)問(wèn)題，因?yàn)樾阅茯?yàn)證并非生態(tài)系統(tǒng)的標(biāo)準(zhǔn)化內(nèi)容。每個(gè)人都在構(gòu)建自己的定制基礎(chǔ)設(shè)施來(lái)回答‘這東西真的運(yùn)行得快嗎？’這個(gè)問(wèn)題。”

然而，速度快也會(huì)帶來(lái)其他問(wèn)題。“對(duì)于某些設(shè)計(jì)，當(dāng)你提高時(shí)鐘性能時(shí)，設(shè)計(jì)中的某些部分會(huì)變成熱點(diǎn)，你真的需要開(kāi)始關(guān)注這些問(wèn)題了，”凱爾夫問(wèn)道?！拔覀兛梢赃\(yùn)行實(shí)際工作負(fù)載和合成工作負(fù)載，看看是否會(huì)觸發(fā)熱點(diǎn)。這與功耗問(wèn)題息息相關(guān)。真正關(guān)注這一點(diǎn)的公司，例如汽車(chē)和數(shù)據(jù)中心，希望確保他們能夠測(cè)試這些熱點(diǎn)，并通過(guò)調(diào)整時(shí)鐘來(lái)驗(yàn)證他們能夠處理熱阻和功耗問(wèn)題?！?/span>

汽車(chē)行業(yè)和其他一些應(yīng)用領(lǐng)域一樣，給這個(gè)問(wèn)題增添了新的層面。“如果你正在為汽車(chē)或工業(yè)應(yīng)用構(gòu)建 RISC-V 系統(tǒng)，那么在安全性和可靠性驗(yàn)證方面，你將面臨全新的挑戰(zhàn)，”P(pán)alfy 說(shuō)道。“ISO 26262 標(biāo)準(zhǔn)并不關(guān)心你是否通過(guò)了 ISA 測(cè)試。它關(guān)注的是故障注入、錯(cuò)誤處理以及功能安全機(jī)制的有效性?，F(xiàn)有的測(cè)試套件在設(shè)計(jì)之初并沒(méi)有考慮到這些，所以你只能從零開(kāi)始。”

其他技術(shù)的作用

形式化驗(yàn)證增加了一系列互補(bǔ)的功能，這些功能發(fā)揮著重要作用。“早期的 RISC-V 討論中就提到了形式化方法，”P(pán)alfy 說(shuō)?！爱?dāng)時(shí)有一種樂(lè)觀的想法：‘這是一個(gè)開(kāi)放規(guī)范。我們可以對(duì)整個(gè)內(nèi)核進(jìn)行形式化驗(yàn)證，使其符合指令集架構(gòu) (ISA)，并證明其正確性?！@在理論上很美好，但在實(shí)踐中卻非常殘酷。”

然而，形式化驗(yàn)證仍然發(fā)揮著重要作用?！靶问交?yàn)證正成為解決方案中越來(lái)越重要的組成部分，”史蒂文斯說(shuō)道?！八诩軜?gòu)合規(guī)性方面尤其強(qiáng)大——確保指令集架構(gòu)（ISA）屬性對(duì)所有合法指令序列都成立——以及在實(shí)現(xiàn)驗(yàn)證中強(qiáng)制執(zhí)行硬件協(xié)議的正確性。但形式化驗(yàn)證并不能取代動(dòng)態(tài)驗(yàn)證或系統(tǒng)級(jí)驗(yàn)證，尤其是在涉及完整的片上系統(tǒng)（SoC）行為和實(shí)際工作負(fù)載時(shí)。在實(shí)踐中，形式化方法扮演著補(bǔ)充角色，證明深度邊界情況的正確性，而仿真和模擬則建立端到端的完整性?！?/span>

形式化驗(yàn)證正被積極應(yīng)用?！安捎眯问交?yàn)證提供了一種方法，可以在一定范圍內(nèi)全面測(cè)試我們?cè)O(shè)計(jì)的有效性，從而從一開(kāi)始就提高代碼質(zhì)量，”Selwan說(shuō)道?！办o態(tài)形式化工具被廣泛用于及早發(fā)現(xiàn)和解決缺陷，從而最大限度地縮短后續(xù)驗(yàn)證周期。形式化驗(yàn)證是我們開(kāi)發(fā)周期中的一個(gè)重要環(huán)節(jié)，通過(guò)驗(yàn)證，它將繼續(xù)在實(shí)現(xiàn)高質(zhì)量嵌入式IP產(chǎn)品方面發(fā)揮重要作用?！?/span>

新的人工智能功能也可以得到充分利用。“RISC-V 是應(yīng)用智能體人工智能進(jìn)行驗(yàn)證的絕佳領(lǐng)域，” ChipAgents首席執(zhí)行官 William Wang 表示。“我們已經(jīng)看到智能體人工智能在形式化驗(yàn)證方面取得了顯著成功，尤其因?yàn)樘幚砥髟O(shè)計(jì)主要由控制信號(hào)構(gòu)成，這使得它們非常適合形式化推理和符號(hào)探索。這與人工智能加速器形成鮮明對(duì)比，后者往往涉及更多以數(shù)據(jù)為中心的流程，不太適合純粹的形式化技術(shù)。隨著 RISC-V 的普及，人工智能驅(qū)動(dòng)的形式化方法可以顯著加速架構(gòu)一致性驗(yàn)證和實(shí)現(xiàn)驗(yàn)證，為確保日益復(fù)雜、可配置的設(shè)計(jì)的正確性和覆蓋率提供可擴(kuò)展的方法?！?/span>

參考鏈接

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