芯华章GalaxEC HEC工具破解RISC-V验证难题

11月3日，由中国计算机学会主办的年度盛会CCF DAC圆满落幕。芯华章研发副总裁刘军受邀致主题演讲，系统分享了GalaxEC HEC工具从技术架构到RISC-V算子完备验证场景的精准适配，从核心算法创新到大规模项目落地的实践路径。

当前，RISC-V开源架构的灵活性推动了定制化设计的爆发式增长，同时也衍生出规范宽泛、算子复杂、全场景仿真验证收敛困难等核心痛点。这些问题直接导致RISC-V芯片验证周期失控、流片风险攀升，成为制约行业发展的共性难题。

作为芯华章自主研发的高阶等价性检查工具，GalaxEC HEC专为AI芯片、DSP及RISC-V定制芯片的数据通路验证打造。

针对RISC-V领域“标准模型缺失、激励开发成本高”的突出痛点，芯华章同步推出RV-APP(RISC-V指令级C++标准模型套件)，以“标准化、自动化”特性填补了行业空白。

现场问答环节，围绕 RISC-V 验证的实战难题，用户直击核心，专业提问接踵而至，引发现场行业同仁的深度共鸣与热烈互动。

一位深耕芯片设计的用户率先发问：

“RISC-V 64位除法器的完备性验证是行业公认的难题，芯华章工具在技术实现上有何创新?”

刘军从技术原理层面给出精准解答：以高基SRT算法除法算子为例，GalaxEC HEC采用“精细化Lemma拆分+多引擎协同求解”的创新方案，通过将除法运算拆解为迭代公式证明、中间引理证明以及最终表达式证明三大核心步骤，结合定制化求解算法，实现了64位整数除法器24小时全量验证、32位除法器10分钟快速验证的行业突破。

这一方案已在某大型CPU芯片设计客户的实际项目中得到实证。该客户初期采用纯仿真验证方案，面临“复杂算子验证不充分、边界bug难以捕捉、大规模项目周期不可控”等共性问题。

芯华章技术团队为其定制“分阶段验证+算法优化”的整体解决方案，最终不仅将验证覆盖率提升至100%，更成功捕捉到超越函数边界场景等仿真难以发现的隐蔽bug。

另一位专注 RISC-V 向量扩展开发的用户进一步追问：

“很多企业直接从RTL开发，缺乏成熟的C参考模型，芯华章提供的RV-APP如何保证模型正确性?”

刘军从标准适配与技术验证双维度回应：“RV-APP参考模型体系基于RISC-V ISA规范与IEEE 754浮点标准开发，相对于业界常用开源SoftFloat模型，更针对性适配GalaxEC HEC底层引擎验证算法。

该模型不仅通过形式化工具完成全量验证，更针对AI客户高频的矢量运算场景做了针对性算法-引擎联合优化，证明效率提升300%以上。

模型的每一个运算单元都经过‘公式证明+标准比对’双重校验，例如整数除法算子通过其乘法逆元 ‘商×除数+余数=被除数’的数学定理进行完备验证，确保完全符合RISC-V指令约束，客户可直接开箱即用，大幅缩短研发周期。”

设计出身的用户则更关注技术落地门槛：

“我们团队形式化验证经验较少，芯华章工具在Lemma拆分等专业操作上是否有标准化方案?”

刘军给出明确指引：“针对RISC-V典型算子，我们已形成标准化拆分指引流程，例如SRT整数除法按‘迭代-中间引理-最终表达式证明’三步拆分，浮点除法算子按‘尾数定点除法部分证明-浮点除法部分证明’两层验证。

配合与芯华章Fusion Debug深度融合的可视化调试工具，双击告警可自动生成波形，再点一步直达源码对比界面，将问题定位时间从小时级压缩至分钟级。

设计人员无需深厚的形式化背景即可快速上手，目前新客户平均1周即可完成工具部署与典型中低端难度算子验证上手。”

面对不断变化的市场需求和技术挑战，芯华章将始终以 “技术深耕” 为底色，用成熟的工具方案支撑产业链伙伴缩短研发周期、突破验证卡点，以踏实的技术迭代、专业的服务能力持续致力于探索EDA工具的创新路径，为客户提供更加高效、可靠的验证解决方案。