基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究
| 摘要 | 第1-7页 |
| Abstract | 第7-16页 |
| 第1章 引言 | 第16-26页 |
| ·研究背景及意义 | 第16-23页 |
| ·功能验证技术 | 第16-20页 |
| ·电路测试技术 | 第20-21页 |
| ·等价性验证和测试生成技术 | 第21-23页 |
| ·论文主要工作和创新点 | 第23-24页 |
| ·论文组织结构 | 第24-26页 |
| 第2章 背景知识 | 第26-42页 |
| ·数字电路 | 第26-28页 |
| ·组合电路 | 第26页 |
| ·时序电路 | 第26-28页 |
| ·故障模型 | 第28-29页 |
| ·二叉判决图 | 第29-33页 |
| ·定义和性质 | 第29-30页 |
| ·BDD变量顺序 | 第30-32页 |
| ·BDD运算操作 | 第32-33页 |
| ·布尔可满足性问题 | 第33-41页 |
| ·SAT问题介绍 | 第33-34页 |
| ·基本DPLL框架 | 第34-35页 |
| ·基于DPLL的优化技术 | 第35-37页 |
| ·组合电路SAT解算器 | 第37-40页 |
| ·时序电路SAT解算器 | 第40-41页 |
| ·本章小结 | 第41-42页 |
| 第3章 组合电路等价性验证技术 | 第42-55页 |
| ·方法概述 | 第42-45页 |
| ·基于输出分组和电路SAT的组合等价性验证算法 | 第45-54页 |
| ·算法流程 | 第45-46页 |
| ·AIG结构简化 | 第46-49页 |
| ·输出分组启发式算法 | 第49-51页 |
| ·电路SAT验证子问题 | 第51-52页 |
| ·继承已有学习信息 | 第52页 |
| ·实验结果 | 第52-54页 |
| ·本章小结 | 第54-55页 |
| 第4章 时序电路等价性验证技术 | 第55-76页 |
| ·面向时序电路的等价性验证系统 | 第55-56页 |
| ·触发器匹配技术 | 第56-62页 |
| ·匹配问题及己有算法介绍 | 第56-58页 |
| ·局部BDD匹配技术 | 第58-59页 |
| ·目标模拟技术 | 第59-60页 |
| ·匹配算法描述 | 第60-61页 |
| ·实验结果 | 第61-62页 |
| ·时序电路等价性验证算法 | 第62-74页 |
| ·之前算法回顾 | 第63-65页 |
| ·基于SAT的时序等价性算法 | 第65-74页 |
| ·时序电路算法流程 | 第65-67页 |
| ·时间帧扩展方法 | 第67-69页 |
| ·动态识别不变量 | 第69-70页 |
| ·反例查找启发式方法 | 第70-72页 |
| ·实验结果 | 第72-74页 |
| ·本章小结 | 第74-76页 |
| 第5章 基于SAT的时序电路自动测试矢量生成技术 | 第76-94页 |
| ·数字系统的自动测试矢量生成技术 | 第76-79页 |
| ·基于SAT的时序ATPG方法 | 第79-82页 |
| ·基于改进联接电路模型的时序ATPG方法 | 第82-85页 |
| ·故障注入技术 | 第82-83页 |
| ·时序ATPG模型介绍 | 第83-85页 |
| ·结合多种SAT引擎的时序ATPG算法 | 第85-92页 |
| ·算法流程 | 第85-87页 |
| ·结构化故障分组策略 | 第87页 |
| ·应用边界模型检验查找测试矢量 | 第87-89页 |
| ·应用不变量来简化电路和识别不可测故障 | 第89页 |
| ·时序SAT求解较难测故障 | 第89页 |
| ·实验结果 | 第89-92页 |
| ·本章小结 | 第92-94页 |
| 第6章 基于SAT的诊断测试生成技术 | 第94-112页 |
| ·引言 | 第94-95页 |
| ·诊断测试矢量生成算法相关研究 | 第95-97页 |
| ·基于SAT的诊断测试矢量生成 | 第97-110页 |
| ·单故障类型的DTPG模型 | 第98-101页 |
| ·不同故障类型间DTPG模型 | 第101-103页 |
| ·多故障间DTPG模型 | 第103-104页 |
| ·诊断测试矢量压缩技术 | 第104-106页 |
| ·基于SAT的DTPG技术的诊断流程 | 第106-107页 |
| ·实验结果 | 第107-110页 |
| ·本章小结 | 第110-112页 |
| 第7章 总结和展望 | 第112-115页 |
| ·论文工作总结 | 第112-113页 |
| ·今后工作展望 | 第113-115页 |
| 参考文献 | 第115-122页 |
| 攻读学位期间发表的学术论文 | 第122-123页 |
| 致谢 | 第123-124页 |
