如何利用形式化驗(yàn)證提高RISC-V處理器質(zhì)量？

在設(shè)計(jì)開發(fā)RISC-V處理器的過(guò)程中，通常遇到很多問(wèn)題。以一個(gè)中等復(fù)雜程度的處理器為例，可以輕易浮現(xiàn)成百上千的錯(cuò)誤漏洞。當(dāng)在引入更多的高級(jí)功能時(shí)，漏洞也會(huì)不經(jīng)意地被帶入，這些漏洞復(fù)雜性各不相同。某些類型的漏洞太過(guò)于復(fù)雜，以致仿真無(wú)法發(fā)現(xiàn)它們，因此必須增強(qiáng)RTL驗(yàn)證方式方法。而增加形式驗(yàn)證是正解之一。從隱藏的案例到隱藏式漏洞，形式驗(yàn)證允許在合理的處理時(shí)間內(nèi)詳盡地探索狀態(tài)。那么如何利用形式化驗(yàn)證來(lái)提高RISC-V處理器的質(zhì)量？

為什么針對(duì)RISC-V使用形式化驗(yàn)證？

RISC-V是一個(gè)模塊化的指令集架構(gòu)，可以為其開發(fā)一個(gè)架構(gòu)測(cè)試套件。它被用于基于仿真的驗(yàn)證，以驗(yàn)證一個(gè)處理器的實(shí)現(xiàn)。同樣地，形式化方法可以用來(lái)驗(yàn)證處理器的架構(gòu)符合性。為什么？因?yàn)镽ISC-V是一個(gè)開放的標(biāo)準(zhǔn)，每個(gè)人都可以把它作為一個(gè)參考模型來(lái)正式驗(yàn)證一個(gè)實(shí)現(xiàn)。

了解何時(shí)以及如何使用形式驗(yàn)證？

對(duì)于所有的硬件設(shè)計(jì)來(lái)說(shuō)，形式化驗(yàn)證有好有壞，也有應(yīng)用的好時(shí)機(jī)和壞時(shí)機(jī)。RISC-V處理器也不例外。

在項(xiàng)目開發(fā)的早期，有時(shí)甚至在仿真測(cè)試平臺(tái)準(zhǔn)備好之前，使用形式化是一個(gè)很好的方法，可以沖掉明顯的錯(cuò)誤漏洞。它可以確保以后執(zhí)行的仿真步驟不會(huì)被這些bug所阻擋。另一方面，形式化驗(yàn)證在項(xiàng)目后期是非常有價(jià)值的，可以發(fā)現(xiàn)所有其他驗(yàn)證方法所遺漏的不易發(fā)現(xiàn)的錯(cuò)誤。

形式化驗(yàn)證的不同變體的考慮主要有：?

基于斷言的驗(yàn)證（ABV）- 使用低級(jí)斷言。

使用高級(jí)斷言的端到端驗(yàn)證，通常需要一個(gè)抽象的設(shè)計(jì)模型。

基于自動(dòng)生成的斷言的形式化流程也非常有用，如驗(yàn)證時(shí)鐘門控的順序等價(jià)檢查，或X-傳播驗(yàn)證。

當(dāng)然更高級(jí)的驗(yàn)證技術(shù)也是適用的，這取決于模塊的特性。例如，安全和功能安全應(yīng)用。

除了這些，RISC-V處理器還可以用RISC-V ISA的架構(gòu)模型進(jìn)行端到端的驗(yàn)證。不過(guò)，應(yīng)用這樣的技術(shù)不能太早，因?yàn)榇蠖鄶?shù)模塊必須準(zhǔn)備好并相互連接：指令獲取、解碼器、執(zhí)行單元、加載-存儲(chǔ)接口?？赡懿淮嬖诘哪K或者因?yàn)椴粔虺墒於缓谙浠哪K，y也可能包括內(nèi)存管理單元（MMU）和緩沖器d等。

形式驗(yàn)證是瑞士奶酪模型驗(yàn)證方法的一個(gè)重要 "切片”。

Codasip的處理器驗(yàn)證方法依靠的是瑞士奶酪模型。通過(guò)這種方法，一些冗余是可以接受的，甚至是有針對(duì)性的。

冗余的重要性！

應(yīng)用端到端的形式化方法，在內(nèi)核上運(yùn)行的仿真測(cè)試平臺(tái)似乎是多余的。事實(shí)上它確實(shí)有些是多余，但在有些情況下，由于缺少檢查器或輸入約束太強(qiáng)，一種方法可能會(huì)錯(cuò)過(guò)一個(gè)漏洞（例如如果它不在中斷或調(diào)試命令的背景下進(jìn)行驗(yàn)證）。還有一種方法s是即使適當(dāng)?shù)臋z查器和輸入生成器已經(jīng)到位，也可能無(wú)法擊中一個(gè)漏洞。對(duì)于仿真來(lái)說(shuō)，這可能是由于缺乏測(cè)試的緣故。

瞄準(zhǔn)隱藏案例！

形式驗(yàn)證可以發(fā)現(xiàn)大多數(shù)類型的漏洞，前提是正確的斷言已經(jīng)到位，輸入約束不是太強(qiáng)，并且使用適當(dāng)?shù)募夹g(shù)來(lái)處理狀態(tài)爆炸（例如抽象）。此外形式化驗(yàn)證在尋找隱藏案例方面也很出色，因?yàn)榕c仿真不同，它將隱藏案例與基本案例同等看待。由于精確時(shí)序條件而出現(xiàn)的錯(cuò)誤l漏洞，用形式化驗(yàn)證通常比用仿真y驗(yàn)證更容易發(fā)現(xiàn)。

仿真驗(yàn)證和形式驗(yàn)證的好與壞？

形式驗(yàn)證在提供 "錯(cuò)誤的故障 "時(shí)，會(huì)受到不良形象的影響。這是因?yàn)樗?"無(wú)限減 "的基礎(chǔ)上工作。事實(shí)上，在默認(rèn)情況下它將達(dá)到無(wú)限狀態(tài)。有些狀態(tài)是不現(xiàn)實(shí)的，會(huì)通過(guò)添加"（減）"的約束條件而被拋棄。如果這些約束不夠嚴(yán)格，漏洞出現(xiàn)。如果它們的限制性太強(qiáng)，就會(huì)隱藏漏洞。但有一些方法可以確保不會(huì)出現(xiàn)這種情況。

另一方面，模擬是在 "零加 "的基礎(chǔ)上工作的。除了測(cè)試平臺(tái)允許的行為，沒(méi)有（"零"）行為會(huì)發(fā)生（"加"）。仿真也會(huì)出現(xiàn) "錯(cuò)誤的失敗"（如果測(cè)試平臺(tái)允許錯(cuò)誤的輸入序列）。隱藏bug的問(wèn)題也出現(xiàn)在仿真中，而且更加重要。如果測(cè)試平臺(tái)不允許特定的有效輸入序列，那么一個(gè)漏洞可能會(huì)被忽略。

應(yīng)用于Codasip RISC-V內(nèi)核的形式驗(yàn)證

在嵌入式內(nèi)核上使用形式驗(yàn)證技術(shù)已被證明是成功和有效的。

編輯：黃飛

?