基于SMT约束求解器的Verilog组合电路等价性验证
| 摘要 | 第1-6页 |
| Abstract | 第6-10页 |
| 第1章 绪论 | 第10-14页 |
| ·研究背景和意义 | 第10-11页 |
| ·研究现状 | 第11-13页 |
| ·论文主要工作 | 第13-14页 |
| 第2章 形式化方法介绍 | 第14-20页 |
| ·模型检测 | 第14-15页 |
| ·定理证明 | 第15页 |
| ·等价性验证 | 第15-18页 |
| ·基于功能的方法 | 第16页 |
| ·基于结构的方法 | 第16-18页 |
| ·基于 SAT 的方法 | 第18页 |
| ·形式化模型提取 | 第18-19页 |
| ·本章小结 | 第19-20页 |
| 第3章 基于 SMT 的组合等价性验证 | 第20-33页 |
| ·基于 SAT 的组合等价性验证 | 第21-23页 |
| ·算法思想 | 第23-24页 |
| ·算法实现 | 第24-26页 |
| ·运行实例 | 第26-29页 |
| ·实验结果和分析 | 第29-32页 |
| ·本章小结 | 第32-33页 |
| 第4章 结合割集和不可满足核的组合等价性验证 | 第33-42页 |
| ·算法思想 | 第33-37页 |
| ·基于割集的方法 | 第33-35页 |
| ·误判问题 | 第35-36页 |
| ·不可满足核与误判消除 | 第36-37页 |
| ·算法实现 | 第37-40页 |
| ·割点产生 | 第38页 |
| ·误判消除 | 第38-39页 |
| ·算法描述 | 第39-40页 |
| ·实验结果和分析 | 第40-41页 |
| ·本章小结 | 第41-42页 |
| 第5章 结论和展望 | 第42-44页 |
| ·结论 | 第42页 |
| ·工作展望 | 第42-44页 |
| 参考文献 | 第44-47页 |
| 附录 | 第47-48页 |
| 附录 A：支持的可综合语法结构 | 第47-48页 |
| 作者简介及在学期间所取得的科研成果 | 第48-49页 |
| 致谢 | 第49页 |
