作为形式验证的重要方法,模型检验在VLSI/SOC设计的功能验证中发挥着越来越重要的作用。在模型检验中,设计被抽象为有限状态转移模型(或者Kripke结构),而所要验证的属性用时态逻辑来表达。通过检验模型是否符合特定的时态属性来对设计进行验证。对模型检验而言,状态空间随状态变量的数目成指数倍增长是阻碍它应用到工业界的根本困难所在。为了缓解甚至克服这种窘境,研究人员已经提出了许多方法。比如,利用二叉决策图的各种优化变种表示模型的转移关系和状态空间;把验证任务转化为布尔可满足问题(SAT);以及对原始模型进行合适的抽象和细化等。在该研究背景下,本文所考察的关键问题是:如何构建紧致且高效的转移关系;如何快速提取极小布尔不可满足子式;求解SAT的调查传播算法对参数步长敏感的问题。针对这些问题,本文做出的贡献和创新点如下:1.针对符号模型检验中如何构建紧致且高效的转移关系问题,提出了对分割的转移关系进行重新分组的有效方法。转移关系的构建是符号模型检验的重要环节,该分组算法充分利用了转移关系各分割部分支撑向量所具有的组块特征,当转移关系各部分的支撑向量差别不大时,就将它们分为一组。分组算法的优点体现在两方面:其一,能够构建紧致的转移关系,通过对基准电路集ISCAS-89中符合条件的实例进行的实验表明,转移关系的大小能够减少约30%～10%。其中转移关系的大小是由表示它的BDD节点数目来衡量。其二,分组的方案减少了求解状态像的运算步骤。2.针对如何快速提取极小布尔不可满足子式的问题,提出了对基于遍历子句的精确提取算法进行预先赋值的优化方案。在基于抽象和细化的模型检验中,提取极小不可满足问题是关键。遍历子句的算法通过逐一判断每个子句的取舍来求解极小不可满足子式,本文优化方案通过对某些变量进行预先赋值,简化了判断子句取舍的计算任务。其优点体现在两方面:其一,作为一种优化方案,提高了算法效率,对SATLIB中的实例进行的实验表明,在求解这些实例时,算法的运算时间能够获得约60%～10%的减少。其二,预先赋值不影响在判断子句取舍时所产生问题的可满足性,这就与原来的遍历子句算法相等价,因此能够获得相同的子式。3.针对求解SAT的调查传播算法对参数步长敏感的问题,探析了步长对算法有效性和效率的影响规律。所谓步长是指每次迭代后被赋值的变量个数。通过对SATLIB中基准实例所进行的实验可以看到,随着步长的增加,算法的有效性和效率体现出此消彼长的规律。该规律为合理利用该算法具有重要的参考价值。