基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究

论文摘要

近些年在布尔可满足性(SAT)领域取得了较大进展,一系列基于DPLL框架的优化算法被提出,有效SAT解算器诸如zChaff等已可解决很大规模的SAT问题。SAT作为一个优秀引擎在EDA领域已广泛应用,本论文的主要方向就是探索如何有效地将SAT技术应用于等价性验证和测试生成这两类重要问题中。下面概括本论文的主要研究方向和创新点:1.基于输出分组和电路SAT的组合等价性验证技术。随着芯片设计规模日益庞大复杂,功能验证成为现阶段IC设计过程中的瓶颈环节,而传统模拟技术已很难满足现时集成电路设计的要求。作为模拟技术的补充,组合等价性验证工具在IC功能验证中使用已日益普遍。本文提出一种基于电路可满足性和输出分组技术的组合电路等价性验证算法。算法首先使用与非图结构哈希技术来简化验证任务。对那些具有较多输出的复杂电路,为共享结构信息从而提高验证速度,使用输出分组技术将那些共享较多内部结点的输出转化为一个子问题,从而验证问题可转化为一系列验证子问题。对每一个子问题,使用将电路SAT和BDD学习等技术结合的验证算法来解决。实验结果表明该类方法可有效用于解决大规模电路的验证问题。2.结合不变量提取和时序SAT的时序等价性验证技术。应用组合等价性验证工具的重要的限制是两个待验证电路的触发器之间存在一一对应关系。然而对一个复杂设计,通常在调用综合工具时会进行重定时等时序优化,这些优化容易破坏综合前后设计触发器间对应关系。因此,验证这些类型设计就必须使用时序等价性验证技术。本文提出一种时序等价性验证框架:为探索验证任务间结构相似性,算法使用不变量提取引擎来提前识别电路中有效不变量;为减少不变量提取时的误判几率,提出了时间帧扩展和动态选择候选集两种优化策略,同时提出了不变量提取过程中的快速查找反例启发式方法。对使用不变量引擎后尚未解决任务,可进一步使用完整的时序SAT引擎来解决。从对部分ISCAS89电路和工业实例的实验结果表明,提出技术对验证复杂时序电路提供了一种可能方案。3.基于改进联接电路模型的时序自动测试生成技术。面向时序电路的ATPG问题是EDA领域中具有高度计算复杂性问题之一,运行传统时序ATPG的观察发现大部分计算开销用于解决那些较难观测故障。针对使用传统SAT方法需要对每个故障构建一次联接电路的不足,本文中提出了可同时注入多个候选故障的电路模型。使用该改进模型的关键好处在于:(1)之前SAT求解过程中获得的有用信息可在测试其他故障时完全重用,这样可大大降低求解的计算开销;(2)当SAT求解结果显示为不可满足时,可以断定剩余所有故障是不可测试的,因此查找那些不可测故障仅仅是SAT求解的副产品。此外,将不变量提取、边界模型检验和时序SAT解算器结合并充分发挥各自引擎的优点,可进一步提高时序ATPG求解的效率。实验表明,该算法是一种有效的算法,尤其适用于测试那些常规方法无法解决的较难观测故障。4.支持多故障和不同故障类型的诊断测试生成技术。时序ATPG的改进联接电路模型可扩展到诊断测试生成(DTPG)应用中,本文提出了一种基于SAT的DTPG技术。基于扩展的模型技术,可共享求解不同故障对DTPG时获得的学习信息来极大地改进DTPG搜索效率。进一步,可将该模型扩展应用于区分多故障、不同故障类型间的DTPG问题,这里故障包括静态和动态故障。为减少产生的诊断矢量数目,文中提出一种探索原始输入中无关值(don’t care)的诊断测试矢量压缩方法。将提出的DTPG技术与已有故障诊断结合起来,实验发现可以获得较好诊断精度和获得更多故障信息。

论文目录

• 摘要
• Abstract
• 第1章 引言
• 1.1 研究背景及意义
• 1.1.1 功能验证技术
• 1.1.2 电路测试技术
• 1.1.3 等价性验证和测试生成技术
• 1.2 论文主要工作和创新点
• 1.3 论文组织结构
• 第2章 背景知识
• 2.1 数字电路
• 2.1.1 组合电路
• 2.1.2 时序电路
• 2.2 故障模型
• 2.3 二叉判决图
• 2.3.1 定义和性质
• 2.3.2 BDD变量顺序
• 2.3.3 BDD运算操作
• 2.4 布尔可满足性问题
• 2.4.1 SAT问题介绍
• 2.4.2 基本DPLL框架
• 2.4.3 基于DPLL的优化技术
• 2.4.4 组合电路SAT解算器
• 2.4.5 时序电路SAT解算器
• 2.5 本章小结
• 第3章 组合电路等价性验证技术
• 3.1 方法概述
• 3.2 基于输出分组和电路SAT的组合等价性验证算法
• 3.2.1 算法流程
• 3.2.2 AIG结构简化
• 3.2.3 输出分组启发式算法
• 3.2.4 电路SAT验证子问题
• 3.2.5 继承已有学习信息
• 3.2.6 实验结果
• 3.3 本章小结
• 第4章 时序电路等价性验证技术
• 4.1 面向时序电路的等价性验证系统
• 4.2 触发器匹配技术
• 4.2.1 匹配问题及己有算法介绍
• 4.2.2 局部BDD匹配技术
• 4.2.3 目标模拟技术
• 4.2.4 匹配算法描述
• 4.2.5 实验结果
• 4.3 时序电路等价性验证算法
• 4.3.1 之前算法回顾
• 4.3.2 基于SAT的时序等价性算法
• 4.3.2.1 时序电路算法流程
• 4.3.2.2 时间帧扩展方法
• 4.3.2.3 动态识别不变量
• 4.3.2.4 反例查找启发式方法
• 4.3.2.5 实验结果
• 4.4 本章小结
• 第5章 基于SAT的时序电路自动测试矢量生成技术
• 5.1 数字系统的自动测试矢量生成技术
• 5.2 基于SAT的时序ATPG方法
• 5.3 基于改进联接电路模型的时序ATPG方法
• 5.3.1 故障注入技术
• 5.3.2 时序ATPG模型介绍
• 5.4 结合多种SAT引擎的时序ATPG算法
• 5.4.1 算法流程
• 5.4.2 结构化故障分组策略
• 5.4.3 应用边界模型检验查找测试矢量
• 5.4.4 应用不变量来简化电路和识别不可测故障
• 5.4.5 时序SAT求解较难测故障
• 5.4.6 实验结果
• 5.5 本章小结
• 第6章 基于SAT的诊断测试生成技术
• 6.1 引言
• 6.2 诊断测试矢量生成算法相关研究
• 6.3 基于SAT的诊断测试矢量生成
• 6.3.1 单故障类型的DTPG模型
• 6.3.2 不同故障类型间DTPG模型
• 6.3.3 多故障间DTPG模型
• 6.3.4 诊断测试矢量压缩技术
• 6.3.5 基于SAT的DTPG技术的诊断流程
• 6.3.6 实验结果
• 6.4 本章小结
• 第7章 总结和展望
• 7.1 论文工作总结
• 7.2 今后工作展望
• 参考文献
• 攻读学位期间发表的学术论文
• 致谢