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