當前位置： CompoTech China > 關鍵技術和應用 >
利用先進形式驗證工具來高效完成RISC-V處理器驗證
前言：
作者：Laurent Arditi, Paul Sargent, Thomas Aird
職務：Codasip高級驗證/形式驗證工程師
我們在上一篇技術白皮書《基于形式驗證的高效RISC-V處理器驗證方法》中，以Codasip L31這款用于微控制器應用的32位中端嵌入式RISC-V處理器內核為例，介紹了一個基于形式驗證的、易于調動的RISC-V處理器驗證程序。它與RISC-V ISA黃金模型和RISC-V合規性自動生成的檢查一起，展示了如何有效地定位那些無法進行仿真的漏洞。
RISC-V的開放性允許定制和擴展基于RISC-V內核的架構和微架構，以滿足特定需求。這種對設計自由的渴望也正在將驗證部分的職責轉移到不斷壯大的開發人員社群。然而，隨著越來越多的企業和開發人員轉型RISC-V，大家才發現處理器驗證絕非易事。新標準由于其新穎和靈活性而帶來的新功能會在無意中產生規范和設計漏洞，因此處理器驗證是處理器開發過程中一項非常重要的環節。
在復雜性一般的RISC-V處理器內核的開發過程中，會發現數百甚至數千個漏洞。當引入更多高級特性的時候，也會引入復雜程度各不相同的新漏洞。而某些類型的漏洞過于復雜，導致在仿真環節都無法找到它們。因此必須通過添加形式驗證來賦能RTL驗證方法。從極端漏洞到隱匿式漏洞，形式驗證能夠讓您在合理的處理時間內詳盡地探索所有狀態。
在本文中，我們將以西門子EDA處理器驗證應用程序為例，結合Codasip L31這款廣受歡迎的RISC-V處理器IP提供的特性，來介紹一種利用先進的EDA工具，在實際設計工作中對處理器進行驗證的具體方法。這種驗證方法通過為每條指令提供一組專用的斷言模板來實現高度自動化，不再需要手動設計，從而提高了形式驗證團隊的工作效率。
如何使用西門子EDA處理器驗證應用程序
在我們使用該工具之前，需要為Codasip L31 RISC-V內核進行形式驗證設置。此設置類似于使用帶有抽象、約束等基于斷言的驗證（ABV）方法來形式驗證標準斷言的設置。
該工具允許驗證特定類別的指令，并啟用或禁用某些資源檢查。有了這個工具，我們的驗證可以從一個簡化的空間開始，這包括：
• 只有最簡單的指令，例如只有整數運算和邏輯指令。
• 只有最簡單（但最重要）的檢查。例如通用寄存器的更新。稍后可以添加的其他檢查指的是系統寄存器（CSR）或程序計數器（PC）的更新以及內存訪問。
• 只有主功能模式：沒有中斷、中止、異常或調試訪問。
這三個正交約束可以根據微架構特征的關鍵程度逐一放寬。經典的形式驗證技術可用于幫助獲得檢查器斷言的結果：抽象、設計縮減、案例拆分、不變量生成、半形式漏洞搜尋等。
結果
這種基于形式的方法使我們能夠找到極端情況，并深入了解改進我們的仿真和測試平臺。在其他基于仿真的驗證流程運行而未發現新漏洞之后，此驗證工作在項目快結束時完成，這使我們能夠找到真正的和重要的漏洞。
我們可以特別關注其中的三個漏洞，它們從用于L31的西門子EDA處理器驗證應用程序中找到。以下是發現和彌補這三個漏洞的具體方法：
1. 分支預測器損壞
有了這個漏洞，返回到先前持有跳轉/分支指令的PC地址會導致分支預測器錯誤地預測跳轉到另一個地址。當滿足以下條件時，會發現這種極端情況：
自修改代碼
當添加未定義的指令（新指令異常）時，也會出現此漏洞極其罕見的版本：
該漏洞是通過檢查PC值的斷言發現的，直接后果是錯誤地執行了一個分支指令，導致代碼執行錯誤。通過正確清除分支預測和流水線的緩沖數據來修復此漏洞。
使用西門子EDA處理器驗證應用程序查找此漏洞需要8個周期和15分鐘的運行時間。在仿真中重現該漏洞需要一個支持自修改代碼的隨機生成器，該代碼可正好返回相同的地址并將該地址從分支修改為另一種類型的指令。換句話說，隨機生成器不可能做到這一點。只有知道漏洞詳細信息的定向序列可以做到。
2. 同一條指令的多次執行
出現這個漏洞，NPC（下一個 PC）單元停頓就會出現，這會導致多次獲取相同的地址。每條指令執行并退出。
當滿足以下條件時，會出現這種極端情況：
• 內核配置有TCM。
• 在提取總線上可以看到特定的延遲。
• 在流水線內可以看到特定的停頓。
該漏洞會直接在流水線的其余部分造成未被正確處理的停頓，導致同一指令的多次執行。可以通過正確處理其余流水線中的停頓來修復此漏洞。
使用西門子EDA處理器驗證應用程序查找此漏洞需要5個周期和10分鐘的運行時間。在仿真中再現它需要隨機延遲和停頓的隨機模式，但也需要相當多的“運氣”來再現這個特定序列。
3. 合法的 FENCE.I 指令被認為是非法的
出現這個漏洞，內存屏障會由CSR單元處理。如果與CSR操作的CSR地址位元對應的指令位元（位 [31:20]）與某些CSR寄存器（例如調試、計數器）匹配，則指令可能會被錯誤地標記為非法。
當滿足以下條件時，會發現這種極端情況：
• imm[11:0]/rs1/rd 中有隨機位元。
• 這些位元與其他一些非法指令相匹配。
該漏洞的直接后果是錯誤地引發了非法指令異常。通過正確解碼流水線每個部分的完整指令可修復此漏洞。
使用西門子EDA處理器驗證應用程序查找此漏洞僅用了8個周期和5分鐘的運行時間。因為編譯器只會創建最簡單的二進制編碼實現，所以很難在仿真中重現該漏洞。它需要一個特殊的編譯器來創建合法編碼的變體，或者使用各種編碼進行特殊的定向測試。
從中發現的優勢/結論
應用這種方法可以提高驗證團隊的工作效率。在項目的關鍵階段提高效率。雖然在開始時構建正確的設置需要付出努力，但隨著我們添加新的指令類別和新的檢查器，進度就會加快。這個“最佳點”是我們發現大多數問題的地方，隨著放寬約束以允許該工具探索更深奧的操作模式，速度就開始放緩。
圖 1 驗證L31 RISC-V內核的最佳效率的最佳點（來源：Codasip）
總的來說，因為使用西門子EDA處理器驗證應用程序驗證整個CPU所需的總體工作量遠低于手動達到類似驗證質量所需的工作量，所以使用該工具是相當高效的。在總共30個漏洞中，有15個是通過形式驗證發現的。
表1 仿真 vs形式驗證
|
驗證技術 |
仿真驗證 |
形式驗證 |
|
驗證基礎設施 |
測試臺、隨機指令生成器、檢查器 |
西門子EDA處理器驗證應用程序提供的斷言 |
|
開發時間 |
人-年（person-years of efforts） |
時間極短（只需要自定義生成的設置） |
|
運行時間 |
成千上萬次的測試/案例和成千上萬個仿真小時 |
在2小時的運行時間內完成完整驗證（最佳情況下） |
當結合在一起到達高質量水平時，仿真和形式驗證是非常強大的，并使我們能夠促進改進驗證的良性循環。
圖 2 通過持續改進達到一流的品質（來源：Codasip）
該解決方案在Codasip L31這種3級流水線微控制器上的實施被證明是可行的，現在已部署到Codasip的下一代RISC-V內核中，包括嵌入式和應用內核。借助在L31上使用西門子EDA處理器驗證應用程序積累的知識，即使應用內核更復雜，也可以減少建立穩健環境所需的工作量。而Codasip的下一步計劃包括進一步研究該工具如何應用于超標量和亂序內核，以及支持新的 RISC-V 擴展。
補充閱讀
• RISC-V處理器的高效驗證——技術白皮書：https://codasip.com/papers/efficientverification-of-riscv-processors-technical-paper/
• 構建用于處理器驗證的瑞士奶酪模型方法 - 博客文章：https://codasip.com/2022/04/29/building-a-swiss-cheese-model-approach-for-processorverification/
本文摘錄于《基于形式的高效 RISC-V 處理器驗證方法 – 形式化驗證》白皮書，出版人為總部位于歐洲的全球領先RISC-V供應商和處理器解決方案領導者，該公司的處理器IP目前已部署在數十億顆芯片中。Codasip通過開放的RISC-V ISA、Codasip Studio處理器設計自動化工具與高品質的處理器IP相結合，為客戶提供定制計算。這種創新方法能夠輕松實現定制和差異化設計，從而開發出高性能的、改變游戲規則的產品，實現真正意義上的轉型。如希望得到該白皮書的完整版本，可瀏覽Codasip中文網站或者關注該公司微信公眾號。
該技術白皮書英文版下載鏈接：https://codasip.com/papers/a-formal-based-approach-for-efficient-riscv-processor-verification
本月熱點 HOME
