Formal Verification of Large Sequential Systems Using Success-Driven ATPG

Virginia Polytechnic Institute And State University, Blacksburg VA

Investigators

Abstract

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 must return 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.