CCF中國(guó)軟件大會(huì)

芯華章GalaxFV融合AI，構(gòu)建覆蓋多個(gè)芯片驗(yàn)證場(chǎng)景的形式化驗(yàn)證APP矩陣，在國(guó)內(nèi)頭部GPGPU、車規(guī)芯片等多個(gè)行業(yè)核心項(xiàng)目中落地。

本次受中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)邀請(qǐng)，在中國(guó)軟件大會(huì)上圍繞形式化驗(yàn)證分享GalaxFV模型檢測(cè)解決方案及成功案例。

“驗(yàn)證周期能不能再壓一壓”

“怎么才能更早地發(fā)現(xiàn)bug”

“門(mén)檻太高難上手”

這些看似直白的訴求背后，藏著的其實(shí)是驗(yàn)證工作的核心矛盾——

不是單純追求“快”，而是要“快且全”;不是盲目壓縮時(shí)間，而是要把精力用在有效驗(yàn)證上;不是被動(dòng)應(yīng)對(duì)復(fù)雜設(shè)計(jì)，而是要找到適配場(chǎng)景的精準(zhǔn)解法。

當(dāng)用戶糾結(jié)于“如何提高效率”“如何降低風(fēng)險(xiǎn)”時(shí)，本質(zhì)上是在問(wèn)：有沒(méi)有一套方案，能真正解決驗(yàn)證中的無(wú)效內(nèi)耗、早期bug難發(fā)現(xiàn)、復(fù)雜場(chǎng)景搞不定的痛點(diǎn)?

相較于傳統(tǒng)仿真驗(yàn)證，形式化驗(yàn)證能夠“窮盡式覆蓋+早期介入”，是一種非常完備的驗(yàn)證方法，但落地難點(diǎn)在于“工具易用性、場(chǎng)景適配性、效率平衡”。

芯華章科技基于Model Checking的形式驗(yàn)證解決方案，從“可落地性、完備性、高效性”出發(fā)，為芯片設(shè)計(jì)企業(yè)、驗(yàn)證團(tuán)隊(duì)提供一套既能破解瓶頸，又能快速落地的驗(yàn)證方案。

為什么選擇形式化驗(yàn)證

驗(yàn)證完備性：窮盡所有狀態(tài)空間，精準(zhǔn)捕捉并發(fā)邏輯等復(fù)雜場(chǎng)景下的高風(fēng)險(xiǎn) bug

早期問(wèn)題排查：無(wú)需等待系統(tǒng)全串聯(lián)，在芯片設(shè)計(jì)驗(yàn)證早期即可定位并解決問(wèn)題，大幅縮短研發(fā)周期

便捷高效部署：無(wú)需人工構(gòu)建激勵(lì)，通過(guò)約束(Assume)自動(dòng)生成激勵(lì)，結(jié)合 SVA 斷言檢測(cè)、自動(dòng)覆蓋率收集，快速搭建驗(yàn)證環(huán)境

快速 bug 定位：Cycle by Cycle遍歷狀態(tài)空間，可輸出最短錯(cuò)誤路徑，解決傳統(tǒng)仿真 “難定位、慢排查” 的痛點(diǎn)

高可復(fù)用性：基于模塊功能設(shè)計(jì)驗(yàn)證平臺(tái)，可跟隨 RTL 模型迭代復(fù)用，無(wú)需重復(fù)搭建測(cè)試平臺(tái)，提升驗(yàn)證復(fù)用效率

GalaxFV 場(chǎng)景化APP矩陣精準(zhǔn)匹配驗(yàn)證需求

時(shí)序等價(jià)性驗(yàn)證：SEC APP

解決時(shí)序優(yōu)化、功耗優(yōu)化、流水線重構(gòu)后的時(shí)序一致性驗(yàn)證問(wèn)題，無(wú)需檢查中間狀態(tài)，也無(wú)需依賴綜合工具提供比較點(diǎn)信息。

大規(guī)模連接性校驗(yàn)：CC APP

針對(duì)信號(hào)預(yù)留穿線場(chǎng)景，檢測(cè)預(yù)留的連接是否正確;選擇器模塊中不同片選信號(hào)對(duì)應(yīng)連通正確性檢測(cè);constant、reset/clock以及Debug信號(hào)連接正確性檢測(cè)。

覆蓋率收斂加速：FRC APP

聯(lián)合芯華章GalaxSim，讀取 GalaxSim生成的XCOVDB 覆蓋率數(shù)據(jù)庫(kù)，檢查(check)無(wú)法到達(dá)(unreachable)的狀態(tài)空間，自動(dòng)剔除設(shè)計(jì)中完全不可達(dá)的狀態(tài)空間，聚焦有效覆蓋場(chǎng)景，大幅提升仿真覆蓋率收斂速度，破解傳統(tǒng)仿真 “60% 后覆蓋率難收斂” 瓶頸。

大模型SVA自動(dòng)化校驗(yàn)：SVAC APP

與中興微電子、國(guó)創(chuàng)中心聯(lián)合研發(fā)，通過(guò)SVAC評(píng)估大語(yǔ)言模型生成的SVA 與自然語(yǔ)言描述的設(shè)計(jì)要求是否一致，提升大語(yǔ)言模型生成SVA的質(zhì)量，大幅減少驗(yàn)證工程師耗時(shí)耗力的SVA編寫(xiě)工作。

早期X態(tài)傳播檢測(cè)：X-PROP APP

用于芯片設(shè)計(jì)迭代早期，檢查迭代過(guò)程中出現(xiàn)的X態(tài)。可精準(zhǔn)檢測(cè) DUT 內(nèi)部(未初始化寄存器、多驅(qū)信號(hào)等)產(chǎn)生及外部傳入的 X 態(tài)傳播，提前規(guī)避 X 態(tài)傳播導(dǎo)致的后期設(shè)計(jì)異常。

多場(chǎng)景案例落地分享

芯華章形式化驗(yàn)證工具GalaxFV解決方案已在國(guó)內(nèi)頭部芯片企業(yè)、車規(guī)芯片、GPGPU等多個(gè)核心項(xiàng)目中落地。

解決超大規(guī)模驗(yàn)證平臺(tái)約束沖突

項(xiàng)目痛點(diǎn)：某客戶模塊A出現(xiàn)大規(guī)模(1000+條)約束沖突，某國(guó)際主流工具無(wú)法排查，驗(yàn)證進(jìn)度阻塞;模塊C驗(yàn)證證明耗時(shí)太長(zhǎng)，一次回歸需要32個(gè)小時(shí)。

落地效果：通過(guò)與客戶合作開(kāi)發(fā)出約束沖突查找功能，且進(jìn)行工具化，有效提高回歸效率，模塊A最終在30分鐘內(nèi)完成約束沖突排查;通過(guò)優(yōu)化模型+定制引擎等方式，將模塊C的證明時(shí)間縮短到了15個(gè)小時(shí)。

車規(guī)芯片高復(fù)雜度驗(yàn)證

項(xiàng)目痛點(diǎn)：某新能源汽車車規(guī)芯片，算法邏輯復(fù)雜、狀態(tài)空間巨大，數(shù)據(jù)位寬大，壓縮算法證明收斂難度高，某國(guó)際主流工具耗時(shí)30小時(shí)仍有8條property無(wú)法證明。

落地效果：基于高性能自適應(yīng)引擎調(diào)度系統(tǒng)，對(duì)property自動(dòng)分組與排序，同時(shí)GalaxFV基于字級(jí)模型建模在處理復(fù)雜運(yùn)算相關(guān)數(shù)據(jù)通路具備巨大優(yōu)勢(shì)，最終GalaxFV FPV 2小時(shí)內(nèi)完成全部Property證明，結(jié)果正確，工具功能正確。

路由模塊數(shù)據(jù)一致性驗(yàn)證

項(xiàng)目痛點(diǎn)：某客戶路由模塊，需通過(guò)scoreboard檢測(cè)數(shù)據(jù)一致性;對(duì)于部分property，第三方工具僅能完成有界證明(Bounded Proof)，存在潛在風(fēng)險(xiǎn)。

落地效果：實(shí)現(xiàn)100%完全證明(Full Proof)收斂，性能與第三方工具持平;其中通過(guò)引擎定制優(yōu)化，將88個(gè)有界證明的Property變成完全證明。

芯華章科技始終以解決客戶實(shí)際痛點(diǎn)為核心，未來(lái)，我們將持續(xù)優(yōu)化工具的易用性與場(chǎng)景適配性，完善COI及Formal Core覆蓋率分析、加速證明收斂、強(qiáng)化sign-off流程等核心能力，進(jìn)一步降低形式驗(yàn)證的落地門(mén)檻，助力更多驗(yàn)證團(tuán)隊(duì)突破驗(yàn)證瓶頸。