Fault diagnosis and logic debugging using Boolean satisfiability
Fault diagnosis and logic debugging using Boolean satisfiability
复制标题
使用布尔可满足性进行故障诊断和逻辑调试
DOI：
10.1109/mtv.2003.1250264
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
A. Veneris
中科院分区：
文献类型：
--
作者：
A. Veneris
布尔可满足性的最新进展使其在解决许多数字超大规模集成电路设计问题（如验证和测试生成）方面具有吸引力。现有的基于可满足性的解决方案尚未解决故障诊断和逻辑调试问题。我们针对这些问题提出了一种基于可满足性的无模型解决方案，试图弥合这一差距。提出的方案直观且易于实现。它表明，可满足性抓住了问题的重要特征，并提供了不同的权衡。它还为基于可满足性的诊断工具和特定于诊断的可满足性算法提供了新的机遇。理论和实验验证了这一说法，并证明了它的潜力。
Recent advances in Boolean satisfiability have made it attractive to solve many digital VLSI design problems such as verification and test generation. Fault diagnosis and logic debugging have not been addressed by existing satisfiability-based solutions. We attempt to bridge this gap by proposing a model-free satisfiability-based solution to these problems. The proposed formulation is intuitive and easy to implement. It shows that satisfiability captures significant problem characteristics and it offers different trade-offs. It also provides new opportunities for satisfiability-based diagnosis tools and diagnosis-specific satisfiability algorithms. Theory and experiments validate the claims and demonstrate its potential.