ISEDA 2025 | 國微芯聚焦形式化驗證難題，創(chuàng)新性提出ITE-PBA 框架
2025年5月12日，ISEDA 2025會議在香港圓滿落幕。來自全球的頂尖學(xué)者、技術(shù)專家和企業(yè)代表齊聚一堂，圍繞電子設(shè)計自動化領(lǐng)域的前沿技術(shù)、發(fā)展趨勢和產(chǎn)業(yè)生態(tài)展開深入交流，共同為集成電路產(chǎn)業(yè)的創(chuàng)新發(fā)展出謀劃策。國微芯作為國產(chǎn) EDA 行業(yè)的杰出代表，受邀參加了此次盛會。在會議中，國微芯技術(shù)人員發(fā)表了題為《ITE-PBA: A Framework for SMT Solving with If-Then-Else Terms Control Flow and Parallel Branching Assignment in Formal Verification》的演講，展示了國微芯在SMT求解器領(lǐng)域的最新研究成果。
此次演講聚焦于 ITE-PBA 框架，國微芯技術(shù)人員詳細(xì)闡述了如何通過ITE的控制流信息優(yōu)化決策順序，以及如何利用并行分支賦值策略提升求解效率，為集成電路形式化驗證提供了一種創(chuàng)新性的解決方案。
隨著集成電路復(fù)雜度的指數(shù)級增長，傳統(tǒng)驗證方法已難以應(yīng)對海量狀態(tài)空間的爆炸式擴(kuò)展。形式驗證作為一種數(shù)學(xué)嚴(yán)謹(jǐn)?shù)尿炞C手段，成為確保芯片功能正確性的關(guān)鍵技術(shù)。國微芯憑借深厚的技術(shù)積累和對行業(yè)痛點的精準(zhǔn)把握，提出了ITE-PBA框架，這一創(chuàng)新性解決方案包含兩大核心技術(shù)：基于 If-Then-Else（ITE）控制流的決策順序優(yōu)化以及并行分支賦值策略。
決策優(yōu)化：挖掘控制流信息
在決策順序優(yōu)化方面，ITE-PBA 深度挖掘 ITE 的結(jié)構(gòu)特性，通過引入控制變量樹、控制“變量森林”和控制深度等創(chuàng)新性概念，優(yōu)先處理高層級的控制變量，并賦予同層級控制變量更高的優(yōu)先級。
這種基于控制流信息的決策順序優(yōu)化，能夠顯著減少后續(xù)搜索空間，極大提升了求解效率。實驗數(shù)據(jù)顯示，與傳統(tǒng)求解器相比，ITE-PBA 在處理 ITE 密集型問題時，性能提升高達(dá) 1.26 倍，展現(xiàn)出其在解決復(fù)雜硬件驗證任務(wù)中的強(qiáng)大優(yōu)勢。
并行賦值：拓展求解路徑
為應(yīng)對不同分支賦值方案在復(fù)雜場景下的局限性，國微芯在 ITE-PBA 框架中引入了并行分支賦值策略。該策略巧妙地利用多核系統(tǒng)的并行計算能力，同時執(zhí)行多個主流的分支賦值方案，實現(xiàn)了對不同搜索路徑的同步探索。
這種創(chuàng)新性的并行探索機(jī)制，極大地提高了找到有效解決方案的可能性，為 SMT 求解器在面對多樣化問題時提供了更靈活、高效的求解路徑。實驗結(jié)果有力地證明了這一策略的有效性，在多個基準(zhǔn)測試中，速度提升因素在1.04到60.98倍之間，展現(xiàn)出其卓越的性能表現(xiàn)。
實驗驗證：展現(xiàn)卓越性能
國微芯在 Yices2 求解器的基礎(chǔ)上實現(xiàn)了 ITE-PBA 框架，并對其進(jìn)行了全面的實驗評估。實驗結(jié)果令人矚目，ITE-PBA 框架在標(biāo)準(zhǔn)基準(zhǔn)測試中相較于原 Yices2 求解器實現(xiàn)了9.46倍的速度提升。在非遞增基準(zhǔn)測試中，其性能優(yōu)勢更為顯著，分別實現(xiàn)了對 Yices2 和 Yices2-ITE 的13.93倍和8.46倍速度提升，整體性能提升達(dá)9.49倍。
這一成果體現(xiàn)了ITE-PBA框架的性能優(yōu)勢，為集成電路形式化驗證領(lǐng)域提供了新的參考，對推動整個行業(yè)向更高效、更智能的驗證流程發(fā)展具有潛在的積極作用。
國微芯深知，集成電路產(chǎn)業(yè)的發(fā)展離不開產(chǎn)業(yè)鏈上下游企業(yè)的緊密合作。通過積極參與行業(yè)會議和技術(shù)交流活動，國微芯不斷加強(qiáng)與學(xué)術(shù)界、工業(yè)界以及各類科研機(jī)構(gòu)的溝通與協(xié)作。此次在 ISEDA 2025 會議上的成果展示，再次彰顯了國微芯在 EDA 領(lǐng)域的深厚技術(shù)實力和創(chuàng)新能力。
國微芯將繼續(xù)以技術(shù)創(chuàng)新為驅(qū)動，以客戶需求為導(dǎo)向，不斷推出更具競爭力的 EDA 產(chǎn)品和解決方案，助力集成電路產(chǎn)業(yè)攻克復(fù)雜設(shè)計挑戰(zhàn)，為全球半導(dǎo)體行業(yè)的發(fā)展貢獻(xiàn)中國智慧和中國方案。
