基于字级求解的电路错误自动定位方法研究

随着VLSI芯片功能越来越复杂，大量的时间消耗在功能验证上，而目前错误定位仍主要依赖于手工劳动，效率低下且易于引入新的错误，因此错误自动定位方法成为新的研究热点。但是现有方法存在抽象层次低、运算复杂度高、处理电路规模有限等问题。.针对这些问题，研究基于字级求解的电路错误自动定位理论与方法；研究基于约束依赖图的高层HDL程序切片算法，以抽取有效电路；研究基于等价约简与蕴含消除的断言精化方法，以减小断言规模；研究融合字级不可满足子式与Craig插值的错误踪迹优化方法，以提高定位精度；研究基于否证分析与增量式求解的错误敏感向量压缩方法，以剔除冗余输入；面向RTL级和行为级电路描述，设计实现错误自动定位的原型系统。.本项目的研究成果，能够显著提高VLSI芯片验证的效率，有助于缩短设计周期，突破制约芯片验证的瓶颈，具有重要理论意义与实际应用价值。

针对VLSI芯片的设计与验证流程中，诊断与定位错误依赖于手工劳动且效率低下的问题，项目重点研究如何自动、高效地定位RTL级和行为级电路描述中的错误，通过设计与实现一系列形式化方法与技术，大大提高错误定位的效率与精度，从而加速芯片的设计与验证流程。项目的主要研究成果包括：.（1）针对近年来出现的许多电路错误定位方法，深入研究与分析了基于位级与字级的错误定位方法的基本原理，并对各种算法进行了评估与分析；并针对不可满足子式能够显著提高错误定位效率与精度进行了深入分析。.（2）针对求解不可满足子式可以显著提高电路定位错误的效率，提出了悖论证明与悖论解析树的概念，并提出一种启发式局部搜索算法，从布尔公式的悖论证明中求解不可满足子式。基于实际测试集进行了实验对比，结果表明该算法优于同类最优算法。.（3）针对布尔不可满足子式能够帮助自动化工具迅速定位电路错误，提出了求解布尔不可满足子式的消解悖论算法。它属于一种非完全算法，对于业界常见的3-SAT和2-SAT问题非常高效。基于随机测试集进行了实验对比，结果表明消解悖论算法优于其他同类算法。.（4）随着硬件设计与验证的抽象层次越来越高，基于一阶逻辑的可满足性模逐渐成为研究热点。针对极小可满足性模的不可满足子式的求解问题，提出了基于深度优先搜索与增量式求解的算法。与目前最优算法对比，该算法能够有效地求解极小不可满足子式，并且随着公式的规模增大，算法更加高效。.（5）高速缓冲存储器（Cache）的错误定位是验证领域的研究热点与难点，对此提出了一种面向Cache的可综合伪随机验证与错误定位方法。与业界常用的方法对比，该方法的处理速度快约3个数量级，并且能够精确地定位更多的功能错误。.（6）谓词抽象技术是解决错误定位中状态空间组合爆炸问题的重要途径，而不可满足子式能够减少谓词抽象过程中精化迭代的次数。因此将两种最小不可满足子式的求解算法进行了集成与对比，并深入分析了不可满足子式在硬件谓词抽象中的作用，以及如何加速电路的错误定位过程。