Study On The Formal Verification Methods In BDD And SAT

With the increasing complexity and tight time-to-market schedules of today's digital, verification is becoming more and more difficult. The report in International technology roadmap for Semi-conductor 2003 has pointed out, that verification has been the bottleneck in the IC design flow. The traditional extensive simulation is no longer adequate, because it is too time-consuming and it gives no absolute guarantees about the correctness of the design. In the past twenty years, people have found a new method—formal verification. It is a hopeful method for the design verification of VLSI. Formal verification means the process of verification is mathematical, and not as simulation technology which is experimental. Mathematical verification conquers the insufficient of simulation for completeness, and can reduce time for verification. Formal verification is the automatic verification for circuit description, and can reduce the complexity of verification.Formal verification as one of complementary approaches has been put forward to solve these problems. The key characteristic of this approach is that formal methods are applied to actually construct a mathematical proof for the correctness of the design.The dissertation gives the study of Binary Decision Diagrams and Boolean Satisfiability algorithms in formal verification method. The dissertation improve on Boolean Satisfiability algorithms,and gives the DC&DS algorithms. The paper gives equivalence checking algorithms in combinational circuit basing on SAT, the arithmetic integrates the strongpoint of BDD and SAT, by restricting the size of constructing BDD, avoids EMS memory exploding .And reasoning minishes searching space of SAT. And apply this new algorithm in formal verification method basing on BDD-SAT.Theoretical research and experimence results have proved the correctness of algorithms and design methods proposed in this dissertation.