穹瀚GalaxFV

穹瀚 GalaxFV 是芯华章面向 HDL 电路设计的形式化验证工具，能够从数学上完备地证明电路的实现方案是否实现了设计规范所描述的功能，从而在数学层面保障设计正确性。

技术原理

GalaxFV 采用基于模型的数学求解方法，针对用户提供的规范断言与属性，面向目标 HDL 设计的所有可能输入进行证明，判定设计是否与给定规范功能一致，避免了仿真难以覆盖全部输入组合的局限，显著提升验证效率。

字级建模

GalaxFV 是国内率先采用高性能字级建模（Word-Level Modeling）方法构建的形式化验证工具。相较传统比特级建模，字级建模颗粒度更大、性能表现更好，并可同时调用字级与比特级求解器，具备较强的可扩展性，模型结构已达到国际先进水平。

核心能力

• 高并发求解器：具备自主研发的高并发高性能求解器，可在服务器集群或云平台上发挥分布式计算的强大性能，支持单机与分布式多机并发。
• 智能调度：研发了针对求解器的智能分组与调度预测算法，结合各引擎特性组合调度求解单元，进一步提高求解效率；在部分客户设计上实测性能优于既有工具。
• 应用级断言库：内置专用高效的应用级断言库，对常用标准组件构建可参数化的断言，降低构建断言与约束的难度，提高易用性；并支持 Plug-in 断言与定制化。

平台协同

GalaxFV 在保留形式化验证完备性的基础上，依托芯华章智V验证平台（FusionVerify Platform），与平台上的逻辑仿真、硬件仿真等其它验证工具在编译、调试、覆盖率等方面互融互通，帮助芯片设计在更早期阶段实现简单高效的完备验证。