形式化验证破局验证效率瓶颈，芯华章RV-APP发布补位RISC-V产业标准验证缺口
第三届设计自动化产业峰会（IDAS）圆满落幕，在活动期间工业和信息化部电子信息司副司长王世江一行莅临芯华章展台视察指导。
芯华章科技联席CEO齐正华全程接待，并围绕公司产品最新进展及核心技术展开详细介绍，全面展现芯华章在EDA验证领域的深耕成果与创新方向。
在AI芯片定制越来越流行的时代，设计者为了提高计算效率、支持特定应用需求（如浮点运算、AI算子等），往往会对传统处理器指令（如RISC-V）进行扩展定制，增加特定的硬件指令。
这种定制化设计虽然可以显著提升芯片性能，但也带来了设计复杂性和验证的挑战。芯华章研发经理林韬博士指出，在大位宽数据通路设计验证流程中，传统仿真方案存在完备性不足、收敛效率低下、边界场景激励构建困难三大瓶颈。
打破时序绑定
专注事务级/算法级等价性验证
无需“逐时钟等价比对”，聚焦算法本质一致性，支持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工具价值也得到进一步实证：
⚪功能上，可在数学层面证明C++模型与RTL实现100%算法等价；
⚪技术上，RV-APP所提供的标准模型是经过形式化完备验证、符合RISC-V标准的指令级C++行为级模型；
⚪效率上，无需编写定制随机激励，可自动化完成全指令集验证，将指令验证时间压缩60%以上；
⚪生态上，已覆盖RV32I、RV64I等主流指令集，持续迭代标准模型，并为复杂定制指令提供专项验证服务。
