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