穹瀚GalaxFV：国内率先基于字级建模的可扩展形式化验证工具_芯华章科技股份有限公司_智能制造博览会

穹瀚GalaxFV：国内率先基于字级建模的可扩展形式化验证工具

关键词：HDL电路设计

所属领域：

SoC设计与功能验证

适用行业：

电子与通信

案例介绍

咨询留言

芯华章穹瀚GalaxFV是一种面向HDL电路设计的形式化验证工具，能够从数学上完备地证明电路的实现方案是否实现了设计规范所描述的功能。其采用基于模型的数学求解方法，针对用户提供的规范断言和属性，面向目标HDL设计的所有可能输入进行证明，确定该设计是否与给定的规范功能一致，从而极大地提升验证效率。穹瀚GalaxFV是国内率先采用高性能字级建模（Word-Level Modeling）方法构建的形式化验证工具。相比于传统比特级建模（Bit-Level Modeling）方法, 字级建模（Word-Level Modeling）方法建模颗粒度大、性能表现好，并可同时调用字级求解器和比特级求解器，可扩展性能力强。在模型结构上已达到国际先进水平。

穹瀚GalaxFV具备自主研发的高并发高性能求解器，在服务器集群或云平台上发挥分布式计算的强大性能，为快速证明求解赋能。并且，穹瀚GalaxFV研发了针对求解器的智能分组和调度预测算法，结合各引擎具体实现算法和特性，在面对不同的设计和断言类型时，组合调度各个求解器单元，进一步提高求解效率。结合了这些技术特点，穹瀚GalaxFV在一些客户设计上给出了亮眼的性能表现，相比于现有的形式化验证工具，实测性能超越约20% 。

此外，穹瀚GalaxFV自主研发了专用高效的应用级断言库，对设计中常用到的标准组件构建断言库，对其参数化，提高可配置性，降低了用户构建断言与约束的难度，提高了易用性和使用效率，为形式化验证应用于产业降低了门槛。

穹瀚GalaxFV在保留形式化验证完备性的基础上，依托于芯华章智V验证平台（FusionVerify Platform）, 与其他验证工具在编译、调试、覆盖率等方面互融互通，进一步加速设计验证收敛，帮助芯片设计在更早期阶段，进行简单高效的完备验证。

(1)仅针对某AsyncFIFO设计实测得出
产品特点

专家团队
芯华章形式化验证工具开发团队由海外归国的资深专家领衔，在形式化验证工具研发方面，积累了数十年开发经验，具备国际化技术视野并拥有多个项目成功开发经历，对形式化模型与求解有深入的理解，为国内形式化验证工具研发领域一支不可忽视的生力军。

关于芯华章
芯华章聚集全球EDA行业精英和尖端科技领域人才，以智能调试、智能编译、智能验证座舱、智能云原生等技术支柱，构建芯华章平台底座，提供全面覆盖数字芯片验证需求的七大产品系列，包括：硬件仿真系统、FPGA原型验证系统、智能场景验证、形式验证、逻辑仿真、系统调试以及验证云，为合作伙伴提供自主研发、安全可靠的芯片产业解决方案与专家级顾问服务。同时，芯华章致力于面向未来的EDA 2.0 智能化电子设计平台的研究与开发，以技术革新加速系统创新效率，让芯片设计更简单、更普惠。

如果您对此感兴趣，欢迎问问展商吧！

芯华章科技股份有限公司