基于布尔可满足性的电路设计错误诊断
| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 绪论 | 第7-16页 |
| §1.1 集成电路的发展和设计流程的演变 | 第7页 |
| §1.2 设计验证和错误诊断 | 第7-10页 |
| §1.3 研究出发点 | 第10-14页 |
| §1.3.1 传统模拟与形式技术 | 第10-12页 |
| §1.3.2 多错误诊断的困难性 | 第12-13页 |
| §1.3.3 计算引擎 | 第13-14页 |
| §1.4 研究主要内容和重点 | 第14页 |
| §1.5 论文结构 | 第14-16页 |
| 第二章 预备知识 | 第16-23页 |
| §2.1 逻辑范式 | 第16页 |
| §2.2 异或运算与布尔差分 | 第16-17页 |
| §2.3 二分决策图 | 第17-19页 |
| §2.4 可满足性问题 | 第19-21页 |
| §2.5 故障模型 | 第21-23页 |
| 第三章 设计错误诊断的技术发展水平 | 第23-34页 |
| §3.1 问题综述 | 第23-25页 |
| §3.1.1 设计错误及其产生原因 | 第23-24页 |
| §3.1.2 设计错误诊断算法的历史 | 第24-25页 |
| §3.2 符号诊断法 | 第25-27页 |
| §3.3 基于电路结构的方法 | 第27-28页 |
| §3.4 基于模拟的方法 | 第28-33页 |
| §3.4.1 Cause-effect方法 | 第28-29页 |
| §3.4.2 Effect-Cause方法 | 第29-33页 |
| §3.5 小结 | 第33-34页 |
| 第四章 基于SAT的诊断算法研究 | 第34-46页 |
| §4.1 电路的可满足性 | 第34-35页 |
| §4.2 基于布尔可满足性的诊断机理 | 第35-37页 |
| §4.3 合取诊断模型 | 第37-38页 |
| §4.4 析取诊断模型 | 第38-39页 |
| §4.5 两种模型的公式分析 | 第39-40页 |
| §4.6 采用析取模型的诊断方法 | 第40-42页 |
| §4.7 实验结果与分析 | 第42-44页 |
| §4.8 小结 | 第44-46页 |
| 第五章 增量式的多错误诊断算法 | 第46-69页 |
| §5.1 问题定义 | 第46-48页 |
| §5.2 诊断问题的编码转换 | 第48-53页 |
| §5.3 增量式的诊断流程 | 第53-55页 |
| §5.4 事件驱动的错误模拟 | 第55-58页 |
| §5.5 计算引擎 | 第58-61页 |
| §5.6 算法实现细节 | 第61-65页 |
| §5.6.1 算法伪代码 | 第61-63页 |
| §5.6.2 加速诊断的启发式策略 | 第63-65页 |
| §5.7 实验结果与分析 | 第65-68页 |
| §5.8 小结 | 第68-69页 |
| 第六章 诊断算法的正确性 | 第69-75页 |
| §6.1 关于算法正确性的讨论 | 第69-73页 |
| §6.2 诊断算法的容错机制 | 第73-75页 |
| 第七章 总结和展望 | 第75-77页 |
| §7.1 论文工作总结 | 第75-76页 |
| §7.2 今后工作展望 | 第76-77页 |
| 参考文献 | 第77-84页 |
| 致谢 | 第84-85页 |
