基于SAT的数字电路ATPG方法及应用

论文摘要

测试向量自动生成（Automatic Test Pattern Generation，ATPG）问题在数字电路的测试领域具有非常重要的地位，不仅影响产品的生产设计成本，而且是评价产品可靠性的重要环节。传统的ATPG求解方法不仅很难求解规模较大的问题，而且无法处理相对较难探测的问题。随着对布尔可满足性（SAT）问题的深入研究和高效SAT求解器的出现，使得处理大规模的SAT问题成为可能。本文通过对Verilog语言描述的集成电路进行解析、建模，将抽象门级的数字电路模型转化为合取范式（Conjunctive NormalForm，CNF）的形式，并针对单固定型故障模型（Single Stuck-at Fault，SSF）进行建模和转化，通过构建连接电路（Miter），将ATPG问题转化为SAT问题，最终由SAT求解器（SAT-solver）进行求解，同时对整个系统的实现过程进行了简要说明。通过对模型的转化，将该方法应用于集成电路的等价性验证（EquivalenceChecking）领域。等价性验证是集成电路设计领域中应用最广泛的验证技术，对产品的设计开发周期有很大影响。通过构建连接电路，将参考电路（ReferenceCircuit）和实现电路（Implementation Circuit）进行连接，通过对用Verilog描述的电路进行Elaboration展开和转为Static Single Assignment （SSA）形式的中间代码描述，最后交由可满足性模理论（Satisfiability ModuloTheories，SMT）求解器进行求解。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 研究背景和意义
• 1.2 研究现状与分析
• 1.3 本文的主要工作
• 1.4 论文组织结构
• 第2章 布尔可满足性问题
• 2.1 SAT 问题简介
• 2.2 基本求解方法
• 2.3 应用范例
• 2.4 本章小结
• 第3章 ATPG 技术
• 3.1 数字电路测试技术
• 3.2 故障和故障模型
• 3.2.1 电路故障
• 3.2.2 故障模型
• 3.3 数字电路的 ATPG 技术
• 3.3.1 ATPG 简介
• 3.3.2 基本求解方法
• 3.4 评价标准
• 3.5 本章小结
• 第4章 基于 SAT 的 ATPG 方法与系统实现
• 4.1 方法简介
• 4.2 总体流程
• 4.3 系统描述
• 4.4 建立模型
• 4.4.1 Verilog 简介
• 4.4.2 构建连接电路
• 4.4.3 语法分析
• 4.4.4 模型抽取
• 4.4.5 转化为逻辑表达式
• 4.5 故障建模
• 4.6 问题求解
• 4.7 系统实现
• 4.8 测试分析
• 4.9 方法评价
• 4.10 本章小结
• 第5章 其他应用
• 5.1 集成电路的等价性验证
• 5.2 基于 SAT 的方法
• 5.3 模型抽取
• 5.4 实验结果
• 5.5 方法评价
• 5.6 本章小结
• 第6章 总结与展望
• 6.1 工作总结
• 6.2 展望
• 参考文献
• 作者简介及在学期间所取得的科研成果
• 致谢