Based On Boolean Satisfiability Circuit Design Error Diagnosis

As today's VLSI designs grow in scale and complexity, errors become more frequent and difficult to track in the design process of integrated circuits. Many sophisticated verification algorithms and techniques exist that ensure the correctness of a design, and answer whether circuit implementation is equivalent with design specification. Verification includes circuit simulation and formal verification which in form of property checking and equivalence checking. All these methods only detect the existence of design errors, but could not tell reasons why the two circuits under checking are not equivalent. Unfortunately, although verification tools become more efficient and automatic, design error diagnosis and correction of digital circuits still remains a time consuming, resource intensive and manually conducted procedure.This thesis is mainly about SAT based design error diagnosis, and describes how to locate the source of errors in an erroneous implementation of design specification. Also a novel design error diagnosis method for combinational circuits is presented.Our approach does not incorporate an error model and, thus, is suitable for general types of design errors. It captures the circuit's logic error by a non-deterministic behavior of the component under model free condition. This thesis builds a hybrid semi-formal technique combined with traditional simulation based approach and multiple SAT solving technique. First it diagnose by a SAT solving procedure, then a small suspicious list is obtained for lighten burden of local error simulation with lossless any potential solutions. Only the signals that can correct every given erroneous input vectors are considered as a potential error source. An incremental SAT-based diagnosis method is proposed, which decomposes multiple error diagnosis into sub-problems with small error cardinality, so that a difficult problem is transformed to easy ones. Our approach is SAT based. Considering the difference of errors' cardinality related to every input test vector, we transform the diagnosis problem to a SAT problem by inserting extra strict or relax logical modules into circuit to build a constrained diagnosis configuration. We use a modified SAT solver as a computer engine to apply to circuit diagnosis field. We also improved the resolution and accuracy of diagnosis by ranking and screening sat solutions with structural information of circuits. A number of heuristics are proposed that keep the method's memory and run-time efficient. Experiments show that due to SAT based diagnosis guarantees to return a correction, so using formal techniques to direct simulation captures significant characteristics and improves the effectiveness and efficiency of the problem of diagnosis.