Lack of complete formal specification is one of the major obstacles to the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. Our coverage metric pinpoints the transitions through which the values of signals are checked. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

Transition coverage has been proposed as a measure of two-pattern test capabilities of TPG circuits for use in BIST. This paper investigates experimentally the relationships between transition coverages and actual stuck-open fault coverages in order to reveal what kind of circuits are appropriate for two-pattern testing. Fault simulation was performed using conventional (n-stage) LFSR, 2n-stage LFSR, and one-dimensional cellular automata (CAs) as TPG circuits and such sample circuits as balanced NAND tree and some ISCAS '85 benchmark circuits as CUTs. It was found that CAs which are designed so as to apply exhaustive transitions to any 3-dimensional subspaces can detect high rate of stuck-open faults. Influence of hazards of decreasing the fault coverage is also mentioned.

A method to design one-dimensional cellular arrays to be used as TPG circuits of BIST is described. The interconnections between cells are not limited to adjacent ones but allowed to some neighbors. Completely regular structures that have full-transition coverages for every k-dimensional subspace of state variables are first shown. Then, almost regular arrays which can operate on maximum cycles are derived based on fast parallel implementations of LFSRs.

A method to analyze two-pattern test capabilities of autonomous test pattern generator (TPG) circuits for use in built-in self-testing are described. The TPG circuits considered here include arbitrary autonomous linear sequential circuits in which outputs are directly fed out from delay elements. Based on the transition matrix of a circuit, it is shown that the number of distinct transitions in a subspace of state variables can be obtained from rank of the submatrix. The two-pattern test capabilities of LFSRs, cellular automata, and their fast parallel implementation are investigated using the transition coverage as a metric. The relationships with dual circuits and reciprocal circuits are also mentioned.