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 产品和解决方案，助力集成电路产业攻克复杂设计挑战，为全球半导体行业的发展贡献中国智慧和中国方案。