《電子技術(shù)應(yīng)用》
您所在的位置:首頁 > 嵌入式技術(shù) > 解決方案 > 基于形式驗證的高效 RISC-V 處理器驗證方法

基于形式驗證的高效 RISC-V 處理器驗證方法

2023-06-01
作者:Laurent Arditi, Paul Sargent, Thomas Aird Codasip高級驗證/形式驗證工程師
來源:Codasip
關(guān)鍵詞: CODASIP RISC-V 處理器驗證

  RISC-V的開放性允許定制和擴(kuò)展基于 RISC-V 內(nèi)核的架構(gòu)和微架構(gòu),,以滿足特定需求,。這種對設(shè)計自由的渴望也正在將驗證部分的職責(zé)轉(zhuǎn)移到不斷壯大的開發(fā)人員社群。然而,,隨著越來越多的企業(yè)和開發(fā)人員轉(zhuǎn)型RISC-V,,大家才發(fā)現(xiàn)處理器驗證絕非易事,。新標(biāo)準(zhǔn)由于其新穎和靈活性而帶來的新功能會在無意中產(chǎn)生規(guī)范和設(shè)計漏洞,因此處理器驗證是處理器開發(fā)過程中一項非常重要的環(huán)節(jié),。

  在復(fù)雜性一般的RISC-V 處理器內(nèi)核的開發(fā)過程中,,會發(fā)現(xiàn)數(shù)百甚至數(shù)千個漏洞。當(dāng)引入更多高級特性的時候,,也會引入復(fù)雜程度各不相同的新漏洞,。而某些類型的漏洞過于復(fù)雜,導(dǎo)致在仿真環(huán)節(jié)都無法找到它們。因此必須通過添加形式驗證來賦能 RTL 驗證方法,。從極端漏洞到隱匿式漏洞,,形式驗證能夠讓您在合理的處理時間內(nèi)詳盡地探索所有狀態(tài)。

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

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

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

28.JPG

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

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

25.JPG

26.JPG

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

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

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

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

  ●驗證是在處理器開發(fā)期間與設(shè)計團(tuán)隊合作完成的,。

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

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

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

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

  仿真實際上不可或缺,,它允許我們在兩個級別上進(jìn)行驗證設(shè)計:

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

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

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

  2.2形式驗證的優(yōu)勢和目的

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

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

  形式驗證用于以下情況:

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

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

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

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

  ●對漏洞進(jìn)行分類和識別,,以便通過形式驗證來學(xué)習(xí)和改進(jìn)測試平臺/仿真。

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

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

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

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

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

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

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

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

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

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

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

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

27.JPG

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

  這種端到端的驗證方法可以在比整個CPU 更小,、更簡單的模塊(例如數(shù)據(jù)緩存)上合理實現(xiàn),。可以在緩存上寫入端到端斷言,,以驗證寫入特定地址的數(shù)據(jù)是否從同一地址正確讀取,。這使用了眾所周知的形式驗證技術(shù),例如記分牌算法,。

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

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

  這種方法同時具有高度可配置性和自動化性,,特別是對于 RISC-V CPU,例如 L31:

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

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

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

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

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



更多精彩內(nèi)容歡迎點(diǎn)擊==>>電子技術(shù)應(yīng)用-AET<<

mmexport1621241704608.jpg

本站內(nèi)容除特別聲明的原創(chuàng)文章之外,,轉(zhuǎn)載內(nèi)容只為傳遞更多信息,,并不代表本網(wǎng)站贊同其觀點(diǎn)。轉(zhuǎn)載的所有的文章,、圖片,、音/視頻文件等資料的版權(quán)歸版權(quán)所有權(quán)人所有。本站采用的非本站原創(chuàng)文章及圖片等內(nèi)容無法一一聯(lián)系確認(rèn)版權(quán)者,。如涉及作品內(nèi)容,、版權(quán)和其它問題,請及時通過電子郵件或電話通知我們,,以便迅速采取適當(dāng)措施,,避免給雙方造成不必要的經(jīng)濟(jì)損失。聯(lián)系電話:010-82306118,;郵箱:[email protected],。