| The problem of Boolean Satisfiability (SAT) is not only of theoretical importance in computer science but also is of interest in practical applications. Since the first search algorithm, known as DPLL algorithm, was provided in the 1960's, active research in this area has resulted in state-of-the-art SAT solvers that can handle large practical problems. SAT problems widely exist in electrical design automation (EDA) areas such as equivalence checking, model checking, and automatic test pattern generation (ATPG). In these areas, SAT problems are usually represented by circuit models and are called as circuit SAT problems. The rapid increase of design complexity demands more and more efficient circuit SAT solvers. Based on different circuit models, circuit SAT problems can be classified into combinational SAT problems and sequential SAT problems. In this thesis, we first present our combinational circuit SAT solver. In our solver, signal topological ordering and signal correlations are utilized to guide decision-variable selection and incremental SAT solving. Signal correlations can be derived by random simulation and used to generate sub-problems. The generated sub-problems are solved following the topological order from inputs to outputs. The learned information (i.e. conflict clauses) in solving a sub-problem is utilized to simplify the circuit model and reduce the search space of other sub-problems, including the original problem.; Although great success has been achieved in solving large practical combinational SAT problems, solving sequential SAT problems remains a challenging problem. The challenges are from state-space explosion and deep sequential depth. We extend our combinational circuit SAT solver into a sequential SAT solver that adopts a complete backward-search algorithm. Several techniques, including solution state reduction, objective state reduction, priority-based search strategy, and implicit time-frame expansion, are provided to address these challenges.; Bounded model checking (BMC) and inductive invariant checking (IIC) are two important techniques for addressing sequential SAT problems. They are incomplete, but complement the backward sequential search algorithm in our sequential SAT solver. In this thesis, several techniques are provided to simplify the computation models in BMC and IIC, and thus, improve their performance. We also present a sequential equivalence checking (SEC) framework which integrates BMC, IIC, and the sequential SAT solver to target for SEC problems. Experimental results demonstrate the effectiveness of this framework for large SEC benchmarks. |
