Evolutionary Algorithms for Symbolic FSM Equivalence Checking

集成电路（ic）变得越来越复杂，市场需求继续迫使设计人员在更短的时间内生产新的ic。由于这些原因，人们对使用验证方法感兴趣，这些方法允许设计人员能够确保其产品的正确性，而无需诉诸耗时的模拟技术。验证的两种方法是等价性检查和模型检查。在这两种方法的内部，通常使用一种检查有限状态机（FSM）等价性的方法。FSM等价性检查通常通过使用使用BDD数据结构和可满足性（SAT）算法的符号状态空间可达性算法来实现。虽然近年来符号FSM机状态空间遍历方法取得了一些进展，但由于转换关系（TR） BDD变得太大，表示已经遍历的状态空间的BDD变得太大，图像计算过程中的中间BDD变得太大，以及整个过程需要太多的计算时间，许多感兴趣的设计仍然无法使用该方法进行验证。进化算法最近被应用于设计自动化中的几个问题。本研究项目涉及使用进化算法进行精确和近似fsmequiquiality检查的调查。进化算法正在开发，以修剪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.