基于可满足性问题解算器的有界模型检验——子句规则和冲突分析研究

作     者：尹文波 

作者单位：复旦大学 

学位级别：硕士

导师姓名：周电

授予年度：2007年

学科分类：080903[工学-微电子学与固体电子学] 0809[工学-电子科学与技术（可授工学、理学学位）] 08[工学] 

主      题：有界模型检验 子句规则 冲突分析 集成电路设计 时序电路 SAT解算器 

摘      要：随着集成电路设计和制造技术的不断进步，电路的规模也在不断增大，电路验证和测试领域面临着前所未有的挑战。传统的基于模拟的验证方法不能满足电路复杂度增大的需要，具有完备性特点的形式化验证方法开始得到人们的关注，成为当前的研究热点。\n 本文研究工作是针对时序电路的有界模型检验进行展开的。由于近些年来，对可满足性问题(SAT)的研究取得了重大进展，有效的SAT解算器诸如zChaff、BerkMin和MiniSat等已经可以在一定时间内解决数十万变量规模的SAT问题，并且作为一个优秀的计算引擎在集成电路验证领域有着广泛的应用。本文分析了有界模型检验在子句规则和冲突分析上的优缺点，并提出了改进的方法，能够加速有界模型检验的执行。\n 本文主要的创新之处在于：(1)对重命名子旬规则进行了改进，引入了逻辑化简、处理多元运算、合并相邻结点等方法，减小了输入到SAT解算器的问题规模，有效的提高了有界模型检验的执行效率。(2)分析了有界模型检验问题冲突蕴涵图的特征，引入辅助学习子句的概念，根据蕴涵图的结构和形状生成辅助学习子句，阻止类似的冲突再次发生，有效的减少了蕴涵图的深度和冲突次数，提高有界模型检验的执行效率。对大量测试电路进行实验的结果表明了这些改进策略的有效性。