CCF中國軟件大會

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

本次受中國計算機學會(CCF)邀請，在中國軟件大會上圍繞形式化驗證分享GalaxFV模型檢測解決方案及成功案例。

“驗證周期能不能再壓一壓”

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

“門檻太高難上手”

這些看似直白的訴求背后，藏著的其實是驗證工作的核心矛盾——

不是單純追求“快”，而是要“快且全”;不是盲目壓縮時間，而是要把精力用在有效驗證上;不是被動應對復雜設計，而是要找到適配場景的精準解法。

當用戶糾結于“如何提高效率”“如何降低風險”時，本質上是在問：有沒有一套方案，能真正解決驗證中的無效內耗、早期bug難發(fā)現(xiàn)、復雜場景搞不定的痛點?

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

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

為什么選擇形式化驗證

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

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

便捷高效部署：無需人工構建激勵，通過約束(Assume)自動生成激勵，結合 SVA 斷言檢測、自動覆蓋率收集，快速搭建驗證環(huán)境

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

高可復用性：基于模塊功能設計驗證平臺，可跟隨 RTL 模型迭代復用，無需重復搭建測試平臺，提升驗證復用效率

GalaxFV 場景化APP矩陣精準匹配驗證需求

時序等價性驗證：SEC APP

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

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

針對信號預留穿線場景，檢測預留的連接是否正確;選擇器模塊中不同片選信號對應連通正確性檢測;constant、reset/clock以及Debug信號連接正確性檢測。

覆蓋率收斂加速：FRC APP

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

大模型SVA自動化校驗：SVAC APP

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

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

用于芯片設計迭代早期，檢查迭代過程中出現(xiàn)的X態(tài)?？删珳蕶z測 DUT 內部(未初始化寄存器、多驅信號等)產生及外部傳入的 X 態(tài)傳播，提前規(guī)避 X 態(tài)傳播導致的后期設計異常。

多場景案例落地分享

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

解決超大規(guī)模驗證平臺約束沖突

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

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

車規(guī)芯片高復雜度驗證

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

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

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

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

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

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