Evolutionary Algorithms for Symbolic FSM Equivalence Checking

集成电路（IC）正变得越来越复杂，市场需求不断迫使设计人员在更短的时间内生产新的IC。 由于这些原因，有兴趣使用verificationmethods，使设计师能够确保其产品的正确性，而无需诉诸耗时的仿真技术。 验证的两种方法是等价性检查和模型检查。 在内部，在这两种方法中，通常使用用于检查有限状态机（FSM）的等价性的方法ASM等价性检查通常通过使用符号状态空间可达性算法来实现，该符号状态空间可达性算法使用BDD数据结构和可满足性（SAT）算法。虽然近年来在符号FSM机器状态空间遍历方法中已经有了进步，但是由于过渡关系（TR）BDD变得太大，表示已经遍历的状态空间的BDD变得太大，图像计算期间的中间BDD变得太大，并且，整个过程需要太多的计算时间。进化算法最近已被应用于设计自动化中的几个问题。 这个研究项目涉及使用进化算法进行精确和近似FSM等价性检查的调查。 正在开发的进化算法，修剪TR和可达状态BDD，使准确的，过近似或欠近似状态空间遍历可以被执行。 由于进化算法可以是相当计算密集型的，这方面的努力的主要部分集中在有效的变异和交叉操作的发展。

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.