第三屆設(shè)計(jì)自動(dòng)化產(chǎn)業(yè)峰會(huì)（IDAS）圓滿落幕，在活動(dòng)期間工業(yè)和信息化部電子信息司副司長(zhǎng)王世江一行蒞臨芯華章展臺(tái)視察指導(dǎo)。

芯華章科技聯(lián)席CEO齊正華全程接待，并圍繞公司產(chǎn)品最新進(jìn)展及核心技術(shù)展開(kāi)詳細(xì)介紹，全面展現(xiàn)芯華章在EDA驗(yàn)證領(lǐng)域的深耕成果與創(chuàng)新方向。

同期，芯華章受邀參與數(shù)字芯片論壇分享——以形式化驗(yàn)證技術(shù)創(chuàng)新為核心，介紹芯華章GalaxEC HEC高階等價(jià)性檢查工具如何提升芯片驗(yàn)證效率，同時(shí)首發(fā)新品RV-APP(RISC-V指令級(jí)C++模型套件)，以“標(biāo)準(zhǔn)化、自動(dòng)化”填補(bǔ)產(chǎn)業(yè)標(biāo)準(zhǔn)驗(yàn)證資源空白。

在AI芯片定制越來(lái)越流行的時(shí)代，設(shè)計(jì)者為了提高計(jì)算效率、支持特定應(yīng)用需求（如浮點(diǎn)運(yùn)算、AI算子等），往往會(huì)對(duì)傳統(tǒng)處理器指令（如RISC-V）進(jìn)行擴(kuò)展定制，增加特定的硬件指令。

這種定制化設(shè)計(jì)雖然可以顯著提升芯片性能，但也帶來(lái)了設(shè)計(jì)復(fù)雜性和驗(yàn)證的挑戰(zhàn)。芯華章研發(fā)經(jīng)理林韜博士指出，在大位寬數(shù)據(jù)通路設(shè)計(jì)驗(yàn)證流程中，傳統(tǒng)仿真方案存在完備性不足、收斂效率低下、邊界場(chǎng)景激勵(lì)構(gòu)建困難三大瓶頸。

芯華章GalaxEC HEC高階等價(jià)性檢查工具并非對(duì)傳統(tǒng)驗(yàn)證方案的局部?jī)?yōu)化，而是從驗(yàn)證邏輯根源出發(fā)，以形式化驗(yàn)證算法創(chuàng)新為核心，形成兼具“完備性、效率、易用性”的一體化解決方案：

打破時(shí)序綁定

專注事務(wù)級(jí)/算法級(jí)等價(jià)性驗(yàn)證

無(wú)需“逐時(shí)鐘等價(jià)比對(duì)”，聚焦算法本質(zhì)一致性，支持C++/C/RTL跨語(yǔ)言、同語(yǔ)言對(duì)比及高級(jí)綜合正確性驗(yàn)證；

C++模型語(yǔ)法支持度高，可將C/C++代碼轉(zhuǎn)換為形式化模型，且支持ANSI C++17標(biāo)準(zhǔn)，支持指針?biāo)阈g(shù)/內(nèi)存讀寫(xiě)；

工具會(huì)自動(dòng)生成C++運(yùn)行時(shí)安全檢查引理（例如數(shù)組越界、除零等）并進(jìn)行自動(dòng)化完備性檢查，保障C/C++參考模型質(zhì)量。

自研引擎+加速技術(shù)

打破收斂瓶頸

在數(shù)據(jù)通路繁重的大位寬電路設(shè)計(jì)過(guò)程中，驗(yàn)證收斂是最大的難題之一，為突破這一難題，GalaxEC HEC工具做了兩大核心設(shè)計(jì)：

通過(guò)“Case拆分+多引擎協(xié)同”，將例如64位浮點(diǎn)乘法、除法等復(fù)雜任務(wù)自動(dòng)完備地拆分為子任務(wù)進(jìn)行并行驗(yàn)證，各引擎實(shí)時(shí)交互實(shí)現(xiàn)“1+1>2”協(xié)同效應(yīng)，目前已實(shí)現(xiàn)整數(shù) / 浮點(diǎn)乘法, 除法和乘累加、各類加解密算法、超越函數(shù)等典型算子的快速收斂。

創(chuàng)新性的“No-Spec”模式，無(wú)需依賴算法參考模型，可直接通過(guò)GalaxEC HEC工具開(kāi)放接口構(gòu)造RTL實(shí)現(xiàn)的算法范式并進(jìn)行快速證明；結(jié)合引擎優(yōu)化技術(shù)，在客戶真實(shí)設(shè)計(jì)中，將Int64類型MAC算子從“24小時(shí)無(wú)法證明收斂”提升至60秒內(nèi)完備驗(yàn)證。

通過(guò)以上加速技術(shù)，GalaxEC HEC在客戶端已實(shí)現(xiàn)64位雙精度浮點(diǎn)乘法200秒完備證明、8位無(wú)符號(hào)類型向量點(diǎn)乘5小時(shí)內(nèi)完成驗(yàn)收收斂，效率超傳統(tǒng)工具10倍。

深度融合Fusion Debug

提升調(diào)試效率

通過(guò)與芯華章Fusion Debug深度融合，Debug流程得以簡(jiǎn)化，雙擊引理驗(yàn)證失敗告警標(biāo)志，即可一鍵式自動(dòng)生成波形，并并列式展示C++/RTL源碼對(duì)比界面。

這使得問(wèn)題定位時(shí)間從小時(shí)級(jí)壓縮至分鐘級(jí)，大幅減少了繁雜的調(diào)試和根因定位工作。

在客戶項(xiàng)目中，GalaxEC HEC工具價(jià)值也得到進(jìn)一步實(shí)證：

在某大型CPU芯片設(shè)計(jì)客戶的40+算子驗(yàn)證項(xiàng)目（含30+浮點(diǎn)算子）中，GalaxEC HEC精準(zhǔn)捕捉傳統(tǒng)仿真難以正向構(gòu)建的“超越函數(shù)邊界場(chǎng)景計(jì)算bug”，補(bǔ)齊驗(yàn)證漏洞；后續(xù)9倍規(guī)模算子驗(yàn)證項(xiàng)目中，在未增人員的情況下同周期完成驗(yàn)證，支撐芯片按期流片。

對(duì)客戶而言，GalaxEC HEC的價(jià)值不僅是效率提升，更在于風(fēng)險(xiǎn)可控，為芯片質(zhì)量提供長(zhǎng)線保障。

針對(duì)RISC-V“標(biāo)準(zhǔn)模型缺失、激勵(lì)開(kāi)發(fā)成本高”痛點(diǎn)，芯華章發(fā)布RV-APP（RISC-V指令級(jí)C++標(biāo)準(zhǔn)模型套件），以“標(biāo)準(zhǔn)化、自動(dòng)化”填補(bǔ)行業(yè)空白：

功能上，可在數(shù)學(xué)層面證明C++模型與RTL實(shí)現(xiàn)100%算法等價(jià)；

技術(shù)上，RV-APP所提供的標(biāo)準(zhǔn)模型是經(jīng)過(guò)形式化完備驗(yàn)證、符合RISC-V標(biāo)準(zhǔn)的指令級(jí)C++行為級(jí)模型；

效率上，無(wú)需編寫(xiě)定制隨機(jī)激勵(lì)，可自動(dòng)化完成全指令集驗(yàn)證，將指令驗(yàn)證時(shí)間壓縮60%以上；

生態(tài)上，已覆蓋RV32I、RV64I等主流指令集，持續(xù)迭代標(biāo)準(zhǔn)模型，并為復(fù)雜定制指令提供專項(xiàng)驗(yàn)證服務(wù)。

從GalaxEC HEC工具破解傳統(tǒng)驗(yàn)證困局，到RV-APP錨定RISC-V產(chǎn)業(yè)未來(lái)發(fā)展方向，芯華章始終以“技術(shù)深耕”為核心——憑借可落地、可量化的方案解決工程師當(dāng)下痛點(diǎn)。 在芯片研發(fā)“效率與質(zhì)量并重”的時(shí)代，我們將持續(xù)以踏實(shí)的技術(shù)實(shí)力，為用戶提供更多差異化的解決方案。