Formal equivalence verification and debugging techniques with auto-correction mechanism for RTL designs

By increasing the complexity of system on chip (SoC) designs formal equivalence verification and debugging have become more and more important. Lower level methods such as BDDs and SAT solvers suffer from space and time explosion problems to match sizes of industrial designs in formal equivalence verification and debugging. This paper proposes techniques to verify and debug datapath intensive designs based on a canonical decision diagram called Horner Expansion Diagram (HED). It allows us to check the equivalence between two models in different levels of abstraction, e.g., a Register Transfer Level (RTL) implementation and a non-cycle-accurate specification. In order to reduce the complexity of equivalence checking problem, we tackle the exponential path enumeration problem by automatically identifying internal equivalent conditional expressions as well as suitable merge points. Our debugging technique is based on introducing mutations into the buggy implementation and then observing if the specification is capable of detecting these changes. We make use of a simple heuristic to reduce the number of mutants when dealing with multiple errors. We report the results of deploying our equivalence verification technique on several industrial designs which show 16.8× average memory usage reduction and 8.0× speedup due to merge-point detection. Furthermore, our debugging technique shows 13.7× average memory usage reduction and 4.6× speedup due to using SMT solvers to find equivalent conditions. In addition, the proposed debugging technique can avoid the computation of unnecessary mutants so that the results show 2.9× average reduction of the number of mutants to be processed.