一个价值千亿的痛点

一颗芯片里有上百亿个晶体管，哪怕只有一个逻辑Bug藏在深处，流片失败就是数千万美元打水漂。形式化验证（Formal Verification）被业界公认为“零缺陷芯片”的终极解法——它用数学证明在全部状态空间内穷举分析，提供100%的确定性保障。

但过去，这项技术是少数“顶尖高手”的专利：写验证断言（SVA）需要精通晦涩的专用语法，门槛极高；人工迭代收敛覆盖率，动辄数周时间；调试过程像“盲人摸象”，效率低下。现在，这一切被重构了。

重磅发布：AI+形式化验证的“王炸组合”

上海阿卡思微电子技术有限公司（北京华大九天科技股份有限公司战略参股公司）联合北京开源芯片研究院（“开芯院”）、中国科学院计算技术研究所（“计算所”），正式推出「HimaFormal MC+UCAgent智能形式化验证解决方案」。

这是全球首次将大模型智能体深度融入形式化验证全流程，成功打通了从“意图描述”到“100%验证闭环”的最后一公里，让原本高门槛的“数学证明”变得人人可用、效率倍增、结果可信、闭环无忧。

四大超能力：像聊天一样做芯片验证

1、说人话，写断言——自然语言秒变专业代码

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

现在：只需用自然语言描述设计意图，或上传RTL代码，AI就能自动理解并生成覆盖协议、时序、仲裁等场景的SVA断言。

2、严把关，找漏洞——数学证明 + 自动反例

生成的断言随即送入HimaFormal MC引擎进行严格的数学推理与穷举证明。工具在全状态空间内自动探索，判定断言通过与否。一旦失败，立刻生成反例激励——直接告诉你在什么输入条件下会出错，无需人工猜测。

3、看得懂，改得快——AI当你的“翻译官”和“分析师”

针对出错场景，UCAgent充当“翻译官”与“分析师”，自动解析错误信息、定位问题根因，并以通俗易懂的语言提示工程师修改方向。告别传统调试的盲目性。

4. 扫盲区，全覆盖——自动迭代直到100%

UCAgent智能体分析COI（Cone-of-Influence，逻辑影响锥）覆盖率数据，自动识别未被覆盖的逻辑盲区，并针对性地补充新断言。这一过程自动循环迭代，直至达成100%可证明COI覆盖率，确保验证不留死角。

实测数据：效率提升16倍，覆盖率飙升38个百分点

在开源RISC-V CPU核PicoRV32上进行实测，该用例的覆盖率从53%提升到91%，自动化流程总耗时约30分钟。相比人工阅读代码、理解设计、手写Property、调试Tcl脚本并进行覆盖率收敛的约8小时基线，整体提速约16倍。

核心指标对比：

这意味着什么？

原本需要一整天的验证工作，现在喝杯咖啡的时间就完成了覆盖率从"不及格"直接跃升到"优秀"，逼近完美目标，工程师可以将精力投入到更有价值的架构创新上。

为什么这是“革命性”的？

传统形式化验证是“人驱动”的：人写断言 → 人跑工具 → 人分析结果 → 人补断言 →循环往复。

HimaFormal MC+UCAgent实现了“AI驱动”的自动化流水线：RTL/自然语言描述→UCAgent自动生成SVA断言→HimaFormal MC运行形式化验证→生成反例激励+断言验证结果→UCAgent分析结果→[失败]自动分析反例并提示修复/[成功]生成COI覆盖率报告→覆盖率达标？是→验证完成/否→自动补充断言→循环迭代

核心价值四句话：

人人可用：告别晦涩SVA语法，自然语言交互让形式化验证进一步普及；

效率倍增：数周人工迭代→数小时甚至数十分钟自动完成；

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

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

未来展望：构建全流程智能化形式化验证生态

阿卡思将持续深化AI与EDA的融合，提升相关产品的使用质量及使用效率，构建全流程智能化形式化验证生态，助力中国芯片产业实现“零缺陷”目标。

关于产品工具

HimaFormal MC——公司自研的形式化属性验证工具，较主流竞品有1.5倍性能优势，并提供断言自动机运行可视化功能。

UCAgent——开芯院自主研发的基于大语言模型的自动化硬件验证AI Agent，支持简单模块100%自动验证。

关于合作方

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

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

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