Research On Model-based Equivalence Checking And Inconsistent Diagnosis Combined With Satisfiability

With the increment of the scalability, the growing of the complexity and the pressingdemand for the time to market of the integrated circuit, ensuring the correctness of theintegrated circuit design is getting much more difficult. SATisfiability(SAT), as a outstandingsearch engine, has been widely used in a series of significant issues in the field of IntergradedCircuit (IC) industry, such as placement and routing, Automatic Test Pattern Generation(ATPG), logic synthesis, equivalence checking, design error diagnosis, fault diagnosis, etc.Boolean satisfiability problem, the first one that was found to be a classic NP-completeproblem, occupies an important position in the fields of Artificial Intelligence, ComputationalComplexity and etc. Many remarkable universities and research institutions of IC industryhave invested substantial resources on the research of SAT problem, and have promoted arapid development in the field of Boolean satisfiability, which also result in an indirectpromotion in a better resolving of the problems that rely on the applying of SAT techniques.This paper is focus on the SAT problem based on the Extension Rule, and explores how toefficiently apply the SAT technique in the equivalence checking and Inconsistent Diagnosis.The work of this paper is introduced in the following.Through the study of the SAT techniques based on the Extension Rule, we proposed amethod based on the Semi-Extension Rule, which improves the efficiency of solving thesatisfiability problem. The Satisfiability Problems is one of the most important problems inthe field of Artificial Intelligence. The Resolution-based method is to try to deduce the emptyclause to check the satisfiability of a clause set, while the Extension rule-based proceedsinversely to resolution, which tries to deduce the set of all the maximum terms to checksatisfiability. After a deep investigation on the extension rule, the concept of Semi-ExtensionRule (SER) is proposed, and a Semi-extension rule based algorithm so-called SER ispresented. The method determines whether the maximum term clause can be expanded by theclauses according to a certain order. If one of the maximum term clause can be expanded by acertain clause, then all the maximum term clauses semi-expanded based on this clause neednot have to determine its expandability, thus reduced the number of maximum term clauseneed to determine. This method fully used the advantage of the extension rule to circumvent the complex solving process using the inclusion-exclusion principle; and fully used theadvantage of whether the maximum term clause can be expanded from the clause of theclause set using algorithm Novel Extension Rule (NER), and moreover, expansion based onsemi-extension rule avoids the necessary of determining all the maximum term clause beforewe get the final result.The introduction of cut-point is a breakthrough in Formal equivalence checking method.However, the method using cut-point is incomplete and may bring false-negative. So far, therehaven't been efficient methods to eliminate the false-negative, and no methods aiming ateliminating the false-negative in the formal equivalence checking on System Level Model(SLM) and Register Transfer Level (RTL) either. Therefore, investigation into the eliminationof false-negative is indispensable, which can improve the efficiency of equivalence checkingand reduce time to market.The current methods of eliminating the false-negative have the disadvantages mainly on:(1) Their efficiency is not high, which is the same as not introducing the candidate equivalentnodes in the worst case.(2) They would have better efficiency only under some specificconditions.(3) Introducing heap structure or adding the corresponding constraint has greatlyaffected the efficiency of the verification.(4) The limitation in the expression power oroperational capability has restricted the scale that these methods can be applied.(5) Theycannot be well used in the elimination of the false-negatives in the equivalence checking onSLM and RTL.For the shortcomings of the methods in eliminating the false-negatives presented above,this paper presents a method to eliminate the false-negative combined with constraintsatisfaction. The major advantages are (1) This method can be applied to the false-negativeelimination in the equivalence checking of RTL vs RTL and SML vs RTL.(2) This methoddirectly calls the constraint solver to eliminate false-negative without additional auxiliarystructure added.(3) When eliminating the false-negatives, the method can choose whether tocall the bit-level constraint solver or the word-level constraint solver, which greatly improvesthe efficiency of equivalence checking.(4) The scale of the problem that can be solved hasconsiderable improvement due to the adoption of the bit-level or word-level solver.The inconsistency diagnosis in Integrated Circuit is an important research subject anddifficult problem as equivalence checking. We present a Dynamic Semi-Extension Rule(DSER) SAT algorithm for dynamically judging whether a component set is consistency-based diagnosis in model-based diagnosis. Firstly, the model of the system to be diagnosedand all the observations are described with conjunctive normal forms (CNF), and the problem of diagnosis is translated into the satisfiability of the related clauses in the CNF files. Next, allthe minimal consistency-based diagnostic sets are derived by calling DSER dynamicallycombining with the improved (Set Enumeration Tree) SE-Tree.Moreover, in order to improve the efficiency in inconsistency diagnosis, we present themethod computing diagnosis with flag propagation and the method hitting set with dynamicmax degree. Firstly, we present the concept of the component output flag, then whether acomponent set is a diagnosis or not can be driven through the propagation of output flag in thesystem. It can compute all the minimal diagnosis directly, without computing all the conflictsets and therefore the hitting sets of the collection of the corresponding conflict sets like theclassical methods; Secondly, this paper presents the concept of degree of un-extended element,and extends the node of SE-Tree in accordance with the descending order of degree ofun-extended elements. With this extend order, we not only can generate hitting set early, butalso can reduce the number of generated nodes. Next, the definition of degree of node is given,which determines whether the set of node is diagnose or not directly, and avoid the computingof hitting set.