由上海 EDA/IP 創(chuàng)新中心、張江高科與上海市集成電路行業(yè)協(xié)會(huì)聯(lián)合主辦，上海市經(jīng)濟(jì)和信息化委員會(huì)指導(dǎo)的《人工智能在 EDA 領(lǐng)域的應(yīng)用與探討》成功舉辦。會(huì)上，芯華章科技副總裁劉軍系統(tǒng)的分享了“AI+EDA”如何重塑驗(yàn)證效率以及客戶應(yīng)用成果。

驗(yàn)證自動(dòng)化應(yīng)該是每個(gè)驗(yàn)證工程師的終極夢想，這不僅意味著效率的提升，更代表著可以將工程師從重復(fù)繁重的手工任務(wù)中解放出來，將創(chuàng)造力聚焦于更具挑戰(zhàn)性的設(shè)計(jì)優(yōu)化難題。

但現(xiàn)實(shí)有著重重挑戰(zhàn)：

編寫定向測試用例耗時(shí)漫長，激勵(lì)分布易偏置導(dǎo)致覆蓋率難以提升

SVA語法復(fù)雜令人生畏，手工編寫易錯(cuò)且效率低下

面對海量回歸失敗，定位根因如同大海撈針

針對這些驗(yàn)證中的“硬骨頭”問題，芯華章以 AI 技術(shù)為核心驅(qū)動(dòng)力，構(gòu)建系統(tǒng)性解決方案，直擊驗(yàn)證中的瓶頸問題。

加速驗(yàn)證收斂：讓測試生成更智能高效

針對仿真驗(yàn)證中測試用例生成低效、激勵(lì)偏置導(dǎo)致覆蓋率難提升的痛點(diǎn)，芯華章引入機(jī)器學(xué)習(xí)技術(shù)，用已生成用例引導(dǎo)隨機(jī)約束求解器動(dòng)態(tài)優(yōu)化激勵(lì)分布。

這種 AI 引導(dǎo)模式將工程師驗(yàn)證經(jīng)驗(yàn)轉(zhuǎn)化為可迭代算法模型，大幅提升測試生成的針對性與高效性，加速功能覆蓋率收斂，讓工程師擺脫重復(fù)試錯(cuò)的激勵(lì)/約束編寫工作，聚焦更高層次的驗(yàn)證策略制定。

Auto Debug：快速定位回歸失敗根源

面對回歸測試中數(shù)千個(gè)仿真失敗用例的排查難題，AI 自動(dòng)故障聚類（Failure Binning）將海量失敗歸納為少數(shù)核心根因。

通過與代碼版本管理工具深度聯(lián)動(dòng)，系統(tǒng)可自動(dòng)關(guān)聯(lián)失敗用例與特定代碼變更，精準(zhǔn)定位問題代碼行或模塊，將調(diào)試周期從數(shù)天縮短至小時(shí)級(jí)，顯著提升驗(yàn)證迭代效率與研發(fā)信心。

AI賦能形式化驗(yàn)證

除了優(yōu)化仿真驗(yàn)證的核心流程，針對仿真難以覆蓋的復(fù)雜邊界場景與完備性驗(yàn)證需求，芯華章在形式化驗(yàn)證領(lǐng)域?qū)崿F(xiàn)了更大幅度的技術(shù)革新。

硬件模型檢測技術(shù)作為形式化驗(yàn)證的核心分支，是確保設(shè)計(jì)關(guān)鍵核心控制邏輯完備驗(yàn)證的重要手段，但面對復(fù)雜的設(shè)計(jì)和眾多的屬性與求解引擎，如何最優(yōu)調(diào)度資源成為巨大挑戰(zhàn)。

芯華章通過 AI 技術(shù)實(shí)現(xiàn)多項(xiàng)關(guān)鍵突破，全面激活形式化驗(yàn)證的高效性，增強(qiáng)新用戶導(dǎo)入形式化驗(yàn)證方法學(xué)進(jìn)行驗(yàn)證提效的信心。

最佳引擎選擇

通過對設(shè)計(jì)、屬性提取數(shù)千個(gè)特征參數(shù)，進(jìn)行離線模型訓(xùn)練與在線實(shí)時(shí)預(yù)測，為每個(gè)待驗(yàn)證屬性動(dòng)態(tài)匹配最優(yōu)底層求解引擎，顯著縮短求解時(shí)間；

屬性求解排序與分組

通過模型預(yù)測屬性求解難度，優(yōu)先攻克簡單問題，最大化有限時(shí)間內(nèi)的驗(yàn)證產(chǎn)出；同時(shí)將相似屬性分組求解，共享求解過程中的 “引理” 知識(shí)，進(jìn)一步提升整體效率；

驗(yàn)證結(jié)果預(yù)測與求解導(dǎo)向

模型可預(yù)測某個(gè)屬性成功或失敗的概率，據(jù)此智能選擇求解引擎策略，避免盲目進(jìn)行無效嘗試，浪費(fèi)計(jì)算資源；

資源需求預(yù)估

根據(jù)用戶提供的 CPU、內(nèi)存等服務(wù)器配置，預(yù)測驗(yàn)證任務(wù)能否在給定資源下完成，從而提供科學(xué)的資源規(guī)劃建議，避免算力浪費(fèi)。

這些智能化手段，使得形式化驗(yàn)證模型檢測技術(shù)煥發(fā)出新的速度和靈活性。

從 “人工苦旅” 走向 “智能生成”

SVA 編寫是硬件模型檢測中不可回避的核心難題 —— 作為形式化屬性驗(yàn)證（FPV）的關(guān)鍵載體，SVA 對確保設(shè)計(jì)正確性至關(guān)重要，但復(fù)雜時(shí)序邏輯的手工編寫耗時(shí)耗力，且易因邊界條件遺漏引發(fā)驗(yàn)證漏洞。

針對這一痛點(diǎn)，芯華章聯(lián)合中興微電子，研發(fā)基于大語言模型（LLM）的SVA生成并引入工業(yè)級(jí)創(chuàng)新評(píng)估系統(tǒng)SVAEval。用戶只需輸入自然語言描述的設(shè)計(jì)意圖，系統(tǒng)便能調(diào)用大語言模型智能體，自動(dòng)生成符合語法的SVA。

隨后，該系統(tǒng)會(huì)進(jìn)行三層自動(dòng)化校驗(yàn)：語法正確性、功能正確性以及質(zhì)量評(píng)估。我們創(chuàng)新地采用了形式化驗(yàn)證與仿真比對相結(jié)合的方式，確保生成的SVA與黃金參考等價(jià)。該框架通過迭代式提示優(yōu)化和指標(biāo)評(píng)估，顯著提升了由大型語言模型生成的 SVA 的質(zhì)量。

SVA智能小助手已成功在中興微電子落地并投入日常使用。實(shí)驗(yàn)數(shù)據(jù)顯示，pass@5較基線提升59%，復(fù)雜斷言開發(fā)效率提升40%以上，有效減輕了工程師編寫SVA的負(fù)擔(dān)，提升了驗(yàn)證代碼的產(chǎn)出效率與質(zhì)量。

未來，芯華章將持續(xù)探索“AI+EDA”創(chuàng)新路徑，與客戶共同研發(fā)適配其技術(shù)路線的驗(yàn)證方案，為客戶提供更加高效、可靠的驗(yàn)證解決方案，實(shí)現(xiàn)從需求響應(yīng)到價(jià)值共創(chuàng)的跨越。