驗(yàn)證過程中,如只考慮基本的ISA以及潛在的自定義擴(kuò)展,該如何為RISC-V內(nèi)核建立通用的設(shè)置,又該如何定義相關(guān)的SVA斷言?這些SVA斷言僅涉及流水線的開始和結(jié)束,而不包括內(nèi)部細(xì)節(jié)或全流程的所有時(shí)鐘周期。如果目標(biāo)是檢測單指令錯(cuò)誤和多指令錯(cuò)誤。單指令錯(cuò)誤的發(fā)現(xiàn)相對容易,而多指令錯(cuò)誤更難識(shí)別,因?yàn)闀?huì)遇到CPU停頓事件,這些事件可以避免發(fā)生寄存器讀寫沖突。
單指令錯(cuò)誤(例如ADD指令是否真的執(zhí)行了加法功能)與上下文無關(guān),因此可以通過在其它空流水線中運(yùn)行該指令來進(jìn)行檢查。但多指令錯(cuò)誤卻與上下文存在相關(guān)性。該如何對所有合法的上下文進(jìn)行驗(yàn)證?首先需要對QED有一些了解。
基于VC Formal的QED驗(yàn)證
快速錯(cuò)誤檢測(QED)
快速錯(cuò)誤檢測(QED)最早是為了硅后驗(yàn)證而發(fā)明的一種方法。在QED方法中,在機(jī)器代碼基礎(chǔ)上,通過一組并行的寄存器/memory位置定期重復(fù)讀寫指令。然后,比較原始值和復(fù)制值;如果二者不同就表示存在錯(cuò)誤。這類方法正逐漸運(yùn)用到前端驗(yàn)證,究其原因,是為了定期比較并行實(shí)現(xiàn)一致性,在被一些更具功能意義的斷言標(biāo)記之前,就早早捕捉到根本原因錯(cuò)誤。這種方法并不局限于形式化驗(yàn)證,在動(dòng)態(tài)驗(yàn)證中也很有用。
最近的一次網(wǎng)絡(luò)研討會(huì)重點(diǎn)介紹了形式化方法與快速錯(cuò)誤檢測(QED)的搭配使用。它賦予了開發(fā)者更多處理問題的思路。SyoSil的驗(yàn)證工程師Frederik M?llerstr?m Lauridsen分享了他將這種方法用于新思科技VC Formal,從而對RISC-V內(nèi)核進(jìn)行驗(yàn)證的做法。
形式化方法與QED相結(jié)合的實(shí)例分享
為了使用QED方法,需要參考設(shè)計(jì)和被測設(shè)計(jì)(DUT)。這里的參考設(shè)計(jì)指的是單指令流水線測試,例如通過其它空流水線推送ADD指令。與此同時(shí),DUT將推送相同的指令。但如何將上下文定義為任意選擇的前后指令呢?為此,F(xiàn)rederick用到了QED的另一個(gè)版本,稱為C-S2QED。
無需過多深入技術(shù)細(xì)節(jié),S2表示“符號狀態(tài)”,它允許任意指令通過流水線,只要進(jìn)入流水線的第一條指令與進(jìn)入?yún)⒖剂魉€的指令相同即可。其中“符號”部分是關(guān)鍵。沒有必要定義其它指令的推送過程,只要是合法的指令就行。由于使用的是形式化方法,因此驗(yàn)證過程中要考慮到所有可能性。Frederick用到的另一個(gè)巧思是首先證明所有指令可在一定的最大周期數(shù)內(nèi)通過流水線,從而為有界證明提供了限制條件。
使用QED方法并利用形式化方法對參考設(shè)計(jì)和DUT進(jìn)行比較,證明了流水線實(shí)現(xiàn)結(jié)果中不存在多指令錯(cuò)誤,否則VC Formal會(huì)提供反例。Frederick表示,他們還沒有將這種方法用到任何標(biāo)準(zhǔn)的RISC-V ISA擴(kuò)展(M、A、F等)中。但事實(shí)上,開發(fā)者也可以使用VC Formal DPV來處理M擴(kuò)展及其它擴(kuò)展。
2023新思科技-英特爾Formal數(shù)獨(dú)挑戰(zhàn)火熱進(jìn)行中
8月25日至9月7日報(bào)名挑戰(zhàn)
通過新思科技VC Formal FPV或者DPV
創(chuàng)建一個(gè)能夠解決數(shù)獨(dú)難題的設(shè)計(jì)/測試平臺(tái)
請于9月30日前解開所有謎題
并提交您創(chuàng)建的平臺(tái)或答案
本次挑戰(zhàn)的優(yōu)勝者將于11月10日公布
掃描下方二維碼,即可報(bào)名
?
? ? ? ? ?
原文標(biāo)題:文末有驚喜挑戰(zhàn) | 基于VC Formal,在RISC-V內(nèi)核上,驗(yàn)證一波!
文章出處:【微信公眾號:新思科技】歡迎添加關(guān)注!文章轉(zhuǎn)載請注明出處。
-
新思科技
+關(guān)注
關(guān)注
5文章
778瀏覽量
50273
原文標(biāo)題:文末有驚喜挑戰(zhàn) | 基于VC Formal,在RISC-V內(nèi)核上,驗(yàn)證一波!
文章出處:【微信號:Synopsys_CN,微信公眾號:新思科技】歡迎添加關(guān)注!文章轉(zhuǎn)載請注明出處。
發(fā)布評論請先 登錄
相關(guān)推薦
評論