可满足性问题及等价性验证关键技术及平台

项目简介

可满足性问题(SAT)是计算机科学和数理逻辑的核心问题之一，作为核心推理引擎被应用于电子设计自动化(EDA)领域中的多个环节，而逻辑等价性验证（LEC）问题则为EDA的一个经典且有关键应用的问题。产业升级和技术进步带来了超大规模的问题和更复杂的难题，对SAT求解器和LEC证明器的拓展能力和求解速度提出了更高的挑战。

可满足性问题及等价性验证关键技术及平台以形式化验证能力、难题的求解能力、分布式并行的适配能力等方面出发，建立了一套可靠、高性能、高拓展性的SAT和LEC系统平台。具有如下特色：

一．混合求解。针对SAT问题，设计了一套以系统搜索为主体，局部搜索辅助进行空间采样的深度混合求解技术，两类算法会定期执行深度的信息交互；针对领域中难以验证的数据通路电路的LEC问题，提出了一种基于多引擎的扫描验证算法，并可以根据子电路区域的特征，在验证局部区域时，动态选择采用SAT求解器或者完备仿真器来进行验证。相关技术大幅提高了验证工具在不同问题上的验证能力和实用性。

二．分布式求解。本平台基于随机初始搜索序扰动技术和线程间子句交互技术，提出了一套分布式SAT求解框架，可以快速适配于任意核心数目下问题的求解，拓展能力强，相比已有公开技术，本技术大幅度求解速度和复杂实例的求解能力。基于相关技术研制的LEC验证工具，可以快速验证许多主流开源工具甚至国内外商用工具难以验证的数据通路电路的等价性难题。

相关技术获发表高水平论文发表高水平学术论文10余篇、专利和软件著作权2项。相关技术于国际SAT比赛、FLoC奥林匹克竞赛获得冠军10余项。在可满足性领域旗舰会议SAT（国际可满足性测试理论及应用大会）荣获最佳论文奖。相关成果已服务于多家头部EDA企业，并成功赋能了军工、金融等领域。

 

技术成熟度：中试