Fixing Design Errors with Counterexamples and Resynthesis
Fixing Design Errors with Counterexamples and Resynthesis
复制标题
通过反例和重新综合修复设计错误
DOI：
10.1109/tcad.2007.907257
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
V. Bertacco
中科院分区：
文献类型：
--
作者：
Kai;I. Markov;V. Bertacco
在这项工作中，我们提出了一个新的纠错框架，称为Core，它使用反例，或错误跟踪，在验证中产生的自动纠正数字设计中的错误。Core由两种创新的再合成技术提供动力，目标导向搜索（GDS）和熵导向搜索（EGS），它们修改内部电路节点的功能以匹配所需的规范。我们评估我们的解决方案的设计和组合等效检查过程中产生的错误，以及基于仿真的数字系统验证。与以前提出的技术相比，Core更强大，因为：（1）它可以修复更广泛的错误类型，因为它不依赖于特定的错误模型;（2）它从仿真向量中导出正确的功能，因此不需要黄金网表;（3）它可以应用于一系列验证流程，包括正式的和基于仿真的。
In this work we propose a new error-correction framework, called CoRe, which uses counterexamples, or bug traces, generated in verification to automatically correct errors in digital designs. CoRe is powered by two innovative resynthesis techniques, goal-directed search (GDS) and entropy-guided search (EGS), which modify the functionality of internal circuit's nodes to match the desired specification. We evaluate our solution to designs and errors arising during combinational equivalence-checking, as well as simulation-based verification of digital systems. Compared with previously proposed techniques, CoRe is more powerful in that: (1) it can fix a broader range of error types because it does not rely on specific error models; (2) it derives the correct functionality from simulation vectors, hence not requiring golden netlists; and (3) it can be applied to a range of verification flows, including formal and simulation-based.