| 摘要 | 第1-7页 |
| Abstract | 第7-12页 |
| 第1章 绪论 | 第12-32页 |
| ·研究背景 | 第12-15页 |
| ·EDA技术发展现状 | 第15-20页 |
| ·SAT问题的研究现状 | 第20-28页 |
| ·目前存在的主要问题 | 第28-29页 |
| ·本文主要工作 | 第29-31页 |
| ·论文的组织结构 | 第31-32页 |
| 第2章 基础理论 | 第32-44页 |
| ·SAT问题和问题复杂性分类 | 第32-35页 |
| ·SAT问题 | 第32-33页 |
| ·问题复杂性分类 | 第33-35页 |
| ·DPLL算法 | 第35-39页 |
| ·计算模型 | 第39-43页 |
| ·CNF | 第39-41页 |
| ·BDD | 第41-42页 |
| ·AIG | 第42-43页 |
| ·本章小结 | 第43-44页 |
| 第3章 基于SAT的等价验证 | 第44-58页 |
| ·引言 | 第44-45页 |
| ·等价验证 | 第45-47页 |
| ·组合电路等价验证 | 第45页 |
| ·时序电路等价验证 | 第45-47页 |
| ·相关定义 | 第47-48页 |
| ·可观无关性利用及SAT求解算法改进 | 第48-54页 |
| ·可观无关条件传播计算 | 第49-51页 |
| ·控制唯一属性的实现 | 第51-53页 |
| ·算法实现 | 第53-54页 |
| ·实验结果 | 第54-56页 |
| ·本章小结 | 第56-58页 |
| 第4章 基于SAT的无界模型检验 | 第58-83页 |
| ·引言 | 第58-60页 |
| ·无界模型检验 | 第60-67页 |
| ·系统和属性表示 | 第61-64页 |
| ·像计算 | 第64-65页 |
| ·前像计算 | 第65-67页 |
| ·搜索空间分析及All-SAT求解算法 | 第67-70页 |
| ·搜索空间分析 | 第67页 |
| ·All-SAT求解算法 | 第67-70页 |
| ·基于All-SAT的前像计算 | 第70-77页 |
| ·变量决策策略改进的标准SAT求解器 | 第71-72页 |
| ·解立方体扩展 | 第72-75页 |
| ·解的存储 | 第75页 |
| ·无关状态利用 | 第75-76页 |
| ·增量式技术 | 第76-77页 |
| ·实验结果 | 第77-82页 |
| ·本章小结 | 第82-83页 |
| 第5章 局部算法和DPLL算法相结合的混合SAT算法 | 第83-97页 |
| ·引言 | 第83-84页 |
| ·局部搜索算法 | 第84-86页 |
| ·混合算法HBISAT及分析 | 第86-87页 |
| ·混合算法改进和实现 | 第87-94页 |
| ·基本思想 | 第87-88页 |
| ·局部算法改进 | 第88-90页 |
| ·随机算法和DPLL算法之间的协调 | 第90-91页 |
| ·子句填充 | 第91-93页 |
| ·混合算法实现 | 第93-94页 |
| ·实验结果 | 第94-96页 |
| ·本章小结 | 第96-97页 |
| 第6章 基于SAT的FPGA工艺映射 | 第97-108页 |
| ·引言 | 第97-98页 |
| ·基于SAT的FPGA工艺映射方法 | 第98-101页 |
| ·FPGA功能到可满足问题的转换 | 第98-100页 |
| ·输入置换 | 第100-101页 |
| ·算法改进思想 | 第101-105页 |
| ·PLB结构中的对称 | 第102-104页 |
| ·布尔函数对称 | 第104-105页 |
| ·FPGA工艺映射流程 | 第105-106页 |
| ·实验结果 | 第106-107页 |
| ·本章小结 | 第107-108页 |
| 结论 | 第108-111页 |
| 参考文献 | 第111-123页 |
| 攻读博士学位期间发表的论文和取得的科研成果 | 第123-124页 |
| 致谢 | 第124页 |