集成电路设计过程中，随着电路规模和复杂度的增大，设计错误变得越来越常见且难于处理。已有的验证算法和技术都是基于确保设计正确性的原则，回答电路实现和规格说明是否等价一致，其包括电路模拟和形式验证——属性检查与等价验证。所有这些方法只能探测设计错误的存在性，而无法指出电路不等价的原因。尽管验证工具越来越趋于高效且自动化，但数字电路的设计错误诊断和纠错依然是人工主导的、耗费时间和资源的过程。本文研究了基于SAT的电路诊断，讨论在错误的电路实现中如何定位设计错误源头，提出一种新的组合电路错误珍断方法。本文提出的方法不依赖于故障模型，从而适合各种类型的设计错误，存与模型无关的条件下依靠电路元件的非决定性行为来实现对电路逻辑错误的诊断定位。该方法是混合半形式的，结合了传统基于模拟的方法和多可满足性问题求解技术。它首先使用形式的SAT诊断，在无损的条件下提供给局部错误模拟一个规模较小的怀疑列表，从而减小了错误模拟的负担，我们判定仅仅是那些能够纠正每一个给定错误输入矢量的信号才被认为是潜在错误源头。该方法提出增量式的诊断流程，将复杂的多错误诊断问题分步化解为错误基数较小的子问题，从而实现诊断问题的“化难为易”。该方法是基于布尔可满足性的，考虑到每个输入测试矢量反映的错误数目差别，通过对诊断电路插入严格约束和松散约束两种性质的额外逻辑单元搭建诊断平台，将诊断问题编码转化为可满足性问题，将修改的SAT算法作为计算引擎应用到电路诊断领域。方法使用多项启发式方法，通过对可满足解的分级排序，提高了多错误诊断定位的分辨率和准确度，在时间和内存上保持了有效性。实验结果表明，由于基于SAT的诊断保证返回一个正确的解，所以利用形式验证的技术来导向模拟的过程，抓住了高复杂度的多错误定位问题的特征，提高了电路错误诊断的效率。