学位论文 > 优秀研究生学位论文题录展示

应用于集成电路形式化验证的SAT算法研究

作　者: 王霄维
导　师: 陈戈珩
学　校: 长春工业大学
专　业: 信号与信息处理
关键词: 集成电路形式验证等价性验证可满足性布尔推理 DPLL
分类号: TN402
类　型: 硕士论文
年　份: 2010年
下　载: 30次
引　用: 1次
阅　读: 论文下载

内容摘要

设计验证是集成电路设计流程中的重要组成部分。随着设计规模的增长,系统的功能越来越复杂,传统的模拟验证方法已不能满足设计的需要,形式验证方法越来越引起人们的重视。电路的等价性验证是形式验证的一个重要方法,它的主要功能是验证电路的两种不同描述之间的功能等价性。基本上所有电路等价性问题的判断都能抽象成为可满足性问题(Satisfiability problems),因此可满足性问题解决器的研究成为形式验证领域的研究关键,国外不少大学、研究机构及大公司(如Intel和IBM等公司)都针对可满足性问题解决器展开了深入的研究,并取得了显著成果。许多研究成果已不再停留在实验室阶段而被成功地应用到实际工业设计中,如微处理器、浮点部件、协议、存储阵列和通信硬件等。许多基于可满足性问题解决器的工具被开发出来,并成功的进入到应用领域。本论文在较为全面的阐述了国内外形式验证技术研究成果的基础上,深入的研究了可满足性问题及DPLL算法,最终设计实现了新型可满足性问题解决器-——ArtSat,并通过比较性试验取得了较为理想的结果。本论文重点讨论了基于DPLL搜索算法中高级推理过程。普通的基于DPLL的算法有四部分组成：决策过程、BCP过程、学习过程和回溯过程,提高DPLL算法的效率从侧面上就要提高这四个过程中某一过程或几个过程中的效率,为了兼顾算法的计算复杂性和时间复杂性,通过对BCP过程的详细研究,本论文创新性的将一元推导技术与动态筛选算法相结合,并在其中加入VSIDS启发式策略,实现了该新型可满足性问题解决器。论文对可满足性问题解决器在算法级别提高效率进行了有意义的探索与研究,对电路等价性问题的提出了合理而有效的方案,在电路形式化验证领域具有一定的参考价值。

全文目录

摘要  2-3
Abstract  3-6
第一章绪论  6-14
  1.1 研究背景及意义  6-7
  1.2 集成电路设计验证综述  7-12
    1.2.1 模拟验证方法  7-8
    1.2.2 形式验证方法  8-12
  1.3 论文的主要工作和章节组织  12-13
    1.3.1 论文的主要工作  12
    1.3.2 章节组织及内容  12-13
  1.4 本章小结  13-14
第二章集成电路的等价性验证  14-18
  2.1 电路等价性检验方法  14-15
  2.2 集成电路等价性验证的一个简单例子  15-17
  2.3 本章小结  17-18
第三章可满足性问题  18-24
  3.1 布尔可满足性问题  18-19
  3.2 电路中布尔可满足性问题的应用  19-22
    3.2.1 布尔代数  19-20
    3.2.2 集合与布尔函数  20-21
    3.2.3 电路中布尔可满足性的应用  21-22
  3.3 可满足性问题算法  22-23
  3.4 本章小结  23-24
第四章 DPLL算法及其相关基础知识  24-33
  4.1 二叉判决图  24-25
  4.2 DPLL算法  25-27
  4.3 蕴含图(IG,IMPLICATION GRAPH)及基于冲突的学习过程  27-31
  4.4 决策变量选择策略  31-32
  4.5 本章小结  32-33
第五章基于高级正向推理的可满足性问题解决器  33-38
  5.1 对称扩展一元推导预处理  33-35
  5.2 动态筛选算法  35-36
    5.2.1 FLD算法  35-36
    5.2.2 动态筛选算法  36
  5.3 高级正向推理的可满足性问题解决器  36-37
  5.4 本章小结  37-38
第六章实验结果及分析  38-41
  6.1 比较性实验与实验分析  38-40
  6.2 实验结论  40-41
总结  41-43
致谢  43-44
参考文献  44-47
附录  47-49
攻读硕士学位期间研究成果  49-50

应用于集成电路形式化验证的SAT算法研究

内容摘要

全文目录

相似论文