华大九天正式推出智能形式化验证解决方案

导语

千亿价值背后的验证痛点

一颗芯片包含上百亿个晶体管，即使只有一个逻辑Bug深藏其中，也可能造成流片失败，令数千万美元付诸东流。业界将形式化验证(Formal Verification)视为实现"零缺陷芯片"的终极解法，它以数学证明穷举分析全部状态空间，带来100%的确定性保障。

过去，这项技术仅掌握在少数"顶尖高手"手中：验证断言(SVA)使用晦涩的专用语法，学习门槛较高；覆盖率依靠人工反复迭代收敛，耗时较长；调试如同"盲人摸象"，效率有所损失。如今，人工智能大模型技术可能重塑形式化EDA产品。

正式亮相：AI+形式化验证的"王炸组合"

高效实用的智能形式化验证解决方案，由北京开源芯片研究院("开芯院")、中国科学院计算技术研究所("计算所")的AI Agent(UCAgent)，联合北京华大九天科技股份有限公司(“华大九天”)旗下形式验证产品Empyrean HimaFormal MC共同形成。

从"意图描述"通往"100%验证闭环"的最后一公里由此被成功打通，这是全球首次让大模型智能体深度参与形式化验证全流程；原本门槛很高的"数学证明"因而能够人人使用，并兼具结果可信、效率倍增与闭环无忧。

四项超能力：用聊天方式完成芯片验证

1 自然表达，生成断言——专业代码由自然语言快速转化

以前：一个模块可能涉及几百行复杂验证断言，工程师既要精通SVA语法，又得逐行手写。

现在：覆盖仲裁、时序、协议等场景的SVA断言，可由AI在自动理解自然语言设计意图或上传的RTL代码后生成。

2 严格把关，发现漏洞——自动反例 + 数学证明

断言生成后会立即进入HimaFormal MC引擎，由其执行严格的数学推理和穷举证明，并在全状态空间内自动探索，以判断断言能否通过。若验证失败，引擎马上生成反例激励，直接指出发生错误的输入条件，不再需要人工猜测。

3 理解容易，修改迅速——让AI担任"翻译官"和"分析师"

面对出错场景，UCAgent会作为"翻译官"和"分析师"，自动解读错误信息、查找问题根因，再用容易理解的语言向工程师提示修改方向，从而摆脱传统的盲目调试。

4 全覆盖，不留盲区——迭代自动进行至100%

未覆盖的逻辑盲区会由智能体根据COI(Cone-of-Influence，逻辑影响锥)覆盖率数据自动找出，随后补充有针对性的新断言；循环迭代无需人工介入，达到100%可证明COI覆盖率后才会结束，从而让验证不存在死角。

实测数据：

覆盖率提高38个百分点，效率提升16倍

形式化验证效率：“百米冲刺”取代“马拉松“

约8小时是人工阅读代码、手写Property、理解设计、调试Tcl脚本并完成覆盖率收敛所需的基线时间；而在开源RISC-V CPU核PicoRV32实测中，自动化流程约30分钟便使该用例覆盖率从53%升至91%，整体约有16倍提速。

覆盖率跨越：从“及格线”迈向“优秀”

核心指标比较

这些数据意味着什么?

过去需要一整天完成的验证任务，如今一杯咖啡的时间即可结束；覆盖率大幅提升并接近完美目标，工程师也能把精力转向更具价值的架构创新。

它为何称得上"革命性"?

"人工驱动"构成传统形式化验证的核心，其循环是：断言由人工写出 → 工具由人工运行 → 结果由人工分析 → 断言由人工增加 →继续循环。

以"AI驱动"为核心，HimaFormal MC+UCAgent实现的自动化流水线依次为：RTL/自然语言描述→SVA断言由AI大模型自动生成→形式化验证由HimaFormal MC运行→错误运行结果的根因由AI大模型分析→更多断言属性由AI大模型生成→通过形式化验证迭代使COI覆盖率收敛→运行过程和结果报告自动生成。

四句话概括核心价值

人人可用：自然语言交互降低形式化验证门槛，无需再面对晦涩SVA语法；

效率倍增：自动完成仅需数小时甚至数十分钟←人工迭代需要数周;

结果可信：AI诊断具有可解释性，数学证明具备确定性，形成双重保障；

闭环无忧：功能验证依靠覆盖率驱动的自动补全机制，达到自动全覆盖。

用户落地成效

形式化验证流程自动化已由某头部AI芯片公司接入其内部大模型实现;而某深圳SSD主控芯片公司将这一流程用作内部芯片数字验证流程的统一智能体接口，并已开展优化开发。

方法学能力延伸

除HimaFormal MC之外，HimaFormal HiLEC和 HimaFormal EC同样借助智能体连接人工智能大模型；它们均属于华大九天的全系列形式验证产品。

基于人工智能大模型的C/C++-to-RTL高阶等价性检查，可由HimaFormal HiLEC按以下流程实现：读入约束和设计后识别设计架构并建立顶层C模型；自行学习手册并写出TCL脚本；运行高阶等价性检查后，对错误结果作根因分析；通过增加覆盖率属性实现覆盖率收敛，最后自动生成运行过程和结果报告流程。

借助人工智能大模型技术，HimaFormal EC可以快速定位错误，明显提高调试效率，并帮助确定以往无法证明的复杂数据通路电路边界；在此基础上分割待证明电路，降低证明复杂度，最终完成电路证明。

性能效率提升和生态建设并重，是华大九天形式化验证产品未来开展人工智能开发的方向；在增强复杂验证任务处理能力的同时，还将探索用本地小模型存储关键信息，并探索AI+EDA的最优解。

合作方简介

北京开源芯片研究院——以深度融合RISC-V创新链和产业链为着力点，是国内领先的开源芯片产业化推进及研发机构。

中国科学院计算技术研究所——我国信息技术领域的奠基人和开拓者，1956年成立，享有"中国计算机事业的摇篮"之誉。

实际发布版本决定具体功能，本文提到的产品和技术仍处于持续迭代优化之中。

全流程、全领域、全球领先的EDA提供商，是北京华大九天科技股份有限公司(简称“华大九天”)致力成为的目标；该公司成立于2009年，业务始终集中在EDA工具的销售、开发及相关服务方面。

华大九天主要产品包括全定制设计平台EDA工具系统、数字电路设计EDA工具、晶圆制造EDA工具、先进封装设计EDA工具和3DIC设计EDA工具等软件及相关技术服务。其中，全定制设计平台EDA工具系统包括模拟电路设计全流程EDA工具系统、存储电路设计全流程EDA工具系统、射频电路设计全流程EDA工具系统和平板显示电路设计全流程EDA工具系统;技术服务主要包括基础IP、晶圆制造工程服务及其他相关服务。产品和服务主要应用于集成电路设计、制造及封装领域。

北京是华大九天的总部所在地；其全资子公司分布于重庆、武汉、天津、西安、北京亦庄、香港、上海、深圳、成都和南京等地，分支机构则设在苏州、厦门等地。