Equivalence Checking And Test Generation Using Boolean Satisfiability

With the development of modern and efficient Boolean Satisfiability (SAT) algorithms in recent years, SAT has increasingly made a significant impact on electronic design automation (EDA) applications. In this thesis we investigate the application of modern SAT engine for the equivalence checking and test pattern generation problems.The original contributions of this thesis are as follows:1. Efficient combinational equivalence checking using output grouping and circuit SAT. As the chip size and complexity dramatically grows, functional verification has become the main botterneck in IC design flows. Today's large, complex designs often require an inordinate amount of time and computation resources to verify using traditional simulation technique alone. An alternative for some verification tasks is to use combinational equivalence checking. A new combinational equivalence checking technique combining output grouping and circuit SAT was introduced in the thesis. And/Inverter structural hashing technique was used to simplify the miter circuit first. The algorithm use our proposed heuristic to do output grouping for complex problems, and thus the equivalence checking problem can be converted into some circuit SAT problems, circuit SAT solver was used to solve these sub-problems. To reduce the search space, useful learning information of some sub-problem was shared. Experiment results for some larger verification tasks demonstrate the proposed algorithm's efficiency.2. Sequential Equivalence Checking using invariant extraction technqiue and sequential SAT solver. One significant limitation of combinational equivalence checking is its requirement that two designs under verification have corresponding flip-flops. Synthesis tools may often apply sequential optimizations such as retiming to complex designs and hence destroy the correspondence between flip-flops in both the reference and implementation designs. Checking the equivalence of such designs should be carried out using sequential equivalence checking. We propose a sequential equivalence checking framework by integrating invariant checking and sequential SAT alternately. To explore the structural similarity, some invariants in the miter circuit are identified in advance, and the search space can be dramatically reduced by constraining these generated invariants. An enhanced invariant checking method that combines timeframe expansion and dynamic candidate selection strategies is proposed. What's more, a heuristic for quickly finding counter-examples of in-equivalent tasks is introduced, it can solve some hard-to-detect problems with long solution length that are typically failed when bounded model checking tool is used. The efficiency of the approach is shown through its application on the ISCAS89 circuits and some hard-to-verify industrial circuits. The experimental results show that this work holds potential for sequential verification of large-scale circuits.3. Sequential automatic test pattern generation using an enhanced miter model which allows reuse of learned clauses for different faults. Automate test pattern generation (ATPG) for sequential circuits remains one of the most computationally difficult problems in EDA areas. It has been observed that the hard-to-detect faults often consume most of computational resources in running a traditional sequential ATPG tool. This thesis presents several ideas on more effective application of Boolean Satisfiability techniques to the sequential ATPG. We first propose an enhanced miter-based model, which can increase reusability of learned computational information by simultaneously injecting a set of target faults in a single miter circuit, instead of building a separate miter circuit for each fault. The use of this model dramatically improves the ATPG efficiency using a sequential satisfiability solver. Furthermore, detecting untestable faults now is only a byproduct of SAT solving. Some recent techniques developed for SAT-based sequential equivalence verification can also be modified and integrated to further improve the engine's efficiency for sequential ATPG. The experimental results show that our method can improve both fault coverage and fault efficiency, and its especially useful for solving those hard-to-detect faults which aborted by using the traditional sequential ATPG tool.4. Diagnostic pattern generation that supports multiple faults with possibly different fault types. We also present an efficient diagnostic test pattern generation (DTPG) framework based upon a Boolean Satisfiability engine. The model used in sequential ATPG is further extended for DTPG application. With this modeling technique, learned information during DTPG for different fault pairs can then be naturally shared without any computational overhead and thus significantly improve the DTPG search efficiency. We also propose a model for DTPG of multiple faults with possibly different fault types, including static and dynamic faults. To reduce the diagnostic pattern count, we further introduce a compaction heuristic by exploring "don't cares" at the primary inputs. We demonstrate experimental results which indicate that the proposed DTPG models and methods can significantly enhance the diagnosis resolution.