Testing and verification by exploring circuit properties

Continuing advances in semiconductor technology have made possible the development of very large system-on-a-chip (SOC) VLSI circuits, in which a density of 100 million transistors on a single chip and a on-chip frequency of more than 1 GHz will be a reality. Nevertheless, it is impossible to build such systems without error and defects introduced during the design and manufacturing process. Testing and verification have become the bottleneck of the time-to-market for launching next generation system-on-a-chip VLSI circuits. This thesis addresses the problems in developing efficient and scalable algorithms for testing and verification of large VLSI circuits.; The first half of this thesis contains two works on property-based sequential test generation. One uses spectral techniques and the other uses logic-simulation. They both follow the idea of exciting certain properties of the circuit for fault detection rather than the traditional path-sensitization idea. Experimental results have shown that both test generators achieve performance (high fault coverage and short execution time) that is comparable and in some cases better than the current state-of-the-art test generators.; The second half of this thesis presents two works on applying Automatic Test Pattern Generation (ATPG) to property-based verification. We first apply a simulation-based ATPG to safety property-checking. Then we propose a novel success-driven learning algorithm that gives a combinational ATPG engine the ability to compute preimages. This is one of the key steps in formal verification. The algorithm effectively pruners redundant search space due to overlapped preimages and constructs a BDD data structure on the fly. This work is original in the sense that, all the preimage computation so far in formal verification has been exclusively based on ROBDD and in return suffers from space explosion; this is among the first work that applies a pure ATPG engine to compute preimages so that the memory explosion problem is tremendously reduced. It makes possible an unbounded model checking framework powered by ATPG (or SAT-solver).