11月3日，由中國(guó)計(jì)算機(jī)學(xué)會(huì)主辦的年度盛會(huì)CCF DAC圓滿落幕。芯華章研發(fā)副總裁劉軍受邀致主題演講，系統(tǒng)分享了GalaxEC HEC工具從技術(shù)架構(gòu)到RISC-V算子完備驗(yàn)證場(chǎng)景的精準(zhǔn)適配，從核心算法創(chuàng)新到大規(guī)模項(xiàng)目落地的實(shí)踐路徑。

當(dāng)前，RISC-V開(kāi)源架構(gòu)的靈活性推動(dòng)了定制化設(shè)計(jì)的爆發(fā)式增長(zhǎng)，同時(shí)也衍生出規(guī)范寬泛、算子復(fù)雜、全場(chǎng)景仿真驗(yàn)證收斂困難等核心痛點(diǎn)。這些問(wèn)題直接導(dǎo)致RISC-V芯片驗(yàn)證周期失控、流片風(fēng)險(xiǎn)攀升，成為制約行業(yè)發(fā)展的共性難題。

作為芯華章自主研發(fā)的高階等價(jià)性檢查工具，GalaxEC HEC專(zhuān)為AI芯片、DSP及RISC-V定制芯片的數(shù)據(jù)通路驗(yàn)證打造。

針對(duì)RISC-V領(lǐng)域“標(biāo)準(zhǔn)模型缺失、激勵(lì)開(kāi)發(fā)成本高”的突出痛點(diǎn)，芯華章同步推出RV-APP(RISC-V指令級(jí)C++標(biāo)準(zhǔn)模型套件)，以“標(biāo)準(zhǔn)化、自動(dòng)化”特性填補(bǔ)了行業(yè)空白。

現(xiàn)場(chǎng)問(wèn)答環(huán)節(jié)，圍繞 RISC-V 驗(yàn)證的實(shí)戰(zhàn)難題，用戶直擊核心，專(zhuān)業(yè)提問(wèn)接踵而至，引發(fā)現(xiàn)場(chǎng)行業(yè)同仁的深度共鳴與熱烈互動(dòng)。

一位深耕芯片設(shè)計(jì)的用戶率先發(fā)問(wèn)：

“RISC-V 64位除法器的完備性驗(yàn)證是行業(yè)公認(rèn)的難題，芯華章工具在技術(shù)實(shí)現(xiàn)上有何創(chuàng)新?”

劉軍從技術(shù)原理層面給出精準(zhǔn)解答：以高基SRT算法除法算子為例，GalaxEC HEC采用“精細(xì)化Lemma拆分+多引擎協(xié)同求解”的創(chuàng)新方案，通過(guò)將除法運(yùn)算拆解為迭代公式證明、中間引理證明以及最終表達(dá)式證明三大核心步驟，結(jié)合定制化求解算法，實(shí)現(xiàn)了64位整數(shù)除法器24小時(shí)全量驗(yàn)證、32位除法器10分鐘快速驗(yàn)證的行業(yè)突破。

這一方案已在某大型CPU芯片設(shè)計(jì)客戶的實(shí)際項(xiàng)目中得到實(shí)證。該客戶初期采用純仿真驗(yàn)證方案，面臨“復(fù)雜算子驗(yàn)證不充分、邊界bug難以捕捉、大規(guī)模項(xiàng)目周期不可控”等共性問(wèn)題。

芯華章技術(shù)團(tuán)隊(duì)為其定制“分階段驗(yàn)證+算法優(yōu)化”的整體解決方案，最終不僅將驗(yàn)證覆蓋率提升至100%，更成功捕捉到超越函數(shù)邊界場(chǎng)景等仿真難以發(fā)現(xiàn)的隱蔽bug。

另一位專(zhuān)注 RISC-V 向量擴(kuò)展開(kāi)發(fā)的用戶進(jìn)一步追問(wèn)：

“很多企業(yè)直接從RTL開(kāi)發(fā)，缺乏成熟的C參考模型，芯華章提供的RV-APP如何保證模型正確性?”

劉軍從標(biāo)準(zhǔn)適配與技術(shù)驗(yàn)證雙維度回應(yīng)：“RV-APP參考模型體系基于RISC-V ISA規(guī)范與IEEE 754浮點(diǎn)標(biāo)準(zhǔn)開(kāi)發(fā)，相對(duì)于業(yè)界常用開(kāi)源SoftFloat模型，更針對(duì)性適配GalaxEC HEC底層引擎驗(yàn)證算法。

該模型不僅通過(guò)形式化工具完成全量驗(yàn)證，更針對(duì)AI客戶高頻的矢量運(yùn)算場(chǎng)景做了針對(duì)性算法-引擎聯(lián)合優(yōu)化，證明效率提升300%以上。

模型的每一個(gè)運(yùn)算單元都經(jīng)過(guò)‘公式證明+標(biāo)準(zhǔn)比對(duì)’雙重校驗(yàn)，例如整數(shù)除法算子通過(guò)其乘法逆元 ‘商×除數(shù)+余數(shù)=被除數(shù)’的數(shù)學(xué)定理進(jìn)行完備驗(yàn)證，確保完全符合RISC-V指令約束，客戶可直接開(kāi)箱即用，大幅縮短研發(fā)周期。”

設(shè)計(jì)出身的用戶則更關(guān)注技術(shù)落地門(mén)檻：

“我們團(tuán)隊(duì)形式化驗(yàn)證經(jīng)驗(yàn)較少，芯華章工具在Lemma拆分等專(zhuān)業(yè)操作上是否有標(biāo)準(zhǔn)化方案?”

劉軍給出明確指引：“針對(duì)RISC-V典型算子，我們已形成標(biāo)準(zhǔn)化拆分指引流程，例如SRT整數(shù)除法按‘迭代-中間引理-最終表達(dá)式證明’三步拆分，浮點(diǎn)除法算子按‘尾數(shù)定點(diǎn)除法部分證明-浮點(diǎn)除法部分證明’兩層驗(yàn)證。

配合與芯華章Fusion Debug深度融合的可視化調(diào)試工具，雙擊告警可自動(dòng)生成波形，再點(diǎn)一步直達(dá)源碼對(duì)比界面，將問(wèn)題定位時(shí)間從小時(shí)級(jí)壓縮至分鐘級(jí)。

設(shè)計(jì)人員無(wú)需深厚的形式化背景即可快速上手，目前新客戶平均1周即可完成工具部署與典型中低端難度算子驗(yàn)證上手?！?/p>

面對(duì)不斷變化的市場(chǎng)需求和技術(shù)挑戰(zhàn)，芯華章將始終以 “技術(shù)深耕” 為底色，用成熟的工具方案支撐產(chǎn)業(yè)鏈伙伴縮短研發(fā)周期、突破驗(yàn)證卡點(diǎn)，以踏實(shí)的技術(shù)迭代、專(zhuān)業(yè)的服務(wù)能力持續(xù)致力于探索EDA工具的創(chuàng)新路徑，為客戶提供更加高效、可靠的驗(yàn)證解決方案。