盡管由于開源架構設計新的微處理器在經濟上是可行的，但測試和驗證仍然是主要障礙。

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

驗證挑戰

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

那么，我們如何期望未來的芯片設計能夠抵御這些使芯片容易受到黑客攻擊的惡意漏洞？我們如何知道該芯片將繼續按預期在航空航天和國防領域工作，并且不會由于測試和驗證期間未發現的有意和無意的錯誤而出現異常？

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

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

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

?

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

?

?

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

方法論

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

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

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

在某些情況下，在開發過程中，我們還發現了我們在測試開發階段引入的錯誤。其中大部分是由于我們對 RISC-V ISA 的理解有誤。值得慶幸的是，根據設計師的反饋，我們能夠將其與 ISA 的要求保持一致。單擊此處了解有關性能的更多詳細信息、我們發現了哪些錯誤、我們能夠獲得多少證明、需要哪些運行時以及我們如何簽署驗證以完成。

總結

我們的目標是進行端到端的形式驗證，但存在以下限制：

（a）我們的工作是在訪問受限的設計師之外進行的，

（b）我們沒有設計微架構的先驗知識，

（ c) 我們沒有描述接口和內部狀態機的全面、詳細的規范。

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

據我們所知，這是第一個獨立于特定形式驗證工具供應商的形式驗證解決方案，它使用所有工具都支持的 SVA 開放標準，并且需要最少的設置，保證大于 99% 的證明收斂.

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

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