?

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

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

基于VC Formal的QED驗證

快速錯誤檢測（QED）

快速錯誤檢測（QED）最早是為了硅后驗證而發(fā)明的一種方法。在QED方法中，在機器代碼基礎(chǔ)上，通過一組并行的寄存器/memory位置定期重復(fù)讀寫指令。然后，比較原始值和復(fù)制值；如果二者不同就表示存在錯誤。這類方法正逐漸運用到前端驗證，究其原因，是為了定期比較并行實現(xiàn)一致性，在被一些更具功能意義的斷言標記之前，就早早捕捉到根本原因錯誤。這種方法并不局限于形式化驗證，在動態(tài)驗證中也很有用。

最近的一次網(wǎng)絡(luò)研討會重點介紹了形式化方法與快速錯誤檢測（QED）的搭配使用。它賦予了開發(fā)者更多處理問題的思路。SyoSil的驗證工程師Frederik M?llerstr?m Lauridsen分享了他將這種方法用于新思科技VC Formal，從而對RISC-V內(nèi)核進行驗證的做法。

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

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

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

使用QED方法并利用形式化方法對參考設(shè)計和DUT進行比較，證明了流水線實現(xiàn)結(jié)果中不存在多指令錯誤，否則VC Formal會提供反例。Frederick表示，他們還沒有將這種方法用到任何標準的RISC-V ISA擴展（M、A、F等）中。但事實上，開發(fā)者也可以使用VC Formal DPV來處理M擴展及其它擴展。

2023新思科技-英特爾Formal數(shù)獨挑戰(zhàn)火熱進行中

8月25日至9月7日報名挑戰(zhàn)

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

創(chuàng)建一個能夠解決數(shù)獨難題的設(shè)計/測試平臺

請于9月30日前解開所有謎題

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

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

掃描下方二維碼，即可報名

?

? ? ? ? ?