盡管由于開源架構(gòu)設(shè)計新的微處理器在經(jīng)濟(jì)上是可行的，但測試和驗證仍然是主要障礙。

隨著 RISC-V 等開源處理器架構(gòu)的出現(xiàn)，芯片設(shè)計變得越來越大眾化，越來越多的組織敢于涉足處理器設(shè)計，從嵌入式微控制器到高端臺式機(jī)和服務(wù)器級 CPU，包括人工智能(AI) 和機(jī)器學(xué)習(xí) (ML) 設(shè)計。

驗證挑戰(zhàn)

盡管由于開源架構(gòu)設(shè)計新的微處理器在經(jīng)濟(jì)上是可行的，但開發(fā)周期的測試和驗證部分仍然是主要障礙，一些人估計這些活動占芯片總成本的 70% 左右發(fā)展。此外，當(dāng)發(fā)現(xiàn)芯片存在制造前未發(fā)現(xiàn)的功能缺陷（錯誤）時，這不考慮遺漏錯誤和重新設(shè)計的成本。人們必須只關(guān)注 Spectre 和 Meltdown 等安全漏洞的后果，這些漏洞幾乎影響了地球上的所有處理器，無論供應(yīng)商是誰，包括 Arm、英特爾和 AMD 等大牌。

那么，我們?nèi)绾纹谕磥淼男酒O(shè)計能夠抵御這些使芯片容易受到黑客攻擊的惡意漏洞？我們?nèi)绾沃涝撔酒瑢⒗^續(xù)按預(yù)期在航空航天和國防領(lǐng)域工作，并且不會由于測試和驗證期間未發(fā)現(xiàn)的有意和無意的錯誤而出現(xiàn)異常？

答案在于查看形式驗證，這是唯一可以提供錯誤不存在“證明”并提供設(shè)計和規(guī)范中錯誤的可證明證據(jù)的驗證技術(shù)。

公理化 RISC-V 處理器的正確性

在Axiomise，我們使用行業(yè)標(biāo)準(zhǔn)、非專有 SystemVerilog 斷言 (SVA) 開發(fā)了一個新的形式證明工具包，用于基于已發(fā)布的 RISC-V ISA 建立 ISA 合規(guī)性，我們已經(jīng)使用了這個確定給定的處理器實現(xiàn)是否符合 ISA 語義。

?

Axiomise RISC-V 正式證明套件（來源：Axiomise.com）

?

?

我們的解決方案完全與形式工具供應(yīng)商無關(guān)，不需要修改設(shè)計，并且只需要最終用戶熟悉 Verilog/VHDL。此外，我們的方法可重復(fù)用于其他 RISC-V 處理器。我們的“公理化”方法是使用 SystemVerilog 斷言的開放標(biāo)準(zhǔn)構(gòu)建的，并通過我們的抽象和問題減少工具包增強(qiáng)了性能。我們在實踐中部署了我們的方法，以確保我們可以確定處理器的所有功能/安全/安全/電源要求都轉(zhuǎn)化為設(shè)計實現(xiàn)的可證明有效的公理（屬性）。

方法論

檢查的一般策略依賴于使用觀察模型觀察從發(fā)出點到完成點的所有指令的路徑，其中非確定性允許其他指令交錯穿插在特定指令的發(fā)出和完成之間被檢查。這確保了我們可以捕獲各種受控制和并發(fā)控制并可能導(dǎo)致錯誤結(jié)果發(fā)生的錯誤。

重要的是要強(qiáng)調(diào)，必須對每條具有不確定性的指令進(jìn)行端到端檢查，因為在實踐中，由于測試的非常直接的性質(zhì)，大多數(shù)錯誤都被遺漏了，這些測試專門探索了從問題到完成的定向路徑，但不一定允許其他指令干擾。

對于大多數(shù)說明，我們通常會圍繞觀察因果關(guān)系編寫一項檢查。對 LOADS 和 STORES 的檢查是使用內(nèi)存的完整接口構(gòu)建的，通過該接口我們檢查 LOADS 和 STORES 的所有變體 - BYTE、WORD、HALF-WORD、對齊和未對齊。這使我們能夠檢查不同風(fēng)格的 LOADS 和 STORES 之間所有可能的依賴關(guān)系，尤其是當(dāng)一個序列具有指向同一地址的這些依賴關(guān)系時。

在某些情況下，在開發(fā)過程中，我們還發(fā)現(xiàn)了我們在測試開發(fā)階段引入的錯誤。其中大部分是由于我們對 RISC-V ISA 的理解有誤。值得慶幸的是，根據(jù)設(shè)計師的反饋，我們能夠?qū)⑵渑c ISA 的要求保持一致。單擊此處了解有關(guān)性能的更多詳細(xì)信息、我們發(fā)現(xiàn)了哪些錯誤、我們能夠獲得多少證明、需要哪些運(yùn)行時以及我們?nèi)绾魏炇痱炞C以完成。

總結(jié)

我們的目標(biāo)是進(jìn)行端到端的形式驗證，但存在以下限制：

（a）我們的工作是在訪問受限的設(shè)計師之外進(jìn)行的，

（b）我們沒有設(shè)計微架構(gòu)的先驗知識，

（ c) 我們沒有描述接口和內(nèi)部狀態(tài)機(jī)的全面、詳細(xì)的規(guī)范。

在許多方面，我們的工作代表了現(xiàn)代設(shè)計驗證的現(xiàn)實，其中忙碌的設(shè)計師通常不會記錄詳細(xì)的微架構(gòu)規(guī)范，初始驗證通常由設(shè)計師自己使用模擬在本地進(jìn)行，或者關(guān)于規(guī)范的知識是口口相傳給獨立驗證設(shè)計的驗證工程師。

據(jù)我們所知，這是第一個獨立于特定形式驗證工具供應(yīng)商的形式驗證解決方案，它使用所有工具都支持的 SVA 開放標(biāo)準(zhǔn)，并且需要最少的設(shè)置，保證大于 99% 的證明收斂.

您可以立即使用我們的證明工具包，并使用您選擇的形式驗證工具開始在您的 RISC-V 設(shè)計中查找錯誤并構(gòu)建錯誤不存在的證明。

請單擊此處了解我們的解決方案與其他解決方案有何不同以及我們在微處理器驗證三個十年的歷史。