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.