Evolutionary Algorithms for Symbolic FSM Equivalence Checking

Mississippi State University, Mississippi State MS

Investigators

Abstract

Integrated Circuits (ICs) are becoming more complex and market demand continues to pressure designers to produce new ICs in a shorter amount of time. For these reasons, there is interest in the use of verification methods that allow designers the ability to ensure correctness of their product without resorting to time-consuming simulation techniques. Two approaches for verification are equivalence checking and model checking. Internally, in these two approaches, a method for checking the equivalence of Finite State Machines (FSM) is commonly used. FSM equivalence checking is typically implemented through the use of a symbolic state-space reachability algorithm that uses BDD data structures and satisfiability (SAT) algorithms. While there have been advances in symbolic FSM machine state-space traversal methods in recent years, many designs of interest still cannot be verified using this method due to the transition relation (TR) BDD becoming too large, the BDD representing the state space already traversed becoming too large, the intermediate BDDs during image computation becoming too large, and, the overall process requiring too much computation time. Evolutionary algorithms have recently been applied to several problems in design automation. This research project involves the investigation of the use of evolutionary algorithms for exact and approximate FSM equivalence checking. Evolutionary algorithms are being developed that prune the TR and the reachable state BDDs such that exact, over-approximation or under-approximation state space traversals can be performed. Since evolutionary algorithms can be quite computationally intensive, a major portion of this effort focuses on the development of efficient mutation and crossover operations.