8月24日，國微芯受邀參與了備受矚目的2023 RISC-V中國峰會。本屆峰會以“RISC-V生態(tài)共建”為主題,結合當下全球新形勢,把握全球新時機,呈現RISC-V全球新觀點、新趨勢。國微芯銷售總監(jiān)鄧金斌在此次盛會中發(fā)表了主題為《基于形式化的高效RISC-V處理器驗證方法》的演講，探討形式化驗證技術，視野開闊、引人深思。

此次演講，鄧金斌先生通過產品介紹和深入的案例分析展示了 “芯天成”形式化驗證工具在RISC-V處理器設計領域突出的應用優(yōu)勢。

全功能形式化驗證平臺

“芯天成”形式化驗證平臺EsseFormal包括C to RTL to Netlist的等價性驗證工具、屬性驗證工具，以及各種實用驗證Apps。這些工具通過數學和邏輯推理及形式化規(guī)范語言，能夠幫助芯片開發(fā)人員識別和解決系統(tǒng)中潛在的錯誤、漏洞和安全隱患，在數字芯片設計的各個環(huán)節(jié)發(fā)揮重要作用。

（EsseFormal平臺工具概述）

香山RISC-V處理器驗證

香山處理器項目由中科院計算所于2019年發(fā)起，經歷兩代微架構迭代，第三代昆明湖架構由北京開源芯片研究院牽頭聯(lián)合開發(fā)研制。香山處理器是基于RISC-V指令集架構的自研處理器，相對于一般處理器，其設計更加復雜，包含更多的指令、寄存器、內存等組件，非常容易出現驗證盲點。

鄧金斌先生指出，形式化工具在驗證RISC-V處理器時，不僅要關注功能正確性和時序正確性，還需要考慮特殊的指令和功能、多個開源實現和變體的差異等等。因此，形式驗證工具需要具備靈活和全面的驗證能力，以及深入理解RISC-V指令集架構和處理器設計特點，才能滿足這些額外的驗證需求。

在香山南湖V2版本處理器的驗證案例中，EsseFormal平臺的等價性驗證工具EsseFECT成功驗證了基于RISC-V的整形模塊和浮點模塊中各類算子的C-RTL功能一致性。

EsseFECT不僅驗證了整形模塊中加減、乘除、邏輯操作等基本算子的準確性，還涵蓋了浮點模塊中加減、乘除、開方等更加復雜的操作。這些驗證不僅僅是為了確認各個算子的功能正確性，更是為了驗證整個處理器在執(zhí)行復雜算術操作時的穩(wěn)健性和一致性。此外，EsseFECT還驗證了整形和浮點數之間的轉換及比較操作，確保了不同數據類型之間的無誤轉換和可靠比較，從而增強了處理器在不同數據處理場景下的可靠性。

助力RISC-V生態(tài)發(fā)展

RISC-V作為一種開源指令集架構，正在迅速發(fā)展并得到廣泛應用。然而，由于其復雜的指令集和靈活的定制化需求，驗證RISC-V處理器的挑戰(zhàn)也越來越大。國微芯不僅擁有自主研發(fā)的EsseFormal工具，還積極參與RISC-V生態(tài)系統(tǒng)的建設和推動。通過與生態(tài)伙伴的緊密合作，國微芯致力于推動RISC-V處理器的發(fā)展，加速國內開源處理器產業(yè)的壯大和創(chuàng)新。