Logic verification based on diagnosis techniques

We present a formal logic verification methodology for combinational circuits. The method uses simulation, logic diagnosis and ATPG to identify circuit lines that implement equivalent logic functions efficiently. One advantage of the proposed technique is that it identifies line equivalences under controllability and observability don´t care conditions, while not suffering from false negatives. The method is easy to implement, and, due to its general nature, existing techniques can benefit from ideas described here. We also give implementation details and present experiments to confirm its potential.