你的位置:首頁 > 互連技術(shù) > 正文

基于形式的高效 RISC-V 處理器驗(yàn)證方法

發(fā)布時(shí)間:2023-05-31 責(zé)任編輯:lina

【導(dǎo)讀】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é)。


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)。


在本文中,我們將介紹一個(gè)基于形式驗(yàn)證的、易于調(diào)動(dòng)的 RISC-V 處理器驗(yàn)證程序。與 RISC-V ISA 黃金模型和 RISC-V 合規(guī)性自動(dòng)生成的檢查一起,展示了如何有效地定位那些無法進(jìn)行仿真的漏洞。通過為每條指令提供一組專用的斷言模板來實(shí)現(xiàn)高度自動(dòng)化,不再需要手動(dòng)設(shè)計(jì),從而提高了形式驗(yàn)證團(tuán)隊(duì)的工作效率。


1、基于先進(jìn)內(nèi)核的處理器開發(fā)


嵌入式系統(tǒng)的應(yīng)用越來越廣泛,同時(shí)對(duì)處理器的性能、功耗和面積(PPA)要求越來越高,因此我們將這樣的產(chǎn)業(yè)和技術(shù)背景下用實(shí)際案例來分析處理器的驗(yàn)證。Codasip L31 是一款用于微控制器應(yīng)用的 32 位中端嵌入式 RISC-V 處理器內(nèi)核。作為一款多功能、低功耗、通用型的 CPU,它實(shí)現(xiàn)了性能和功耗的理想平衡。從物聯(lián)網(wǎng)設(shè)備到工業(yè)和汽車控制,或作為大型系統(tǒng)中的深度嵌入式內(nèi)核,L31可在一個(gè)非常小巧緊湊的硅片面積中實(shí)現(xiàn)本地處理能力。L31是通過 Codasip Studio 使用 CodAL 語言設(shè)計(jì)而成,該內(nèi)核完全可定制,包括經(jīng)典的擴(kuò)展和特性,以及實(shí)現(xiàn)這些擴(kuò)展和特性所需的高效和徹底的驗(yàn)證。


基于形式的高效 RISC-V 處理器驗(yàn)證方法

圖1 Codasip L31處理器內(nèi)核架構(gòu)圖解(來源:Codasip)


表 1 Codasip L31內(nèi)核展示了RISC-V處理器的優(yōu)異特性


特性

描述

指令集架構(gòu) (ISA)

RV32 I/M/C/F/B

流水線

3級(jí)順序流水線

分支預(yù)測(cè)器

可選,優(yōu)化過的單線程性能

并行乘法器

并行實(shí)現(xiàn),單周期乘法

序列除法器

順序執(zhí)行

內(nèi)存保護(hù)

●具有 2/4/8/16 個(gè)區(qū)域的可選MPU

●具有 2/4/8/16 個(gè)區(qū)域的物理內(nèi)存屬性

機(jī)器和用戶權(quán)限模式

緊耦合存儲(chǔ)器 (TCM)

●指令和數(shù)據(jù)TCM

●可定制大小高達(dá)2MB

AHB-Lite TCM 輔助端口

接口

用于獲取和數(shù)據(jù)的 32 位 AHB-Lite 接口(帶緩存的 AXI-Lite)

浮點(diǎn)單元 (FPU)

可選,單精度

調(diào)試

●標(biāo)準(zhǔn) RISC-V 調(diào)試

●2/4 JTAG

●2-8 個(gè)斷點(diǎn)和觀察點(diǎn)

●系統(tǒng)總線接入

中斷

●中斷控制器

●標(biāo)準(zhǔn) RISC-V CLINT   執(zhí)行

●多達(dá) 128 個(gè)中斷

●WFI(等待中斷)

●NMI(不可屏蔽中斷)


2     創(chuàng)建最優(yōu)的RISC-V處理器驗(yàn)證方法


處理器驗(yàn)證需要制定合適的策略、勤勉的工作流程和完整性,而方興未艾的、更加靈活的RISC-V處理器開發(fā)則需要針對(duì)自己處理器功能設(shè)置做詳盡的驗(yàn)證規(guī)劃;也需要參考一些內(nèi)核供應(yīng)商的內(nèi)外部因素,比如該供應(yīng)商自己的開發(fā)工具體現(xiàn)和外部開發(fā)工具伙伴,以及同系、同款或者同廠內(nèi)核的出貨量等。


驗(yàn)證處理器意味著需要考慮諸多不確定性。最終產(chǎn)品將運(yùn)行什么軟件?用例是什么?可能發(fā)生哪些異步事件?這些未知數(shù)意味著較大的驗(yàn)證范圍。然而,覆蓋整個(gè)處理器狀態(tài)空間是無法實(shí)現(xiàn)的,這也不是Codasip這樣的領(lǐng)先內(nèi)核供應(yīng)商的目標(biāo)。


在確保處理器品質(zhì)的同時(shí),充分利用時(shí)間和資源才是處理器驗(yàn)證的正解。明智的處理器驗(yàn)證意味著在產(chǎn)品開發(fā)過程中盡早并高效地發(fā)現(xiàn)相關(guān)漏洞。在頂層方面,Codasip提供了多種創(chuàng)新的驗(yàn)證路徑,其驗(yàn)證方法基于以下內(nèi)容:


  • 驗(yàn)證是在處理器開發(fā)期間與設(shè)計(jì)團(tuán)隊(duì)合作完成的。

  • 驗(yàn)證是所有行業(yè)標(biāo)準(zhǔn)技術(shù)的組合。使用多種技術(shù)可以讓您最大限度地發(fā)揮每一種技術(shù)的潛力,并有效地覆蓋盡可能多的極端情況。

  • 驗(yàn)證需持續(xù)進(jìn)行。有效的辦法是運(yùn)用隨著處理器復(fù)雜程度而不斷發(fā)展的技術(shù)組合。


在驗(yàn)證L31內(nèi)核時(shí),我們的想法是讓仿真和形式驗(yàn)證相輔相成。


2.1仿真的優(yōu)勢(shì)和目的


仿真實(shí)際上不可或缺,它允許我們?cè)趦蓚€(gè)級(jí)別上進(jìn)行驗(yàn)證設(shè)計(jì):


  • 頂層仿真(Top-level),主要是為了確保設(shè)計(jì)在最常見的情況下符合其規(guī)范(CPU 的 ISA)。

  • 塊級(jí)仿真(Block-level),以確保微架構(gòu)按照預(yù)期設(shè)計(jì)。然而,很難將這些檢查與頂層架構(gòu)規(guī)范聯(lián)系起來,因?yàn)檫@通常依賴于定向隨機(jī)測(cè)試生成,因此能夠應(yīng)付棘手和不尋常的情況。


頂層仿真通常不像塊級(jí)仿真那樣特意強(qiáng)調(diào)設(shè)計(jì)。因此,它可以實(shí)現(xiàn)針對(duì) ISA 的設(shè)計(jì)的整體驗(yàn)證。


2.2形式驗(yàn)證的優(yōu)勢(shì)和目的


形式驗(yàn)證使用數(shù)學(xué)技術(shù)對(duì)以斷言形式編寫的問題提供有關(guān)設(shè)計(jì)的明確答案。


形式驗(yàn)證工具對(duì)斷言和設(shè)計(jì)的組合進(jìn)行詳盡的分析。不需要指定任何刺激,除了指定一些非正常情況以避免假漏洞。該驗(yàn)證工具可以提供詳盡的“已證實(shí)”答案或“失敗”答案,同時(shí)生成顯示刺激的波形,證明斷言是錯(cuò)誤的。在大型和復(fù)雜的設(shè)計(jì)中,工具有時(shí)只能提供有限的證明,這意味著從重置到特定數(shù)量的周期都不存在漏洞場(chǎng)景。同時(shí)也存在不同的技術(shù)方法來增加該周期循環(huán)次數(shù),或獲得“已證明”或“失敗”的答案。


形式驗(yàn)證用于以下情況:


  • 為完整的驗(yàn)證一個(gè)模塊,潛在地消除了任何仿真的需要。由于形式驗(yàn)證的計(jì)算復(fù)雜性,形式化驗(yàn)收(sign-off)僅限于小模塊。

  • 除了仿真之外,還要驗(yàn)證一個(gè)模塊,即使是個(gè)大模塊,因?yàn)樾问津?yàn)證能夠在極端情況下找到漏洞,而隨機(jī)仿真只能“靠運(yùn)氣”找到,而且概率非常低。

  • 處理一些仿真不充分的驗(yàn)證任務(wù),例如時(shí)鐘門控、X態(tài)傳播(X-propagation)、數(shù)據(jù)增量處理(CDC)、等價(jià)性檢查等。

  • 幫助調(diào)查缺少調(diào)試信息的已知漏洞,并確定潛在的設(shè)計(jì)修復(fù)。

  • 對(duì)漏洞進(jìn)行分類和識(shí)別,以便通過形式驗(yàn)證來學(xué)習(xí)和改進(jìn)測(cè)試平臺(tái)/仿真。

  • 為了潛在地幫助仿真,填充覆蓋范圍中的漏洞。


3解決方案:一種基于形式驗(yàn)證的高效的 RISC-V 處理器驗(yàn)證方法


為了獲得一種高效的RISC-V處理器驗(yàn)證方法,我們決定以采用西門子EDA 處理器驗(yàn)證APP來高效驗(yàn)證Codasip  L31 RISC-V 內(nèi)核為例,來進(jìn)行詳盡的說明。該工具的目標(biāo)是確保 RTL 級(jí)別的處理器設(shè)計(jì)正確且詳盡地實(shí)現(xiàn)指令集架構(gòu) (ISA)規(guī)范,而本文希望介紹的是一種端到端的解決方案


1.該工具從一個(gè)頂層并有效的“黃金模型”中生成以下:

  • 在 Verilog 語言中,ISA 的單周期執(zhí)行模型。

  • 一組斷言,用于檢查待測(cè)試模塊 (DUT)和模型 (M)在架構(gòu)級(jí)別的功能是否相同。

注意:這并沒有進(jìn)行任何正式等價(jià)性檢查。

2.當(dāng)在 DUT 中獲取新指令 (I)時(shí),會(huì)捕獲架構(gòu)狀態(tài) (DUT-init)。

3.該指令在流水線中運(yùn)行。

4.捕獲另一個(gè)架構(gòu)狀態(tài)(DUT-final)。

5.M 被輸入 DUT-init 和 I,并計(jì)算出一個(gè)新的 M-final 狀態(tài)。

6.斷言檢查 M-final 和 DUT-final 中的資源是否具有相同的值。


基于形式的高效 RISC-V 處理器驗(yàn)證方法

圖 2 3 級(jí) L31 內(nèi)核的端到端驗(yàn)證流程(當(dāng)驗(yàn)證指令 I 既沒有停止也沒有清除緩存數(shù)據(jù)時(shí))


這種端到端的驗(yàn)證方法可以在比整個(gè)CPU 更小、更簡(jiǎn)單的模塊(例如數(shù)據(jù)緩存)上合理實(shí)現(xiàn)??梢栽诰彺嫔蠈懭攵说蕉藬嘌?,以驗(yàn)證寫入特定地址的數(shù)據(jù)是否從同一地址正確讀取。這使用了眾所周知的形式驗(yàn)證技術(shù),例如記分牌算法。


然而,對(duì)于 CPU來說,手動(dòng)編寫這樣的斷言是不可行的。它需要指定每條指令的語義,并與所有執(zhí)行模式交叉。這通常根本不可能實(shí)現(xiàn)。 CPU 的形式驗(yàn)證被分成更小的部分,但是仍然無法驗(yàn)證所有部分是否正確執(zhí)行了 ISA。


使用建議的方法意味著能夠立即驗(yàn)證完整的 L31 內(nèi)核,而無需編寫任何復(fù)雜的斷言。如上所述,黃金模型和檢查斷言是自動(dòng)生成的。


這種方法同時(shí)具有高度可配置性和自動(dòng)化性,特別是對(duì)于 RISC-V CPU,例如 L31:


  • 用戶可以指定設(shè)計(jì)執(zhí)行的頂層 RISC-V 參數(shù)和擴(kuò)展。

  • 該工具能夠自動(dòng)從設(shè)計(jì)中提取數(shù)據(jù),例如將架構(gòu)寄存器與實(shí)際每秒浮點(diǎn)運(yùn)算次數(shù)相關(guān)聯(lián)。

  • 該工具允許添加自定義,例如用來驗(yàn)證的新指令(具有為用戶“擴(kuò)展”黃金模型的能力)。

最后,黃金模型不是由Codasip開發(fā)的(除了一些自定義部分),這一事實(shí)提供了額外的保證,這從驗(yàn)證獨(dú)立性的角度來看很重要。


本文摘錄于《基于形式的高效 RISC-V 處理器驗(yàn)證方法 – 形式化驗(yàn)證》白皮書,出版人為總部位于歐洲的全球領(lǐng)先RISC-V供應(yīng)商和處理器解決方案領(lǐng)導(dǎo)者,該公司的處理器IP目前已部署在數(shù)十億顆芯片中。Codasip通過開放的RISC-V ISA、Codasip Studio處理器設(shè)計(jì)自動(dòng)化工具與高品質(zhì)的處理器IP相結(jié)合,為客戶提供定制計(jì)算。這種創(chuàng)新方法能夠輕松實(shí)現(xiàn)定制和差異化設(shè)計(jì),從而開發(fā)出高性能的、改變游戲規(guī)則的產(chǎn)品,實(shí)現(xiàn)真正意義上的轉(zhuǎn)型。如希望得到該白皮書的完整版本,可瀏覽Codasip中文網(wǎng)站或者關(guān)注該公司微信公眾號(hào)。


該技術(shù)白皮書英文版下載鏈接:https://codasip.com/papers/a-formal-based-approach-for-efficient-riscv-processor-verification


免責(zé)聲明:本文為轉(zhuǎn)載文章,轉(zhuǎn)載此文目的在于傳遞更多信息,版權(quán)歸原作者所有。本文所用視頻、圖片、文字如涉及作品版權(quán)問題,請(qǐng)聯(lián)系小編進(jìn)行處理。


推薦閱讀:

TI 利用兩種控制方案降低 BLDC 電機(jī)驅(qū)動(dòng)器的噪音

高速數(shù)字接口測(cè)試,讓容限測(cè)試更高效

智者避危于無形,如何讓您的電子系統(tǒng)實(shí)現(xiàn)可靠的安全認(rèn)證?

模擬量輸入測(cè)量值顯示滿量程(上溢)的故障處理方法

三極管用飽和Rce,而MOSFET用飽和Vds?

特別推薦
技術(shù)文章更多>>
技術(shù)白皮書下載更多>>
熱門搜索
?

關(guān)閉

?

關(guān)閉