?

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

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

基于VC Formal的QED驗證

快速錯誤檢測（QED）

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

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

形式化方法與QED相結合的實例分享

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

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

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

2023新思科技-英特爾Formal數獨挑戰火熱進行中

8月25日至9月7日報名挑戰

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

創建一個能夠解決數獨難題的設計/測試平臺

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

并提交您創建的平臺或答案

本次挑戰的優勝者將于11月10日公布

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

?

? ? ? ? ?