| 摘要 | 第5-6页 |
| Abstract | 第6-7页 |
| 第一章 绪论 | 第10-13页 |
| 1.1 研究背景 | 第10-11页 |
| 1.2 国内外发展现状 | 第11-12页 |
| 1.3 研究内容与研究意义 | 第12页 |
| 1.4 文章结构组织 | 第12-13页 |
| 第二章 相关理论与背景技术 | 第13-30页 |
| 2.1 常见模型检测 | 第13-22页 |
| 2.1.1 CTL模型检测 | 第13-14页 |
| 2.1.2 边界模型检测(BMC) | 第14-15页 |
| 2.1.3 GSTE模型检测 | 第15-22页 |
| 2.2 基于BDD的GSTE模型检测工具简介 | 第22-27页 |
| 2.2.1 BDD简介 | 第22-25页 |
| 2.2.2 基于BDD的GSTE模型检测工具 | 第25-27页 |
| 2.3 对基于BDD的GSTE工具的分析与本文基本思路 | 第27-28页 |
| 2.4 工作平台及实验环境 | 第28-29页 |
| 2.4.1 ABC | 第28-29页 |
| 2.4.2 vl2mv | 第29页 |
| 2.5 本章小结 | 第29-30页 |
| 第三章 基于AIG的GSTE模型检测 | 第30-50页 |
| 3.1 AIG简介 | 第30-33页 |
| 3.1.1 基本概念 | 第30-31页 |
| 3.1.2 常用的AIG化简 | 第31页 |
| 3.1.3 AIG常用布尔操作 | 第31-32页 |
| 3.1.4 与BDD间的转化及比较 | 第32-33页 |
| 3.2 使用AIG的模型表示 | 第33-35页 |
| 3.2.1 使用AIG表示模型 | 第33-34页 |
| 3.2.2 使用AIG表示断言图 | 第34-35页 |
| 3.3 使用AIG完成POST计算 | 第35-48页 |
| 3.3.1 FRAIGs | 第35-36页 |
| 3.3.2 量词调度 | 第36-48页 |
| 3.4 使用AIG的cons验证 | 第48页 |
| 3.5 使用AIG的局限 | 第48-49页 |
| 3.6 本章小结 | 第49-50页 |
| 第四章 结合AIG和SAT的GSTE模型检测 | 第50-62页 |
| 4.1 SAT求解器 | 第50-55页 |
| 4.1.1 SAT问题 | 第50-51页 |
| 4.1.2 SAT求解器 | 第51-54页 |
| 4.1.3 MiniSAT | 第54-55页 |
| 4.2 AIG与CNF范式的转化 | 第55-56页 |
| 4.3 使用SAT求解器的量词消除 | 第56-58页 |
| 4.4 基于电路分解的量词消除 | 第58-61页 |
| 4.4.1 方法背景介绍 | 第58页 |
| 4.4.2 基于电路分解的SAT求解器量词消除方法 | 第58-59页 |
| 4.4.3 相关优化 | 第59-61页 |
| 4.5 使用SAT求解器和使用AIG、BDD的比较 | 第61页 |
| 4.6 本章小结 | 第61-62页 |
| 第五章 实验结果与分析 | 第62-73页 |
| 5.1 SPDIF_ENCODE模块及其断言图设计 | 第62-69页 |
| 5.1.1 SPDIF_ENCODE模块简介 | 第62-64页 |
| 5.1.2 相关性质及其断言图设计 | 第64-69页 |
| 5.2 实验与数据分析 | 第69-72页 |
| 5.3 本章小结 | 第72-73页 |
| 第六章 总结与展望 | 第73-76页 |
| 6.1 全文总结 | 第73-74页 |
| 6.1.1 主要研究成果与创新点 | 第73-74页 |
| 6.1.2 存在的不足 | 第74页 |
| 6.2 下一步的工作与展望 | 第74-76页 |
| 致谢 | 第76-77页 |
| 参考文献 | 第77-81页 |
| 攻读硕士期间取得的研究成果 | 第81-82页 |
