Verifying the Equivalence of Sequential Circuits with Genetic Algorithms

In the design flow of digital VLSI circuits, modern state-of-the-art Computer-Aided Design techniques implemented in automatic synthesis and optimization tools can handle designs with thousands of flip-flops. However, many design steps are not guaranteed to be correct, either due to human intervention or to software bugs. The final quality of the produced circuit, therefore, heavily depends of the existence of an accurate and effective verification phase. This paper presents a new verification methodology suited to be used when the equivalence between two gate-level versions of the same circuit must be verified (e.g., after an optimization step); the approach is based on Genetic Algorithms and, while sometimes sacrificing exactness, is able to handle large circuits and give designers the opportunity to trade off CPU time with confidence on the result. The proposed methodology is able to fruitfully integrate the results provided by an exact verification tool, dramatically increasing the confidence on the validity of an optimization process. A prototypical tool has been developed and preliminary experimental results that support this claim are shown in the paper.