形式化验证技术在EDA软件开发中的应用
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 第一章 绪论 | 第7-15页 |
| ·研究背景 | 第7-8页 |
| ·基于 HDL 的 FPGA 设计流程 | 第8-11页 |
| ·设计输入 | 第8-9页 |
| ·功能仿真 | 第9页 |
| ·综合优化 | 第9-10页 |
| ·综合后仿真 | 第10页 |
| ·布局布线 | 第10-11页 |
| ·布局布线后仿真 | 第11页 |
| ·生成并下载位流文件 | 第11页 |
| ·形式化验证 | 第11-13页 |
| ·本文研究内容和章节安排 | 第13-15页 |
| 第二章 时序逻辑及框架时序逻辑程序设计语言 | 第15-21页 |
| ·时序逻辑 | 第15-16页 |
| ·框架时序逻辑程序设计语言 | 第16-19页 |
| ·本章小结 | 第19-21页 |
| 第三章 解释器工具移植开发及应用 | 第21-35页 |
| ·解释器设计原理 | 第21-23页 |
| ·解释器移植 | 第23-26页 |
| ·QT 简介 | 第23-24页 |
| ·解释器移植框架 | 第24-26页 |
| ·设计简单时序电路 | 第26-34页 |
| ·触发器电路 | 第27-29页 |
| ·使用框架时序逻辑语言描述触发器元件 | 第29-31页 |
| ·寄存器电路 | 第31-32页 |
| ·使用框架时序逻辑语言设计寄存器电路 | 第32-34页 |
| ·本章小结 | 第34-35页 |
| 第四章 可满足性验证 | 第35-49页 |
| ·可满足性验证 | 第35-37页 |
| ·布尔公式 | 第35-37页 |
| ·消解和相融 | 第37页 |
| ·SAT 算法 | 第37-40页 |
| ·DP 算法 | 第38-39页 |
| ·DPLL 算法 | 第39-40页 |
| ·DPLL 算法改进 | 第40-47页 |
| ·基本流程 | 第40-41页 |
| ·启发分支 | 第41-42页 |
| ·决策推理 | 第42-43页 |
| ·基于冲突的学习和非同步回溯 | 第43-44页 |
| ·预处理、重启及其它技术 | 第44页 |
| ·学习子句的删除 | 第44-45页 |
| ·基准电路测试 | 第45-47页 |
| ·本章小结 | 第47-49页 |
| 第五章 组合电路的等价性验证 | 第49-61页 |
| ·逻辑综合 | 第49-56页 |
| ·约束条件 | 第50页 |
| ·基本流程 | 第50-53页 |
| ·逻辑综合工具 | 第53-55页 |
| ·RTL 设计原则 | 第55-56页 |
| ·逻辑综合前后电路等价性 | 第56-59页 |
| ·本章小结 | 第59-61页 |
| 总结与展望 | 第61-63页 |
| 致谢 | 第63-65页 |
| 参考文献 | 第65-69页 |
| 研究成果 | 第69-70页 |
