文末有驚喜挑戰(zhàn) | 基于VC Formal，在RISC-V內(nèi)核上，驗(yàn)證一波！

?

驗(yàn)證過程中，如只考慮基本的ISA以及潛在的自定義擴(kuò)展，該如何為RISC-V內(nèi)核建立通用的設(shè)置，又該如何定義相關(guān)的SVA斷言？這些SVA斷言僅涉及流水線的開始和結(jié)束，而不包括內(nèi)部細(xì)節(jié)或全流程的所有時(shí)鐘周期。如果目標(biāo)是檢測(cè)單指令錯(cuò)誤和多指令錯(cuò)誤。單指令錯(cuò)誤的發(fā)現(xiàn)相對(duì)容易，而多指令錯(cuò)誤更難識(shí)別，因?yàn)闀?huì)遇到CPU停頓事件，這些事件可以避免發(fā)生寄存器讀寫沖突。

單指令錯(cuò)誤（例如ADD指令是否真的執(zhí)行了加法功能）與上下文無關(guān)，因此可以通過在其它空流水線中運(yùn)行該指令來進(jìn)行檢查。但多指令錯(cuò)誤卻與上下文存在相關(guān)性。該如何對(duì)所有合法的上下文進(jìn)行驗(yàn)證？首先需要對(duì)QED有一些了解。

基于VC Formal的QED驗(yàn)證

快速錯(cuò)誤檢測(cè)（QED）

快速錯(cuò)誤檢測(cè)（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ò)誤檢測(cè)（QED）的搭配使用。它賦予了開發(fā)者更多處理問題的思路。SyoSil的驗(yàn)證工程師Frederik M?llerstr?m Lauridsen分享了他將這種方法用于新思科技VC Formal，從而對(duì)RISC-V內(nèi)核進(jìn)行驗(yàn)證的做法。

形式化方法與QED相結(jié)合的實(shí)例分享

為了使用QED方法，需要參考設(shè)計(jì)和被測(cè)設(shè)計(jì)（DUT）。這里的參考設(shè)計(jì)指的是單指令流水線測(cè)試，例如通過其它空流水線推送ADD指令。與此同時(shí)，DUT將推送相同的指令。但如何將上下文定義為任意選擇的前后指令呢？為此，F(xiàn)rederick用到了QED的另一個(gè)版本，稱為C-S2QED。

無需過多深入技術(shù)細(xì)節(jié)，S2表示“符號(hào)狀態(tài)”，它允許任意指令通過流水線，只要進(jìn)入流水線的第一條指令與進(jìn)入?yún)⒖剂魉€的指令相同即可。其中“符號(hào)”部分是關(guān)鍵。沒有必要定義其它指令的推送過程，只要是合法的指令就行。由于使用的是形式化方法，因此驗(yàn)證過程中要考慮到所有可能性。Frederick用到的另一個(gè)巧思是首先證明所有指令可在一定的最大周期數(shù)內(nèi)通過流水線，從而為有界證明提供了限制條件。

使用QED方法并利用形式化方法對(duì)參考設(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日?qǐng)?bào)名挑戰(zhàn)

通過新思科技VC Formal FPV或者DPV

創(chuàng)建一個(gè)能夠解決數(shù)獨(dú)難題的設(shè)計(jì)/測(cè)試平臺(tái)

請(qǐng)于9月30日前解開所有謎題

并提交您創(chuàng)建的平臺(tái)或答案

本次挑戰(zhàn)的優(yōu)勝者將于11月10日公布

掃描下方二維碼，即可報(bào)名

?

? ? ? ? ?