Recent years have seen a dramatic growth in the application of SAT solvers to problems in electronic design automation. This trend is due in part to recent developments in SAT algorithms which have revolutionized the field of satisfiability testing. SAT has grown from a problem of academic interest to a core computational resource of immense value.; However, despite the significant progress in this domain there is considerable room for improvement in several areas. The goal of this dissertation is to advance the theory, practice and core technology of SAT algorithms in the context of EDA applications. The success of a SAT algorithm in a given EDA application may be ensured by a realistic quantitative assessment of the projected performance of the overall algorithm in a practical setting, by carefully orchestrating the use of SAT in the application and by improving the SAT algorithm per se. This dissertation addresses these three issues.; The first part of the dissertation presents a framework for analyzing the complexity of a SAT based formulation of the combinational ATPG problem, in a practical setting. We introduce the concept of cut-width of a circuit and characterize the complexity of ATPG in terms of this property. We present theoretical results and empirical evidence to argue that a large class of practical circuits can be expected to have cut-width characteristics conducive to an efficient solution of ATPG on them. These results also help to reconcile the intractability of ATPG, as predicted by traditional worst case analysis results, with the relative ease of solving practical instances of the problem.; The second part of the dissertation focuses on the optimum orchestration of SAT methods for a given EDA application. We revisit the application of SAT algorithms to the combinational equivalence checking (CEC) problem. We argue that SAT is a more robust and flexible engine of Boolean reasoning for the CEC application than binary decision diagrams (BDDs), which have traditionally been the method of choice. Preliminary results on a simple framework for SAT-based CEC show a speedup of up to two orders of magnitude over previous methods for SAT-based CEC. Further, the prototype implementation is only moderately slower and sometimes faster than a state-of-the-art BDD-based mixed-engine commercial CEC tool.; The third and final part of the dissertation is aimed at enhancing the core techniques used in current SAT solvers. We introduce the notion of problem symmetry in search based SAT algorithms. We develop a theory of essential points to formally characterize the potential search space pruning that can be realized by exploiting problem symmetry. We unify several powerful search pruning techniques used in modern SAT solvers under a single framework, by showing them to be special cases of the theory of essential points. We also propose a new pruning rule exploiting problem symmetry. Preliminary experimental results validate the efficacy of this rule in providing additional search space pruning over the pruning realized by techniques implemented in leading-edge SAT solvers.
展开▼
