Approximate equivalence verification of sequential circuits via genetic algorithms

We have presented VEGA2: a Genetic Algorithm-based approach to the problem of equivalence verification of sequential circuits. Although sacrificing the exactness of the verification, the advantages of such an approach lie in the ability to handle large designs and in the possibility to easily trade off CPU time with confidence on the result (by tuning the maximum number of generations). VEGA2 is not a replacement for exact verification tools, but a complement: when the complexity of the circuits prevents the use of a BDD-based algorithm, it is still able to provide meaningful results. We also presented a prototypical tool and experimental analysis that shows that VEGA2 is able to provide a larger number of correct results than both an exact method and the previous GA-based approach. Thus it is able increase confidence on the validity of an optimization process.