芯华章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流程等核心能力，进一步降低形式验证的落地门槛，助力更多验证团队突破验证瓶颈。
