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

导语

一个价值千亿的行业痛点

一颗芯片包含上百亿个晶体管，即使只有一个逻辑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覆盖率达成，让验证没有死角。

实测数据：

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

从“百米冲刺”看形式化验证告别“马拉松“

在开源RISC-V CPU核PicoRV32上的实测显示，该用例覆盖率由53%上升至91%，自动化流程整体用时约30分钟。人工完成代码阅读、设计理解、Property手写、Tcl脚本调试及覆盖率收敛，基线时间约为8小时；与之相比，整体速度提升约16倍。

覆盖率跃升：从“及格线”直达“优秀”

核心指标对比

这代表什么?

过去要用一整天完成的验证工作，如今在喝杯咖啡的时间内即可结束，覆盖率也随之跃升并接近完美目标，工程师因而能够把精力转向更具价值的架构创新。

它为何具有“革命性”?

人工写断言 → 人工跑工具 → 人工分析结果 → 人工增加断言 →循环往复，这套依靠人员反复操作的过程，构成传统形式化验证的核心，即“人工驱动”。

以“AI驱动”为核心，HimaFormal MC+UCAgent把自动化流水线组织为以下流程：先输入RTL/自然语言描述，由AI大模型自动生成SVA断言；再让HimaFormal MC运行形式化验证，并由AI大模型针对错误运行结果给出根因分析；随后AI大模型生成更多断言属性，使形式化验证经迭代达到COI覆盖率收敛，最终自动生成运行过程和结果报告。

四句话概括核心价值

人人可用：自然语言交互推动形式化验证进一步普及，让用户摆脱晦涩SVA语法；

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

结果可信：双重保障来自AI诊断的可解释性 + 数学证明的确定性;

闭环无忧：功能验证要实现自动全覆盖，由覆盖率驱动的自动补全机制完成。

用户导入后的实际成效

该流程的企业应用已有两种：某深圳SSD主控芯片公司将其设为公司内部芯片数字验证流程的统一智能体接口，并开展优化开发;某头部AI芯片公司则将其接入公司内部的大模型，让形式化验证流程实现自动化。

方法学能力进一步拓展

人工智能大模型不仅通过智能体接入HimaFormal HiLEC和 HimaFormal EC，也接入HimaFormal MC；这些产品共同构成华大九天的全系列形式验证产品。

基于人工智能大模型的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、晶圆制造工程服务及其他相关服务。产品和服务主要应用于集成电路设计、制造及封装领域。

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