Formal Verification and Debugging of VLSI Logic Design for Systems Dependability: Experiments and Evaluation

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.