作者：Laurent Arditi, Paul Sargent, Thomas Aird
職務(wù)：Codasip高級(jí)驗(yàn)證/形式驗(yàn)證工程師
我們?cè)谏弦黄夹g(shù)白皮書《基于形式驗(yàn)證的高效RISC-V處理器驗(yàn)證方法》中，以Codasip L31這款用于微控制器應(yīng)用的32位中端嵌入式RISC-V處理器內(nèi)核為例，介紹了一個(gè)基于形式驗(yàn)證的、易于調(diào)動(dòng)的RISC-V處理器驗(yàn)證程序。它與RISC-V ISA黃金模型和RISC-V合規(guī)性自動(dòng)生成的檢查一起，展示了如何有效地定位那些無法進(jìn)行仿真的漏洞。
(資料圖片)
RISC-V的開放性允許定制和擴(kuò)展基于RISC-V內(nèi)核的架構(gòu)和微架構(gòu)，以滿足特定需求。這種對(duì)設(shè)計(jì)自由的渴望也正在將驗(yàn)證部分的職責(zé)轉(zhuǎn)移到不斷壯大的開發(fā)人員社群。然而，隨著越來越多的企業(yè)和開發(fā)人員轉(zhuǎn)型RISC-V，大家才發(fā)現(xiàn)處理器驗(yàn)證絕非易事。新標(biāo)準(zhǔn)由于其新穎和靈活性而帶來的新功能會(huì)在無意中產(chǎn)生規(guī)范和設(shè)計(jì)漏洞，因此處理器驗(yàn)證是處理器開發(fā)過程中一項(xiàng)非常重要的環(huán)節(jié)。
在復(fù)雜性一般的RISC-V處理器內(nèi)核的開發(fā)過程中，會(huì)發(fā)現(xiàn)數(shù)百甚至數(shù)千個(gè)漏洞。當(dāng)引入更多高級(jí)特性的時(shí)候，也會(huì)引入復(fù)雜程度各不相同的新漏洞。而某些類型的漏洞過于復(fù)雜，導(dǎo)致在仿真環(huán)節(jié)都無法找到它們。因此必須通過添加形式驗(yàn)證來賦能RTL驗(yàn)證方法。從極端漏洞到隱匿式漏洞，形式驗(yàn)證能夠讓您在合理的處理時(shí)間內(nèi)詳盡地探索所有狀態(tài)。
在本文中，我們將以西門子EDA處理器驗(yàn)證應(yīng)用程序?yàn)槔?，結(jié)合Codasip L31這款廣受歡迎的RISC-V處理器IP提供的特性，來介紹一種利用先進(jìn)的EDA工具，在實(shí)際設(shè)計(jì)工作中對(duì)處理器進(jìn)行驗(yàn)證的具體方法。這種驗(yàn)證方法通過為每條指令提供一組專用的斷言模板來實(shí)現(xiàn)高度自動(dòng)化，不再需要手動(dòng)設(shè)計(jì)，從而提高了形式驗(yàn)證團(tuán)隊(duì)的工作效率。
如何使用西門子EDA處理器驗(yàn)證應(yīng)用程序
在我們使用該工具之前，需要為Codasip L31 RISC-V內(nèi)核進(jìn)行形式驗(yàn)證設(shè)置。此設(shè)置類似于使用帶有抽象、約束等基于斷言的驗(yàn)證（ABV）方法來形式驗(yàn)證標(biāo)準(zhǔn)斷言的設(shè)置。
該工具允許驗(yàn)證特定類別的指令，并啟用或禁用某些資源檢查。有了這個(gè)工具，我們的驗(yàn)證可以從一個(gè)簡(jiǎn)化的空間開始，這包括：
? 只有最簡(jiǎn)單的指令，例如只有整數(shù)運(yùn)算和邏輯指令。
? 只有最簡(jiǎn)單（但最重要）的檢查。例如通用寄存器的更新。稍后可以添加的其他檢查指的是系統(tǒng)寄存器（CSR）或程序計(jì)數(shù)器（PC）的更新以及內(nèi)存訪問。
? 只有主功能模式：沒有中斷、中止、異?；蛘{(diào)試訪問。
這三個(gè)正交約束可以根據(jù)微架構(gòu)特征的關(guān)鍵程度逐一放寬。經(jīng)典的形式驗(yàn)證技術(shù)可用于幫助獲得檢查器斷言的結(jié)果：抽象、設(shè)計(jì)縮減、案例拆分、不變量生成、半形式漏洞搜尋等。
結(jié)果
這種基于形式的方法使我們能夠找到極端情況，并深入了解改進(jìn)我們的仿真和測(cè)試平臺(tái)。在其他基于仿真的驗(yàn)證流程運(yùn)行而未發(fā)現(xiàn)新漏洞之后，此驗(yàn)證工作在項(xiàng)目快結(jié)束時(shí)完成，這使我們能夠找到真正的和重要的漏洞。
我們可以特別關(guān)注其中的三個(gè)漏洞，它們從用于L31的西門子EDA處理器驗(yàn)證應(yīng)用程序中找到。以下是發(fā)現(xiàn)和彌補(bǔ)這三個(gè)漏洞的具體方法：
1. 分支預(yù)測(cè)器損壞
有了這個(gè)漏洞，返回到先前持有跳轉(zhuǎn)/分支指令的PC地址會(huì)導(dǎo)致分支預(yù)測(cè)器錯(cuò)誤地預(yù)測(cè)跳轉(zhuǎn)到另一個(gè)地址。當(dāng)滿足以下條件時(shí)，會(huì)發(fā)現(xiàn)這種極端情況：
自修改代碼
image001.png
當(dāng)添加未定義的指令（新指令異常）時(shí)，也會(huì)出現(xiàn)此漏洞極其罕見的版本：
image003.png
該漏洞是通過檢查PC值的斷言發(fā)現(xiàn)的，直接后果是錯(cuò)誤地執(zhí)行了一個(gè)分支指令，導(dǎo)致代碼執(zhí)行錯(cuò)誤。通過正確清除分支預(yù)測(cè)和流水線的緩沖數(shù)據(jù)來修復(fù)此漏洞。
使用西門子EDA處理器驗(yàn)證應(yīng)用程序查找此漏洞需要8個(gè)周期和15分鐘的運(yùn)行時(shí)間。在仿真中重現(xiàn)該漏洞需要一個(gè)支持自修改代碼的隨機(jī)生成器，該代碼可正好返回相同的地址并將該地址從分支修改為另一種類型的指令。換句話說，隨機(jī)生成器不可能做到這一點(diǎn)。只有知道漏洞詳細(xì)信息的定向序列可以做到。
2. 同一條指令的多次執(zhí)行
出現(xiàn)這個(gè)漏洞，NPC（下一
個(gè) PC）單元停頓就會(huì)出現(xiàn)，這會(huì)導(dǎo)致多次獲取相同的地址。每條指令執(zhí)行并退出。
當(dāng)滿足以下條件時(shí)，會(huì)出現(xiàn)這種極端情況：
? 內(nèi)核配置有TCM。
? 在提取總線上可以看到特定的延遲。
? 在流水線內(nèi)可以看到特定的停頓。
該漏洞會(huì)直接在流水線的其余部分造成未被正確處理的停頓，導(dǎo)致同一指令的多次執(zhí)行?？梢酝ㄟ^正確處理其余流水線中的停頓來修復(fù)此漏洞。
使用西門子EDA處理器驗(yàn)證應(yīng)用程序查找此漏洞需要5個(gè)周期和10分鐘的運(yùn)行時(shí)間。在仿真中再現(xiàn)它需要隨機(jī)延遲和停頓的隨機(jī)模式，但也需要相當(dāng)多的“運(yùn)氣”來再現(xiàn)這個(gè)特定序列。
3. 合法的 FENCE.I 指令被認(rèn)為是非法的
出現(xiàn)這個(gè)漏洞，內(nèi)存屏障會(huì)由CSR單元處理。如果與CSR操作的CSR地址位元對(duì)應(yīng)的指令位元（位 [31:20]）與某些CSR寄存器（例如調(diào)試、計(jì)數(shù)器）匹配，則指令可能會(huì)被錯(cuò)誤地標(biāo)記為非法。
當(dāng)滿足以下條件時(shí)，會(huì)發(fā)現(xiàn)這種極端情況：
? imm[11:0]/rs1/rd 中有隨機(jī)位元。
? 這些位元與其他一些非法指令相匹配。
image005.jpg
該漏洞的直接后果是錯(cuò)誤地引發(fā)了非法指令異常。通過正確解碼流水線每個(gè)部分的完整指令可修復(fù)此漏洞。
使用西門子EDA處理器驗(yàn)證應(yīng)用程序查找此漏洞僅用了8個(gè)周期和5分鐘的運(yùn)行時(shí)間。因?yàn)榫幾g器只會(huì)創(chuàng)建最簡(jiǎn)單的二進(jìn)制編碼實(shí)現(xiàn)，所以很難在仿真中重現(xiàn)該漏洞。它需要一個(gè)特殊的編譯器來創(chuàng)建合法編碼的變體，或者使用各種編碼進(jìn)行特殊的定向測(cè)試。
從中發(fā)現(xiàn)的優(yōu)勢(shì)/結(jié)論
應(yīng)用這種方法可以提高驗(yàn)證團(tuán)隊(duì)的工作效率。在項(xiàng)目的關(guān)鍵階段提高效率。雖然在開始時(shí)構(gòu)建正確的設(shè)置需要付出努力，但隨著我們添加新的指令類別和新的檢查器，進(jìn)度就會(huì)加快。這個(gè)“最佳點(diǎn)”是我們發(fā)現(xiàn)大多數(shù)問題的地方，隨著放寬約束以允許該工具探索更深?yuàn)W的操作模式，速度就開始放緩。
image007.png
圖 1 驗(yàn)證L31 RISC-V內(nèi)核的最佳效率的最佳點(diǎn)（來源：Codasip）
總的來說，因?yàn)槭褂梦鏖T子EDA處理器驗(yàn)證應(yīng)用程序驗(yàn)證整個(gè)CPU所需的總體工作量遠(yuǎn)低于手動(dòng)達(dá)到類似驗(yàn)證質(zhì)量所需的工作量，所以使用該工具是相當(dāng)高效的。在總共30個(gè)漏洞中，有15個(gè)是通過形式驗(yàn)證發(fā)現(xiàn)的。
表1仿真 vs形式驗(yàn)證
