Formal Verification of Large Sequential Systems Using Success-Driven ATPG

本研究的目的是基于新的自动测试模式生成（ATPG）技术，在当前基于二进制决策图（BDD）的方法失败的情况下，为大型顺序电路中状态集的高效一步预像计算开发一个新的概念和基础。这是通过利用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.