Evolutionary Algorithms for Symbolic FSM Equivalence Checking

集成电路(IC)正变得越来越复杂，市场需求继续迫使设计者在更短的时间内生产出新的IC。出于这些原因，人们对使用验证方法感兴趣，这种方法允许设计者在不诉诸耗时的模拟技术的情况下确保其产品的正确性。验证的两种方法是等价性检验和模型检验。在内部，在这两种方法中，通常使用一种检查有限状态机(FSM)等价性的方法。FSM等价性检查通常通过使用使用BDD数据结构和可满足性(SAT)算法的符号状态空间可达性算法来实现。虽然近年来在符号有限状态机状态空间遍历方法方面取得了一些进展，但由于转移关系(TR)BDD变得太大、表示已经遍历的状态空间的BDD变得太大、图像计算过程中的中间BDD变得太大以及整个过程需要太多的计算时间，许多感兴趣的设计仍然无法使用该方法进行验证。该研究项目涉及使用进化算法进行精确和近似FSM等价性验证的研究。正在开发修剪TR和可达状态BDDS的进化算法，使得可以执行精确的、过近似的或欠近似的状态空间遍历。由于进化算法可能是计算密集型的，这项工作的主要部分集中在开发高效的变异和交叉操作上。

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 verificationmethods 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 FSMequivalence 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 beperformed. Since evolutionary algorithms can be quite computationally intensive, a major portion of this effort focuses on the development of efficient mutation and crossover operations.