芯华章GalaxFV模型检测解决方案及成功案例分享

CCF中国软件大会

芯华章GalaxFV融合AI，构建覆盖多个芯片验证场景的形式化验证APP矩阵，在国内头部GPGPU、车规芯片等多个行业核心项目中落地。

本次受中国计算机学会(CCF)邀请，在中国软件大会上围绕形式化验证分享GalaxFV模型检测解决方案及成功案例。

“验证周期能不能再压一压”

“怎么才能更早地发现bug”

“门槛太高难上手”

这些看似直白的诉求背后，藏着的其实是验证工作的核心矛盾——

不是单纯追求“快”，而是要“快且全”;不是盲目压缩时间，而是要把精力用在有效验证上;不是被动应对复杂设计，而是要找到适配场景的精准解法。

当用户纠结于“如何提高效率”“如何降低风险”时，本质上是在问：有没有一套方案，能真正解决验证中的无效内耗、早期bug难发现、复杂场景搞不定的痛点?

相较于传统仿真验证，形式化验证能够“穷尽式覆盖+早期介入”，是一种非常完备的验证方法，但落地难点在于“工具易用性、场景适配性、效率平衡”。

芯华章科技基于Model Checking的形式验证解决方案，从“可落地性、完备性、高效性”出发，为芯片设计企业、验证团队提供一套既能破解瓶颈，又能快速落地的验证方案。

为什么选择形式化验证

验证完备性：穷尽所有状态空间，精准捕捉并发逻辑等复杂场景下的高风险 bug

早期问题排查：无需等待系统全串联，在芯片设计验证早期即可定位并解决问题，大幅缩短研发周期

便捷高效部署：无需人工构建激励，通过约束(Assume)自动生成激励，结合 SVA 断言检测、自动覆盖率收集，快速搭建验证环境

快速 bug 定位：Cycle by Cycle遍历状态空间，可输出最短错误路径，解决传统仿真 “难定位、慢排查” 的痛点

高可复用性：基于模块功能设计验证平台，可跟随 RTL 模型迭代复用，无需重复搭建测试平台，提升验证复用效率

GalaxFV 场景化APP矩阵精准匹配验证需求

时序等价性验证：SEC APP

解决时序优化、功耗优化、流水线重构后的时序一致性验证问题，无需检查中间状态，也无需依赖综合工具提供比较点信息。

大规模连接性校验：CC APP

针对信号预留穿线场景，检测预留的连接是否正确;选择器模块中不同片选信号对应连通正确性检测;constant、reset/clock以及Debug信号连接正确性检测。

覆盖率收敛加速：FRC APP

联合芯华章GalaxSim，读取 GalaxSim生成的XCOVDB 覆盖率数据库，检查(check)无法到达(unreachable)的状态空间，自动剔除设计中完全不可达的状态空间，聚焦有效覆盖场景，大幅提升仿真覆盖率收敛速度，破解传统仿真 “60% 后覆盖率难收敛” 瓶颈。

大模型SVA自动化校验：SVAC APP

与中兴微电子、国创中心联合研发，通过SVAC评估大语言模型生成的SVA 与自然语言描述的设计要求是否一致，提升大语言模型生成SVA的质量，大幅减少验证工程师耗时耗力的SVA编写工作。

早期X态传播检测：X-PROP APP

用于芯片设计迭代早期，检查迭代过程中出现的X态。可精准检测 DUT 内部(未初始化寄存器、多驱信号等)产生及外部传入的 X 态传播，提前规避 X 态传播导致的后期设计异常。

多场景案例落地分享

芯华章形式化验证工具GalaxFV解决方案已在国内头部芯片企业、车规芯片、GPGPU等多个核心项目中落地。

解决超大规模验证平台约束冲突

项目痛点：某客户模块A出现大规模(1000+条)约束冲突，某国际主流工具无法排查，验证进度阻塞;模块C验证证明耗时太长，一次回归需要32个小时。

落地效果：通过与客户合作开发出约束冲突查找功能，且进行工具化，有效提高回归效率，模块A最终在30分钟内完成约束冲突排查;通过优化模型+定制引擎等方式，将模块C的证明时间缩短到了15个小时。

车规芯片高复杂度验证

项目痛点：某新能源汽车车规芯片，算法逻辑复杂、状态空间巨大，数据位宽大，压缩算法证明收敛难度高，某国际主流工具耗时30小时仍有8条property无法证明。

落地效果：基于高性能自适应引擎调度系统，对property自动分组与排序，同时GalaxFV基于字级模型建模在处理复杂运算相关数据通路具备巨大优势，最终GalaxFV FPV 2小时内完成全部Property证明，结果正确，工具功能正确。

路由模块数据一致性验证

项目痛点：某客户路由模块，需通过scoreboard检测数据一致性;对于部分property，第三方工具仅能完成有界证明(Bounded Proof)，存在潜在风险。

落地效果：实现100%完全证明(Full Proof)收敛，性能与第三方工具持平;其中通过引擎定制优化，将88个有界证明的Property变成完全证明。

芯华章科技始终以解决客户实际痛点为核心，未来，我们将持续优化工具的易用性与场景适配性，完善COI及Formal Core覆盖率分析、加速证明收敛、强化sign-off流程等核心能力，进一步降低形式验证的落地门槛，助力更多验证团队突破验证瓶颈。