(資料圖)

作者：Laurent Arditi, Paul Sargent, Thomas Aird
職務：Codasip高級驗證/形式驗證工程師

RISC-V的開放性允許定制和擴展基于 RISC-V 內核的架構和微架構，以滿足特定需求。這種對設計自由的渴望也正在將驗證部分的職責轉移到不斷壯大的開發人員社群。然而，隨著越來越多的企業和開發人員轉型RISC-V，大家才發現處理器驗證絕非易事。新標準由于其新穎和靈活性而帶來的新功能會在無意中產生規范和設計漏洞，因此處理器驗證是處理器開發過程中一項非常重要的環節。

在復雜性一般的RISC-V 處理器內核的開發過程中，會發現數百甚至數千個漏洞。當引入更多高級特性的時候，也會引入復雜程度各不相同的新漏洞。而某些類型的漏洞過于復雜，導致在仿真環節都無法找到它們。因此必須通過添加形式驗證來賦能 RTL 驗證方法。從極端漏洞到隱匿式漏洞，形式驗證能夠讓您在合理的處理時間內詳盡地探索所有狀態。

在本文中，我們將介紹一個基于形式驗證的、易于調動的 RISC-V 處理器驗證程序。與 RISC-V ISA 黃金模型和 RISC-V 合規性自動生成的檢查一起，展示了如何有效地定位那些無法進行仿真的漏洞。通過為每條指令提供一組專用的斷言模板來實現高度自動化，不再需要手動設計，從而提高了形式驗證團隊的工作效率。

1、基于先進內核的處理器開發

嵌入式系統的應用越來越廣泛，同時對處理器的性能、功耗和面積（PPA）要求越來越高，因此我們將這樣的產業和技術背景下用實際案例來分析處理器的驗證。Codasip L31 是一款用于微控制器應用的 32 位中端嵌入式 RISC-V 處理器內核。作為一款多功能、低功耗、通用型的 CPU，它實現了性能和功耗的理想平衡。從物聯網設備到工業和汽車控制，或作為大型系統中的深度嵌入式內核，L31可在一個非常小巧緊湊的硅片面積中實現本地處理能力。L31是通過 Codasip Studio 使用 CodAL 語言設計而成，該內核完全可定制，包括經典的擴展和特性，以及實現這些擴展和特性所需的高效和徹底的驗證。

image001.png

表 1 Codasip L31內核展示了RISC-V處理器的優異特性

<rt id="yc22u"></rt>