形式化验证的AI时代: HimaFormal MC+UCAgent实现形式化验证全自动智能化
随着芯片设计复杂度不断攀升，如何确保隐藏在代码中的逻辑Bug无处遁形，成为芯片成功流片的关键。形式化验证（Formal Verification）技术通过严谨的数学证明，在芯片设计的全部状态空间内进行穷尽式分析，提供“数学确定性”的保障。这无疑是通往“零缺陷”芯片的最优路径。然而，形式化验证存在两大难题：一是编写验证规则（SVA断言）需要极高的专业技能，二是实现100%的验证覆盖率过程繁琐且耗时。
近日，国内领先的EDA企业上海阿卡思微电子技术有限公司（北京华大九天科技股份有限公司战略参股公司）与北京开源芯片研究院（简称“开芯院”）、中国科学院计算技术研究所（ICT，简称“计算所”）合作，推出“HimaFormal MC+UCAgent智能形式化验证解决方案”。该方案首次将人工智能大模型智能体深度融入形式化验证全流程，成功打通了从“意图描述”到“100%验证闭环”的最后一公里，让原本高门槛的“数学证明”变得人人可用。
形式化验证是一种通过数学方法证明设计无误的“白盒”技术，能从根源上排查风险。但在实际工程中，它长期面临两大应用痛点：
-
门槛高：编写验证专用的SVA断言语言像做“数学证明题”，极度依赖资深专家，费时费力。
-
收敛慢：确保逻辑覆盖率达标需要反复手工迭代，周期漫长。
HimaFormal MC+UCAgent方案将阿卡思自研的HimaFormal MC形式化工具与开芯院自主研发的UCAgent大模型智能体相结合，构建了从“一句需求描述”到“100%验证覆盖”的形式验证自动化流水线。HimaFormal MC+UCAgent的核心价值在于其端到端的智能化与自动化，它彻底重构了传统形式化验证的工作流。形式化验证的流程如下图，左边是典型的形式化验证方案，人工介入较多，右边是HimaFormal MC+UCAgent的智能形式化验证方案，即从一条提示到形式化验证100%覆盖率闭环，构建了自动化验证闭环，该方案中调用的模型可选通用人工智能大模型，通过MCP接口与UCAgent智能体交互运行。
用户无需精通繁琐的SVA语法，只需提供RTL设计描述或自然语言规范，工具便能自动理解设计意图，智能生成覆盖协议、时序、仲裁等各种场景的SVA断言。
生成的断言随即送入HimaFormal MC引擎进行严格的数学推理与穷举证明。工具将在全状态空间内自动探索，判定断言通过与否，一旦失败即刻生成反例激励。
针对出错场景，工具充当了“翻译官”与“分析师”，自动解析错误信息、定位问题根因，并以通俗易懂的语言提示工程师修改方向，告别传统调试的盲目性。
UCAgent智能体分析COI（Cone-of-Influence，逻辑影响锥）覆盖率数据，自动识别未被覆盖的逻辑盲区，并针对性地补充新断言。这一过程将自动循环迭代，直至达成100%可证明COI覆盖率，确保验证不留死角。此外，针对ProofCore的覆盖率数据分析功能也将推出。
-
人人可用：告别晦涩的SVA语法，通过自然语言交互让形式化验证进一步普及。
-
效率倍增：将原本需要数周的人工迭代工作，压缩至数小时甚至更短。
-
结果可信：数学证明的确定性+AI诊断的可解释性，双重保障验证质量。
-
闭环无忧：依托覆盖率驱动的自动补全机制，实现功能验证的自动全覆盖。
目前，HimaFormal MC+UCAgent 智能验证解决方案已面向国内芯片设计企业开放试用，UCAgent程序代码已在GitHub开源。
未来，阿卡思将继续深化AI与EDA的融合，提升 HimaFormal MC 形式化验证软件的断言属性质量，提高 HimaFormal EC 等价性检查和 HimaFormal HiLEC 高阶等价性检查的调试效率，构建全流程智能化形式验证生态。
北京开源芯片研究院是国内领先的开源芯片研发及产业化推进机构，着力推动RISC-V创新链与产业链的深度融合，加速科技成果落地，构建全球领先的RISC-V产业生态。
中国科学院计算技术研究所是中国科学院下属、中国第一个专门从事计算机科学技术综合性研究的学术机构，成立于1956年，被誉为“中国计算机事业的摇篮”。作为我国信息技术领域的开拓者和奠基人，计算所秉持“基础性、战略性、前瞻性”的三性原则，坚持“四个面向”，致力于建成引领创新型战略高技术研究所，保障国家信息安全，引领产业技术方向，率先成为世界一流水平的科研机构。
关于上海阿卡思
上海阿卡思微电子技术有限公司由硅谷回国的资深电子设计自动化(EDA)专家于2020年在上海张江高科技园区设立，旗下子公司成都奥卡思微电科技有限公司于2018年在成都高新区创立，公司聚集国际知名EDA公司和芯片设计公司具有多年研发经验的尖端人才，基于形式化方法为逻辑芯片设计和工控软件等提供验证工具及验证咨询服务，凭借在形式化方法领域深厚的技术积累及深入的产品实践，已推出多款商用性能优异的核心验证工具及其他相关验证工具，服务于复杂芯片设计及通用设计流程，公司产品获得四十余个客户，包括国家头部通讯、高性能计算及AI芯片企业等标杆客户的采购、使用及好评。公司将紧密把握IC设计复杂度提升及验证方法学多样化需求提升的趋势，致力于成为国内领先的形式化技术开发与服务商。
夜雨聆风
