第三屆設計自動化產業峰會（IDAS）圓滿落幕，在活動期間工業和信息化部電子信息司副司長王世江一行蒞臨芯華章展臺視察指導。

芯華章科技聯席CEO齊正華全程接待，并圍繞公司產品最新進展及核心技術展開詳細介紹，全面展現芯華章在EDA驗證領域的深耕成果與創新方向。

同期，芯華章受邀參與數字芯片論壇分享——以形式化驗證技術創新為核心，介紹芯華章GalaxEC HEC高階等價性檢查工具如何提升芯片驗證效率，同時首發新品RV-APP(RISC-V指令級C++模型套件)，以“標準化、自動化”填補產業標準驗證資源空白。

在AI芯片定制越來越流行的時代，設計者為了提高計算效率、支持特定應用需求（如浮點運算、AI算子等），往往會對傳統處理器指令（如RISC-V）進行擴展定制，增加特定的硬件指令。

這種定制化設計雖然可以顯著提升芯片性能，但也帶來了設計復雜性和驗證的挑戰。芯華章研發經理林韜博士指出，在大位寬數據通路設計驗證流程中，傳統仿真方案存在完備性不足、收斂效率低下、邊界場景激勵構建困難三大瓶頸。

芯華章GalaxEC HEC高階等價性檢查工具并非對傳統驗證方案的局部優化，而是從驗證邏輯根源出發，以形式化驗證算法創新為核心，形成兼具“完備性、效率、易用性”的一體化解決方案：

打破時序綁定

專注事務級/算法級等價性驗證

無需“逐時鐘等價比對”，聚焦算法本質一致性，支持C++/C/RTL跨語言、同語言對比及高級綜合正確性驗證；

C++模型語法支持度高，可將C/C++代碼轉換為形式化模型，且支持ANSI C++17標準，支持指針算術/內存讀寫；

工具會自動生成C++運行時安全檢查引理（例如數組越界、除零等）并進行自動化完備性檢查，保障C/C++參考模型質量。

自研引擎+加速技術

打破收斂瓶頸

在數據通路繁重的大位寬電路設計過程中，驗證收斂是最大的難題之一，為突破這一難題，GalaxEC HEC工具做了兩大核心設計：

通過“Case拆分+多引擎協同”，將例如64位浮點乘法、除法等復雜任務自動完備地拆分為子任務進行并行驗證，各引擎實時交互實現“1+1>2”協同效應，目前已實現整數 / 浮點乘法, 除法和乘累加、各類加解密算法、超越函數等典型算子的快速收斂。

創新性的“No-Spec”模式，無需依賴算法參考模型，可直接通過GalaxEC HEC工具開放接口構造RTL實現的算法范式并進行快速證明；結合引擎優化技術，在客戶真實設計中，將Int64類型MAC算子從“24小時無法證明收斂”提升至60秒內完備驗證。

通過以上加速技術，GalaxEC HEC在客戶端已實現64位雙精度浮點乘法200秒完備證明、8位無符號類型向量點乘5小時內完成驗收收斂，效率超傳統工具10倍。

深度融合Fusion Debug

提升調試效率

通過與芯華章Fusion Debug深度融合，Debug流程得以簡化，雙擊引理驗證失敗告警標志，即可一鍵式自動生成波形，并并列式展示C++/RTL源碼對比界面。

這使得問題定位時間從小時級壓縮至分鐘級，大幅減少了繁雜的調試和根因定位工作。

在客戶項目中，GalaxEC HEC工具價值也得到進一步實證：

在某大型CPU芯片設計客戶的40+算子驗證項目（含30+浮點算子）中，GalaxEC HEC精準捕捉傳統仿真難以正向構建的“超越函數邊界場景計算bug”，補齊驗證漏洞；后續9倍規模算子驗證項目中，在未增人員的情況下同周期完成驗證，支撐芯片按期流片。

對客戶而言，GalaxEC HEC的價值不僅是效率提升，更在于風險可控，為芯片質量提供長線保障。

針對RISC-V“標準模型缺失、激勵開發成本高”痛點，芯華章發布RV-APP（RISC-V指令級C++標準模型套件），以“標準化、自動化”填補行業空白：

功能上，可在數學層面證明C++模型與RTL實現100%算法等價；

技術上，RV-APP所提供的標準模型是經過形式化完備驗證、符合RISC-V標準的指令級C++行為級模型；

效率上，無需編寫定制隨機激勵，可自動化完成全指令集驗證，將指令驗證時間壓縮60%以上；

生態上，已覆蓋RV32I、RV64I等主流指令集，持續迭代標準模型，并為復雜定制指令提供專項驗證服務。

從GalaxEC HEC工具破解傳統驗證困局，到RV-APP錨定RISC-V產業未來發展方向，芯華章始終以“技術深耕”為核心——憑借可落地、可量化的方案解決工程師當下痛點。 在芯片研發“效率與質量并重”的時代，我們將持續以踏實的技術實力，為用戶提供更多差異化的解決方案。