基于布尔可满足性的电路设计错误诊断

论文摘要

集成电路设计过程中，随着电路规模和复杂度的增大，设计错误变得越来越常见且难于处理。已有的验证算法和技术都是基于确保设计正确性的原则，回答电路实现和规格说明是否等价一致，其包括电路模拟和形式验证——属性检查与等价验证。所有这些方法只能探测设计错误的存在性，而无法指出电路不等价的原因。尽管验证工具越来越趋于高效且自动化，但数字电路的设计错误诊断和纠错依然是人工主导的、耗费时间和资源的过程。本文研究了基于SAT的电路诊断，讨论在错误的电路实现中如何定位设计错误源头，提出一种新的组合电路错误珍断方法。本文提出的方法不依赖于故障模型，从而适合各种类型的设计错误，存与模型无关的条件下依靠电路元件的非决定性行为来实现对电路逻辑错误的诊断定位。该方法是混合半形式的，结合了传统基于模拟的方法和多可满足性问题求解技术。它首先使用形式的SAT诊断，在无损的条件下提供给局部错误模拟一个规模较小的怀疑列表，从而减小了错误模拟的负担，我们判定仅仅是那些能够纠正每一个给定错误输入矢量的信号才被认为是潜在错误源头。该方法提出增量式的诊断流程，将复杂的多错误诊断问题分步化解为错误基数较小的子问题，从而实现诊断问题的“化难为易”。该方法是基于布尔可满足性的，考虑到每个输入测试矢量反映的错误数目差别，通过对诊断电路插入严格约束和松散约束两种性质的额外逻辑单元搭建诊断平台，将诊断问题编码转化为可满足性问题，将修改的SAT算法作为计算引擎应用到电路诊断领域。方法使用多项启发式方法，通过对可满足解的分级排序，提高了多错误诊断定位的分辨率和准确度，在时间和内存上保持了有效性。实验结果表明，由于基于SAT的诊断保证返回一个正确的解，所以利用形式验证的技术来导向模拟的过程，抓住了高复杂度的多错误定位问题的特征，提高了电路错误诊断的效率。

论文目录

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