Formal Verification and Debugging of VLSI Logic Design for Systems Dependability: Experiments and Evaluation
Formal Verification and Debugging of VLSI Logic Design for Systems Dependability: Experiments and Evaluation
复制标题
用于系统可靠性的 VLSI 逻辑设计的形式验证和调试：实验和评估
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
K. Wakabayashi
中科院分区：
文献类型：
--
作者：
M. Fujita;Takeshi Matsumoto;A. M. Gharehbaghi;Kosuke Oshima;Satoshi Jo;Hiroaki Yoshida;Takashi Takenaka;K. Wakabayashi
在这一章中，我们讨论了逻辑验证和调试方法，并对工业设计和基准电路进行了评估。首先，形式验证方法，主要是形式等价性检查问题，快速审查相对于基于C的设计流程。通过各种评估，包括与工业设计，它被发现，如果这两个设计描述是文本上或结构上接近，形式验证是有用的和可扩展的，而如果这两个是非常不同的，如在C和RTL/门级的设计之间的情况下，除非内部信号的信息是可用的，验证问题仍然非常困难。为了解决这一问题，提出了一种从RTL/门级生成C语言描述的新方法，将C语言与RTL/门级之间的等价性检验问题转化为两个C设计之间的等价性检验问题。然后，形式逻辑调试方法进行评估，使用工业错误电路。将童车设计的修正问题分为三种情况，并结合工业设计实验对每种情况进行了讨论。在前两种情况下，涵盖了工业设计中大约70-80%的错误，将错误设计转换为正确设计的策略相当简单，而且可扩展。然而，为了涵盖其余的童车设计，必须处理需要全局拓扑变化的最一般和最困难的情况。作为一种尝试来解决这个问题，一个全新的方法，这种情况下，搜索适当的和最小的信号集的门，而不显式地产生门的功能。
In this chapter, we discuss logic verification and debugging methods with evaluation results on the industrial designs as well as benchmark circuits. First, formal verification methods, mainly for formal equivalence checking problems, are quickly reviewed with respect to C-based design flows. Through various evaluations including the ones with industrial designs, it is found that, if the two design descriptions are textually or structurally close, formal verification is useful and scalable, whereas if the two are very different, such as the case between designs in C and RTL/gate level, unless information on internal signals are available, the verification problem remains very hard. As an attempt to overcome the problem, a new method, which generates C descriptions from RTL/gate level in order to convert the equivalence checking problems between C and RTL/gate level into the ones between two C designs is introduced. Then, formal logic debugging methods are evaluated using industrial buggy circuits. The correction problems for the buggy designs are classified into three situations, and each one is discussed with experiments on industrial designs. In the first two situations, which covers around 70–80% of bugs in industrial designs, the strategy to transform the buggy designs into correct ones is fairly simple and also scalable. In order to cover the rest of the buggy designs, however, the most general and difficult situation which needs global topological changes must be dealt with. As an attempt to resolve the problem, a completely new approach for such a situation, which searches for appropriate and minimum sets of signals for gates without explicitly generating the functions of the gates is introduced.