导语

一个价值千亿的行业痛点

一颗芯片包含上百亿个晶体管，即使只有一个逻辑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上的实测覆盖率达到91%，此前为53%，自动化流程约30分钟即可完成。若采用人工方式，阅读代码、理解设计、手写Property、调试Tcl脚本以及收敛覆盖率的基线耗时约8小时，因此整体速度约为原来的16倍。

覆盖率跃升：由“及格线”迈向“优秀”

核心指标对比

这意味着什么?

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

为何称其为"革命性"?

人工写断言 → 人工跑工具 → 人工分析结果 → 人工增加断言 →循环往复，这套由各环节反复人工操作构成的流程，正是传统形式化验证"人工驱动"的核心。

以"AI驱动"为核心，HimaFormal MC+UCAgent把各环节串成自动化流水线：输入RTL/自然语言描述→由AI大模型自动生成SVA断言→通过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年，并被誉为"中国计算机事业的摇篮"。

文中涉及的产品与技术仍在持续迭代优化，实际功能请以正式发布版本为准。

自2009年成立以来，北京华大九天科技股份有限公司(简称“华大九天”)始终以EDA工具的开发、销售及相关服务业务为聚焦方向，致力于成长为全球领先且覆盖全流程、全领域的EDA提供商。

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

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