行業(yè)峰會(huì)｜國(guó)微芯引領(lǐng)高效RISC-V處理器驗(yàn)證新浪潮
8月24日，國(guó)微芯受邀參與了備受矚目的2023 RISC-V中國(guó)峰會(huì)。本屆峰會(huì)以“RISC-V生態(tài)共建”為主題,結(jié)合當(dāng)下全球新形勢(shì),把握全球新時(shí)機(jī),呈現(xiàn)RISC-V全球新觀點(diǎn)、新趨勢(shì)。國(guó)微芯銷售總監(jiān)鄧金斌在此次盛會(huì)中發(fā)表了主題為《基于形式化的高效RISC-V處理器驗(yàn)證方法》的演講，探討形式化驗(yàn)證技術(shù)，視野開闊、引人深思。
此次演講，鄧金斌先生通過(guò)產(chǎn)品介紹和深入的案例分析展示了 “芯天成”形式化驗(yàn)證工具在RISC-V處理器設(shè)計(jì)領(lǐng)域突出的應(yīng)用優(yōu)勢(shì)。
全功能形式化驗(yàn)證平臺(tái)
“芯天成”形式化驗(yàn)證平臺(tái)EsseFormal包括C to RTL to Netlist的等價(jià)性驗(yàn)證工具、屬性驗(yàn)證工具，以及各種實(shí)用驗(yàn)證Apps。這些工具通過(guò)數(shù)學(xué)和邏輯推理及形式化規(guī)范語(yǔ)言，能夠幫助芯片開發(fā)人員識(shí)別和解決系統(tǒng)中潛在的錯(cuò)誤、漏洞和安全隱患，在數(shù)字芯片設(shè)計(jì)的各個(gè)環(huán)節(jié)發(fā)揮重要作用。
（EsseFormal平臺(tái)工具概述）
香山RISC-V處理器驗(yàn)證
香山處理器項(xiàng)目由中科院計(jì)算所于2019年發(fā)起，經(jīng)歷兩代微架構(gòu)迭代，第三代昆明湖架構(gòu)由北京開源芯片研究院牽頭聯(lián)合開發(fā)研制。香山處理器是基于RISC-V指令集架構(gòu)的自研處理器，相對(duì)于一般處理器，其設(shè)計(jì)更加復(fù)雜，包含更多的指令、寄存器、內(nèi)存等組件，非常容易出現(xiàn)驗(yàn)證盲點(diǎn)。
鄧金斌先生指出，形式化工具在驗(yàn)證RISC-V處理器時(shí)，不僅要關(guān)注功能正確性和時(shí)序正確性，還需要考慮特殊的指令和功能、多個(gè)開源實(shí)現(xiàn)和變體的差異等等。因此，形式驗(yàn)證工具需要具備靈活和全面的驗(yàn)證能力，以及深入理解RISC-V指令集架構(gòu)和處理器設(shè)計(jì)特點(diǎn)，才能滿足這些額外的驗(yàn)證需求。
在香山南湖V2版本處理器的驗(yàn)證案例中，EsseFormal平臺(tái)的等價(jià)性驗(yàn)證工具EsseFECT成功驗(yàn)證了基于RISC-V的整形模塊和浮點(diǎn)模塊中各類算子的C-RTL功能一致性。
EsseFECT不僅驗(yàn)證了整形模塊中加減、乘除、邏輯操作等基本算子的準(zhǔn)確性，還涵蓋了浮點(diǎn)模塊中加減、乘除、開方等更加復(fù)雜的操作。這些驗(yàn)證不僅僅是為了確認(rèn)各個(gè)算子的功能正確性，更是為了驗(yàn)證整個(gè)處理器在執(zhí)行復(fù)雜算術(shù)操作時(shí)的穩(wěn)健性和一致性。此外，EsseFECT還驗(yàn)證了整形和浮點(diǎn)數(shù)之間的轉(zhuǎn)換及比較操作，確保了不同數(shù)據(jù)類型之間的無(wú)誤轉(zhuǎn)換和可靠比較，從而增強(qiáng)了處理器在不同數(shù)據(jù)處理場(chǎng)景下的可靠性。
助力RISC-V生態(tài)發(fā)展
RISC-V作為一種開源指令集架構(gòu)，正在迅速發(fā)展并得到廣泛應(yīng)用。然而，由于其復(fù)雜的指令集和靈活的定制化需求，驗(yàn)證RISC-V處理器的挑戰(zhàn)也越來(lái)越大。國(guó)微芯不僅擁有自主研發(fā)的EsseFormal工具，還積極參與RISC-V生態(tài)系統(tǒng)的建設(shè)和推動(dòng)。通過(guò)與生態(tài)伙伴的緊密合作，國(guó)微芯致力于推動(dòng)RISC-V處理器的發(fā)展，加速國(guó)內(nèi)開源處理器產(chǎn)業(yè)的壯大和創(chuàng)新。
