Project Title: Evolutionary Algorithms for Symbolic FSM Equivalence Checking Research Results in Equivalence Checking

ABSTRACT: Formal methods for the verification of Integrated Circuits (ICs) are a collection of techniques used to ensure the correctness of a design before fabrication. Formal methods have been investigated recently and continue to be an area of active research in the Computer Aided Design (CAD) for Electronic Design Automation (EDA) community. While many important results and CAD tools have resulted, the verification problem continues to be difficult due to the high complexity of the underlying algorithms and the circuits that they are intended to validate for correctness. One of the more successful approaches for formal verification is Equivalence Checking (EC), both for combinational and synchronous sequential circuits. In general EC is a method that requires two different models of a circuit that are used as input, typically at different levels of abstraction, and determines the functional equivalence (or non-equivalence) at some level. In this research, we are investigating methods to increase the effectiveness of EC. Specifically, we are experimenting with new data structures that are tuned specifically for use in EC algorithms. 1