芯片制造领域，一颗芯片集成了上百亿个晶体管，即便仅有一个隐藏的逻辑错误，都可能导致价值数千万美元的流片失败。形式化验证作为实现“零缺陷芯片”的关键技术，凭借数学证明在完整状态空间内进行全面分析，为芯片质量提供100%的确定性保障。然而，这项技术曾因门槛过高，仅掌握在少数专业人士手中。如今，随着AI技术的深度融合，形式化验证正迎来一场颠覆性变革。
上海阿卡思微电子技术有限公司（北京华大九天科技股份有限公司战略参股企业）联合北京开源芯片研究院、中国科学院计算技术研究所，共同推出“HimaFormal MC+UCAgent智能形式化验证解决方案”。这一创新方案首次将大模型智能体全面融入验证全流程，从设计意图描述到最终验证闭环，彻底打破了传统技术的高门槛壁垒，让形式化验证变得简单易用、高效可靠。
该方案具备四大核心优势，重新定义了芯片验证流程。其一，自然语言交互生成断言。工程师无需掌握复杂的SVA语法，只需通过自然语言描述设计需求或上传RTL代码，AI即可自动生成覆盖协议、时序、仲裁等场景的专业断言，大幅降低技术门槛。其二，数学证明与自动反例结合。生成的断言会进入HimaFormal MC引擎进行严格推理，在全状态空间内完成验证。若验证失败，系统会立即生成反例激励，明确指出错误输入条件，避免人工排查的盲目性。
其三，AI辅助问题分析与修复。针对验证失败场景，UCAgent智能体可自动解析错误信息，定位问题根源，并以通俗语言提供修改建议，成为工程师的“智能助手”。其四，覆盖率驱动的自动迭代。UCAgent会分析逻辑影响锥（COI）覆盖率数据，识别未覆盖区域并补充新断言，通过循环迭代实现100%覆盖率，确保验证无死角。
在开源RISC-V CPU核PicoRV32的实测中，该方案展现了显著优势。验证覆盖率从53%提升至91%，自动化流程仅耗时约30分钟，而传统人工方式（包括代码阅读、属性编写、脚本调试等）需要约8小时，效率提升达16倍。这一突破意味着，原本需要一整天完成的验证工作，现在可在短时间内完成，且覆盖率从“及格”跃升至“优秀”，为工程师释放了更多时间用于架构创新。
与传统“人驱动”模式不同，新方案构建了“AI驱动”的自动化流水线：从RTL或自然语言描述开始，UCAgent自动生成断言，HimaFormal MC执行验证并生成结果，UCAgent分析结果并决定后续动作——若失败则提供修复建议，若成功则生成覆盖率报告；若覆盖率未达标，系统会自动补充断言并重新迭代，直至完成全覆盖验证。
这一变革的核心价值体现在四个方面：一是技术普及化，自然语言交互让更多工程师能够使用形式化验证；二是效率指数级提升，人工数周的迭代周期缩短至数小时甚至数十分钟；三是结果双重保障，数学证明的确定性与AI诊断的可解释性相结合；四是闭环自动化，覆盖率驱动的补全机制确保功能验证全面无遗漏。
在技术支撑层面，HimaFormal MC是阿卡思自主研发的形式化属性验证工具，性能较主流竞品提升1.5倍，并支持断言自动机运行可视化；UCAgent则由开芯院基于大语言模型开发，可实现简单模块的100%自动验证。合作方中，北京开源芯片研究院致力于推动RISC-V生态建设，中国科学院计算技术研究所则是我国计算机领域的权威科研机构，为技术突破提供了坚实基础。
