Search algorithms for satisfiability problems in combinational switching circuits.

Abstract

A number of tasks in computer-aided analysis of combinational circuits, including test pattern generation, timing analysis, delay fault testing and logic verification, can be viewed as particular formulations of the satisfiability problem (SAT). The first purpose of this dissertation is to describe a configurable search-based algorithm for SAT that can be used for implementing different circuit analysis tools. Several methods for reducing the amount of search are detailed and integrated into a general algorithmic framework for solving SAT. Special emphasis is given to the description of methods for diagnosing the causes of conflicts that may be identified while searching for a solution to each instance of SAT. These methods allow the implementation of non-chronological backtracking, conflict identification based on equivalence relations and logic value assertions derived from conflicts. Path sensitization in combinational circuits is often used to solve test pattern generation, timing analysis and delay fault testing problems. While path sensitization can be cast as an instance of SAT, such an approach can conceal desirable structural properties of the problem and may lead to exponential size representations. Another purpose of this dissertation is to introduce a new model for path sensitization that permits modeling test pattern generation and timing analysis with linear size representations. In addition, this formulation for path sensitization permits the adaptation of all the pruning methods developed for the general SAT problem. The proposed SAT algorithms and path sensitization model form an initial kernel for the development of tools for the analysis of combinational circuits. Their practical applicability is supported by experimental results obtained with test pattern generation and timing analysis tools.