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