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

《基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、浙江大学博+L学位论文摘要近些年在布尔可满足性(SAT)领域取得了较大进展，一系列基于DPLL框架的优化算法被提出，有效SAT解算器诸如zChaff等已可解决很大规模的SAT问题。SAT作为一个优秀引擎在EDA领域已广泛应用，本论文的主要方向就是探索如何有效地将SAT技术应用于等价性验证和测试生成这两类重要问题中。下面概括本论文的主要研究方向和创新点：1．基于输出分组和电路SAT的组合等价性验证技术。随着芯片设计规模同益庞大复杂，功能验证成为现阶段IC设计过程中的瓶颈环节，而传统模拟技术已很难满足现时集成电路设计的要求。作为模拟技术的补充，组合等价性验证工具在IC功能验

2、证中使用已日益普遍。本文提出一种基于电路可满足性和输出分组技术的组合电路等价性验证算法。算法首先使用与非图结构哈希技术来简化验证任务。对那些具有较多输出的复杂电路，为共享结构信息从而提高验证速度，使用输出分组技术将那些共享较多内部结点的输出转化为一个子问题，从而验证问题可转化为一系列验证子问题。对每一个子问题，使用将电路SAT和BDD学习等技术结合的验证算法来解决。实验结果表明该类方法可有效用于解决大规模电路的验证问题。2．结合不变量提取和时序SAT的时序等价性验证技术。应用组合等价性验证工具的重要的限制是两个待验证电路的触发器之间存在一一对应关系。然而对一个复杂设计，

3、通常在调用综合工具时会进行重定时等时序优化，这些优化容易破坏综合前后设计触发器间对应关系。因此，验证浙江大学博I：学位论文摘要这些类型设计就必须使用时序等价性验证技术。本文提出一种时序等价性验证框架：为探索验证任务间结构相似性，算法使用不变量提取引擎来提前识别电路中有效不变量；为减少不变量提取时的误判几率，提出了时间帧扩展和动态选择候选集两种优化策略，同时提出了不变量提取过程中的快速查找反例启发式方法。对使用不变量引擎后尚未解决任务，可进一步使用完整的时序SAT引擎来解决。从对部分ISCAS89电路和工业实例的实验结果表明，提出技术对验证复杂时序电路提供了一种可能方案。

4、3．基于改进联接电路模型的时序自动测试生成技术。面向时序电路的ATPG问题是EDA领域中具有高度计算复杂性问题之一，运行传统时序ATPG的观察发现大部分计算开销用于解决那些较难观测故障。针对使用传统SAT方法需要对每个故障构建一次联接电路的不足，本文中提出了可同时注入多个候选故障的电路模型。使用该改进模型的关键好处在于：(1)之前SAT求解过程中获得的有用信息可在测试其他故障时完全重用，这样可大大降低求解的计算开销；(2)当SAT求解结果显示为不可满足时，可以断定剩余所有故障是不可测试的，因此查找那些不可测故障仅仅是SAT求解的副产品。此外，将不变量提取、边界模型检验和

5、时序SAT解算器结合并充分发挥各自引擎的优点，可进一步提高时序ATPG求解的效率。实验表明，该算法是一种有效的算法，尤其适用于测试那些常规方法无法解决的较难观测故障。4．支持多故障和不同故障类型的诊断测试生成技术。时序ATPG的改进联接电路模型可扩展到诊断测试生成(DTPG)应用中，本文提出了一种基于SAT的DTPG技术。基于扩展的模型技术，可共享求解不同故浙江人学博{：学位论文摘要障对DTPG时获得的学习信息来极大地改进DTPG搜索效率。进一步，可将该模型扩展应用于区分多故障、不同故障类型间的DTPG问题，这里故障包括静态和动态故障。为减少产生的诊断矢量数目，文中提出

6、一种探索原始输入中无关值(don’tcare)的诊断测试矢量压缩方法。将提出的DTPG技术与已有故障诊断结合起来，实验发现可以获得较好诊断精度和获得更多故障信息。关键词形式验证；等价性验证；二叉判决图；可满足性问题；不变量；自动测试矢量生成；故障诊断；浙江大学博l：学位论文AbstractAbstractWiththedevelopmentofmodemandefficientBooleanSatisfiability(SAT)algorithmsinrecentyears，SAThasincreasinglymadeasignificantimpactonelectr

7、onicdesignautomation(EDA)applications．InthisthesisweinvestigatetheapplicationofmodemSATenginefortheequivalencecheckingandtestpatterngenerationproblems．Theoriginalcontributionsofthisthesisareasfollows：1．Efficientcombinationalequivalencecheckingusingoutputgroupingandcircuit