芯片制造領域，一顆芯片集成了上百億個晶體管，即便僅有一個隱藏的邏輯錯誤，都可能導致價值數千萬美元的流片失敗。形式化驗證作為實現“零缺陷芯片”的關鍵技術，憑借數學證明在完整狀態空間內進行全面分析，為芯片質量提供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生態建設，中國科學院計算技術研究所則是我國計算機領域的權威科研機構，為技術突破提供了堅實基礎。