EDA形式验证中可满足性(SAT)问题的算法研究

随着集成电路设计规模和复杂性的增加，验证成为设计的瓶颈。而依靠测试向量的模拟验证方法远远不能满足大规模设计验证的需求。具有完备特性的形式化方法成为验证的一个重要选择，但目前只能在用户不断的干预下解决小规模的验证问题。在本项目中，我们将针对集成电路验证问题规模大的特点和EDA验证工具自动化的需求，研究形式化验证中的核心问题-SAT算法。首先，研究SAT问题的变量类型和高效预处理方法，建立一个能够产生"多米诺骨牌效应"的不断简化的，结合多种预处理技术的高效预处理器，目的是在初始阶段减小问题的规模和难度。其次，在求解过程中，通过研究学习子句的空间有效性，及时动态地删除冗余学习子句来控制问题规模的增加，避免解决器因为内存爆炸而得不到解。最后，我们将利用SAT解决器解决大规模设计验证过程中的等价性验证和模型检验问题。