模型检验及其布尔可满足问题的研究

论文题目: 模型检验及其布尔可满足问题的研究

论文类型: 博士论文

论文专业: 计算机系统结构

作者: 邵明

导师: 李晓维

关键词: 模型检验,有界模型检验,布尔可满足问题,模型的抽象和细化,极小不可满足问题

文献来源: 中国科学院研究生院（计算技术研究所）

发表年度: 2005

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

论文目录:

中文摘要

英文摘要

插图目录

第一章 引 言

1.1 形式化验证方法

1.2 本文研究背景及相关工作

1.2.1 符号模型检验

1.2.2 模型检验与布尔可满足问题

1.2.2.1 有界模型检验

1.2.2.2 求解布尔可满足问题

1.2.2.3 模型抽象细化技术与提取不可满足问题核

1.3 本文主要工作

1.4 本文章节安排

第二章符号模型检验中转移关系的分组策略

2.1 有限状态转移模型

2.2 时态逻辑

2.2.1 计算树逻辑公式（CTL）

2.2.2 其它时态逻辑

2.3 满足时态逻辑公式状态集合的不动点表征

2.4 布尔函数的支撑变量

2.5 二叉决策图

2.6 二叉决策图的节点与支撑向量

2.7 基于支撑向量海明距离的转移关系分组策略

2.8 实验结果分析

2.9 本章小结

第三章模型检验与布尔可满足问题

3.1 布尔可满足问题

3.2 有界模型检验的例子

3.3 有界模型检验

3.4 有界模型检验的完全性问题

3.5 模型的抽象和细化技术

3.5.1 模型的抽象方法

3.5.1.1 基于实存的抽象方法

3.5.1.2 基于影响锥的抽象

3.5.1.3 谓词抽象

3.5.2 伪反例的识别

3.5.3 基于极小不可满足问题的抽象细化

3.6 本章小结

第四章布尔可满足问题的求解

4.1 DPLL算法

4.1.1 基于分解的算法及其复杂度

4.1.2 DPLL算法

4.1.3 分支的启发式策略以及布尔传播过程

4.1.4 冲突分析

4.2 调查传播算法

4.2.1 合取范式的因子图表示

4.2.2 调查传播算法

4.2.3 调查传播算法的迭代

4.2.4 按照赋值倾向进行变量赋值

4.2.5 转入局部搜索算法的判据

4.2.6 随机行走算法

4.2.7 调查传播算法的收敛问题

4.2.8 步长对调查传播算法的影响规律探析

4.2.8.1 步长对算法效率影响的模拟实验

4.2.8.2 步长对算法有效性影响的模拟实验

4.2.8.3 步长对调查传播算法的影响规律

4.3 本章小结

第五章 极小布尔不可满足问题

5.1 引言

5.2 识别MU的算法

5.3 提取MU子式的算法

5.3.1 提取MU子式的自适应搜索算法

5.3.2 利用蕴含图的近似提取算法

5.3.3 利用蕴含图提取MU的算法误差模拟实验

5.3.4 AMUSE方法

5.4 提取MU的精确算法

5.4.1 利用线性规划的提取算法

5.4.2 遍历子句的算法及预先局部赋值优化策略

5.5 本章小结

第六章可满足问题在测试端口序故障中的应用

6.1 端口序故障模型

6.2 利用可满足问题检测端口序故障

6.3 实验结果

6.4 本章小结

第七章 结论与未来工作

7.1 本文工作总结

7.2 存在的问题和未来工作

参考文献

致谢

作者简历

发布时间: 2006-12-27

参考文献

• [1].面向数据安全的形式化验证可满足问题研究[D]. 秦莹.国防科学技术大学2016
• [2].基于生化反应的典型约束可满足问题求解算法研究[D]. 吴帆.湖南大学2017

相关论文

• [1].面向UML的模型检验研究[D]. 董威.中国人民解放军国防科学技术大学2002
• [2].并发系统的模型检测与测试[D]. 吴鹏.中国科学院研究生院（软件研究所）2005
• [3].超大规模集成电路形式验证的方法研究[D]. 卢永江.浙江大学2005
• [4].可满足性问题算法研究以及在时序电路等价验证中的应用[D]. 丁敏.复旦大学2005
• [5].集成电路寄存器传输级故障模型与测试生成研究[D]. 杨修涛.中国科学院研究生院（计算技术研究所）2006
• [6].模拟验证中的激励产生与覆盖评估[D]. 鲁巍.中国科学院研究生院（计算技术研究所）2006
• [7].数字电路测试压缩方法研究[D]. 韩银和.中国科学院研究生院（计算技术研究所）2005
• [8].集成电路的逻辑等价性验证研究[D]. 杨军.浙江大学2007

标签：模型检验论文;  有界模型检验论文;  布尔可满足问题论文;  模型的抽象和细化论文;  极小不可满足问题论文;