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

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

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

針對RISC-V領域“標準模型缺失、激勵開發(fā)成本高”的突出痛點，芯華章同步推出RV-APP(RISC-V指令級C++標準模型套件)，以“標準化、自動化”特性填補了行業(yè)空白。

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

一位深耕芯片設計的用戶率先發(fā)問：

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

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

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

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

另一位專注 RISC-V 向量擴展開發(fā)的用戶進一步追問：

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

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

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

模型的每一個運算單元都經過‘公式證明+標準比對’雙重校驗，例如整數除法算子通過其乘法逆元 ‘商×除數+余數=被除數’的數學定理進行完備驗證，確保完全符合RISC-V指令約束，客戶可直接開箱即用，大幅縮短研發(fā)周期?！?/p>

設計出身的用戶則更關注技術落地門檻：

“我們團隊形式化驗證經驗較少，芯華章工具在Lemma拆分等專業(yè)操作上是否有標準化方案?”

劉軍給出明確指引：“針對RISC-V典型算子，我們已形成標準化拆分指引流程，例如SRT整數除法按‘迭代-中間引理-最終表達式證明’三步拆分，浮點除法算子按‘尾數定點除法部分證明-浮點除法部分證明’兩層驗證。

配合與芯華章Fusion Debug深度融合的可視化調試工具，雙擊告警可自動生成波形，再點一步直達源碼對比界面，將問題定位時間從小時級壓縮至分鐘級。

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

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