隨著芯片設(shè)計(jì)復(fù)雜度不斷攀升，如何確保隱藏在代碼中的邏輯Bug無(wú)處遁形，成為芯片成功流片的關(guān)鍵。形式化驗(yàn)證(Formal Verification)技術(shù)通過(guò)嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)證明，在芯片設(shè)計(jì)的全部狀態(tài)空間內(nèi)進(jìn)行窮盡式分析，提供“數(shù)學(xué)確定性”的保障。這無(wú)疑是通往“零缺陷”芯片的最優(yōu)路徑。然而，形式化驗(yàn)證存在兩大難題：一是編寫驗(yàn)證規(guī)則(SVA斷言)需要極高的專業(yè)技能，二是實(shí)現(xiàn)100%的驗(yàn)證覆蓋率過(guò)程繁瑣且耗時(shí)。

近日，國(guó)內(nèi)領(lǐng)先的EDA企業(yè)上海阿卡思微電子技術(shù)有限公司(北京華大九天科技股份有限公司戰(zhàn)略參股公司)與北京開(kāi)源芯片研究院(簡(jiǎn)稱“開(kāi)芯院”)、中國(guó)科學(xué)院計(jì)算技術(shù)研究所(ICT，簡(jiǎn)稱“計(jì)算所”)合作，推出“HimaFormal MC+UCAgent智能形式化驗(yàn)證解決方案”。該方案首次將人工智能大模型智能體深度融入形式化驗(yàn)證全流程，成功打通了從“意圖描述”到“100%驗(yàn)證閉環(huán)”的最后一公里，讓原本高門檻的“數(shù)學(xué)證明”變得人人可用。 形式化驗(yàn)證是一種通過(guò)數(shù)學(xué)方法證明設(shè)計(jì)無(wú)誤的“白盒”技術(shù)，能從根源上排查風(fēng)險(xiǎn)。但在實(shí)際工程中，它長(zhǎng)期面臨兩大應(yīng)用痛點(diǎn)：

門檻高：編寫驗(yàn)證專用的SVA斷言語(yǔ)言像做“數(shù)學(xué)證明題”，極度依賴資深專家，費(fèi)時(shí)費(fèi)力。

收斂慢：確保邏輯覆蓋率達(dá)標(biāo)需要反復(fù)手工迭代，周期漫長(zhǎng)。

HimaFormal MC+UCAgent方案將阿卡思自研的HimaFormal MC形式化工具與開(kāi)芯院自主研發(fā)的UCAgent大模型智能體相結(jié)合，構(gòu)建了從“一句需求描述”到“100%驗(yàn)證覆蓋”的形式驗(yàn)證自動(dòng)化流水線。HimaFormal MC+UCAgent的核心價(jià)值在于其端到端的智能化與自動(dòng)化，它徹底重構(gòu)了傳統(tǒng)形式化驗(yàn)證的工作流。形式化驗(yàn)證的流程如下圖，左邊是典型的形式化驗(yàn)證方案，人工介入較多，右邊是HimaFormal MC+UCAgent的智能形式化驗(yàn)證方案，即從一條提示到形式化驗(yàn)證100%覆蓋率閉環(huán)，構(gòu)建了自動(dòng)化驗(yàn)證閉環(huán)，該方案中調(diào)用的模型可選通用人工智能大模型，通過(guò)MCP接口與UCAgent智能體交互運(yùn)行。

其核心工作流存在如下優(yōu)點(diǎn)：

1、智能生成：說(shuō)人話，寫斷言 用戶無(wú)需精通繁瑣的SVA語(yǔ)法，只需提供RTL設(shè)計(jì)描述或自然語(yǔ)言規(guī)范，工具便能自動(dòng)理解設(shè)計(jì)意圖，智能生成覆蓋協(xié)議、時(shí)序、仲裁等各種場(chǎng)景的SVA斷言。

2、自動(dòng)證明：嚴(yán)把關(guān)，找漏洞 生成的斷言隨即送入HimaFormal MC引擎進(jìn)行嚴(yán)格的數(shù)學(xué)推理與窮舉證明。工具將在全狀態(tài)空間內(nèi)自動(dòng)探索，判定斷言通過(guò)與否，一旦失敗即刻生成反例激勵(lì)。

3、精準(zhǔn)診斷：看得懂，改得快 針對(duì)出錯(cuò)場(chǎng)景，工具充當(dāng)了“翻譯官”與“分析師”，自動(dòng)解析錯(cuò)誤信息、定位問(wèn)題根因，并以通俗易懂的語(yǔ)言提示工程師修改方向，告別傳統(tǒng)調(diào)試的盲目性。

4、迭代收斂：掃盲區(qū)，全覆蓋 UCAgent智能體分析COI(Cone-of-Influence，邏輯影響錐)覆蓋率數(shù)據(jù)，自動(dòng)識(shí)別未被覆蓋的邏輯盲區(qū)，并針對(duì)性地補(bǔ)充新斷言。這一過(guò)程將自動(dòng)循環(huán)迭代，直至達(dá)成100%可證明COI覆蓋率，確保驗(yàn)證不留死角。此外，針對(duì)ProofCore的覆蓋率數(shù)據(jù)分析功能也將推出。

5、價(jià)值落地：降門檻，提效能 該方案為芯片設(shè)計(jì)企業(yè)帶來(lái)了四重核心價(jià)值：

人人可用：告別晦澀的SVA語(yǔ)法，通過(guò)自然語(yǔ)言交互讓形式化驗(yàn)證進(jìn)一步普及。

效率倍增：將原本需要數(shù)周的人工迭代工作，壓縮至數(shù)小時(shí)甚至更短。

結(jié)果可信：數(shù)學(xué)證明的確定性+AI診斷的可解釋性，雙重保障驗(yàn)證質(zhì)量。

閉環(huán)無(wú)憂：依托覆蓋率驅(qū)動(dòng)的自動(dòng)補(bǔ)全機(jī)制，實(shí)現(xiàn)功能驗(yàn)證的自動(dòng)全覆蓋。

目前，HimaFormal MC+UCAgent 智能驗(yàn)證解決方案已面向國(guó)內(nèi)芯片設(shè)計(jì)企業(yè)開(kāi)放試用，UCAgent程序代碼已在GitHub開(kāi)源。

未來(lái)，阿卡思將繼續(xù)深化AI與EDA的融合，提升 HimaFormal MC 形式化驗(yàn)證軟件的斷言屬性質(zhì)量，提高 HimaFormal EC 等價(jià)性檢查和 HimaFormal HiLEC 高階等價(jià)性檢查的調(diào)試效率，構(gòu)建全流程智能化形式驗(yàn)證生態(tài)。

關(guān)于北京開(kāi)源芯片研究院

北京開(kāi)源芯片研究院是國(guó)內(nèi)領(lǐng)先的開(kāi)源芯片研發(fā)及產(chǎn)業(yè)化推進(jìn)機(jī)構(gòu)，著力推動(dòng)RISC-V創(chuàng)新鏈與產(chǎn)業(yè)鏈的深度融合，加速科技成果落地，構(gòu)建全球領(lǐng)先的RISC-V產(chǎn)業(yè)生態(tài)。

關(guān)于中國(guó)科學(xué)院計(jì)算所

中國(guó)科學(xué)院計(jì)算技術(shù)研究所是中國(guó)科學(xué)院下屬、中國(guó)第一個(gè)專門從事計(jì)算機(jī)科學(xué)技術(shù)綜合性研究的學(xué)術(shù)機(jī)構(gòu)，成立于1956年，被譽(yù)為“中國(guó)計(jì)算機(jī)事業(yè)的搖籃”。作為我國(guó)信息技術(shù)領(lǐng)域的開(kāi)拓者和奠基人，計(jì)算所秉持“基礎(chǔ)性、戰(zhàn)略性、前瞻性”的三性原則，堅(jiān)持“四個(gè)面向”，致力于建成引領(lǐng)創(chuàng)新型戰(zhàn)略高技術(shù)研究所，保障國(guó)家信息安全，引領(lǐng)產(chǎn)業(yè)技術(shù)方向，率先成為世界一流水平的科研機(jī)構(gòu)。

關(guān)于上海阿卡思

上海阿卡思微電子技術(shù)有限公司由硅谷回國(guó)的資深電子設(shè)計(jì)自動(dòng)化(EDA)專家于2020年在上海張江高科技園區(qū)設(shè)立，旗下子公司成都奧卡思微電科技有限公司于2018年在成都高新區(qū)創(chuàng)立，公司聚集國(guó)際知名EDA公司和芯片設(shè)計(jì)公司具有多年研發(fā)經(jīng)驗(yàn)的尖端人才，基于形式化方法為邏輯芯片設(shè)計(jì)和工控軟件等提供驗(yàn)證工具及驗(yàn)證咨詢服務(wù)，憑借在形式化方法領(lǐng)域深厚的技術(shù)積累及深入的產(chǎn)品實(shí)踐，已推出多款商用性能優(yōu)異的核心驗(yàn)證工具及其他相關(guān)驗(yàn)證工具，服務(wù)于復(fù)雜芯片設(shè)計(jì)及通用設(shè)計(jì)流程，公司產(chǎn)品獲得四十余個(gè)客戶，包括國(guó)家頭部通訊、高性能計(jì)算及AI芯片企業(yè)等標(biāo)桿客戶的采購(gòu)、使用及好評(píng)。公司將緊密把握IC設(shè)計(jì)復(fù)雜度提升及驗(yàn)證方法學(xué)多樣化需求提升的趨勢(shì)，致力于成為國(guó)內(nèi)領(lǐng)先的形式化技術(shù)開(kāi)發(fā)與服務(wù)商。