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