第三届设计自动化产业峰会（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产业未来发展方向，芯华章始终以“技术深耕”为核心——凭借可落地、可量化的方案解决工程师当下痛点。 在芯片研发“效率与质量并重”的时代，我们将持续以踏实的技术实力，为用户提供更多差异化的解决方案。
来源：芯华章科技