Formal Verification of Large Sequential Systems Using Success-Driven ATPG

针对目前基于二叉决策图(BDD)的方法所无法实现的大规模时序电路状态集的一步前像计算，提出了一种新的基于ATPG(自动测试模式生成)技术的新概念和新基础。这是因为ATPG发动机不容易受到空间爆炸问题的影响，因此基于ATPG的技术可以适用于非常大的设计。然而，前像的计算将以一种以前不需要的方式扩展ATPG-它们必须转向所有解决方案，而不仅仅是一个解决方案。换言之，即使最先进的ATPG能够有效地找到一个解，但简单地让它们继续搜索所有其他解将导致时间爆炸，其中将需要指数时间来计算完整的前像。为了解决这一问题，需要一种新的ATPG算法来智能地剪枝由于解重叠而产生的冗余搜索空间。通过这样做，这种新的方法可以显著加快搜索前像计算所需的所有解的速度。一旦可以有效地执行前像计算的构建块，它就可以自然地插入大型顺序系统的形式模型检查和等价检查引擎中。这项研究涉及以下相关问题：(A)识别先前探索的包含解的空间；(B)修剪仅包含冲突的空间；(C)以紧凑的形式组合多个解；以及(D)迭代计算过程以获得多个周期的原像。由于本研究提出了一种隐式状态空间遍历的新方法，为大型复杂时序系统的设计验证提供了一个全新而有效的维度。

The objective of this research is on developing a new concept and foundation for efficient one-step preimage computation for sets of states in large sequential circuits based on novel automatic test pattern generation (ATPG) techniques, where current binary-decision-diagram (BDD)-based approaches fail. This is by taking the advantage that ATPG engines are not vulnerable to the space explosion problem, and thus the ATPG-based techniques can be applicable to very large designs. However, computation of preimages will stretch ATPGs in a way that they were not required before - they mustreturn all solutions instead of merely one solution. In other words, even though the state-of-the-art ATPGs are efficient in finding one solution, simply making them continue to search all other solutions will result in temporal explosion, in which exponential time will be required to compute the complete preimage. To remedy this problem, a new ATPG algorithm that intelligently prunes the redundant search spaces due to overlapping solutions is needed. In doing so, this new approach can significantly accelerate the search for all solutions necessary for preimage computation. Once the building block for preimage computation can be efficiently performed, it can naturally be plugged into formal model checking and equivalence checking engines for large sequential systems. This research addresses the following relevant issues: (a) identification of previously explored spaces that contain solutions; (b) pruning of the spaces that only contain conflicts; (c) combination of multiple solutions in a compact form; and (d) iteration of the computation process to obtain preimage for multiple cycles. As this research brings about a new approach via which implicit state-space traversal can be performed, it offers an entirely new and effective dimension to the design verification arena for verifying large and complex sequential systems.