Why does equivalence checking work in practice?
The application of formal methods for hardware verification had various degrees of success in practical design flows. For example, because of its limited capacity and significant impact on the design methodology, a broad use of model checking for entire designs is still challenging. In contrast, formal equivalence checking has been adopted as a main stream tool in many design flows. In the presentation we will discuss basic approaches to the equivalence checking problem and demonstrate how the corresponding algorithms can be adopted to make them work for a large class of circuits despite their computational complexity.