Research On Methods For Formal Verification Of Vlsi Circuit

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. Extensive simulation, the traditional approach is no longer adequate, because it is too time-consuming and it gives no absolute guarantees about the correctness of the design. 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.In this dissertation, the algorithms about formal verification are investigated. With lots of previous work on formal techniques for verification on large digital design, algorithms for combinational equivalence checking (CEC) and sequential equivalence checking (SEC) are presented and implemented. The main contents are as follows:Combinational circuit verification is an important aspect and foundation of formal verification of digital integrated circuits. A new combinational equivalence checking approach integrating Binary Decision Diagrams and Boolean Satisfiability is proposed in this dissertation. The algorithm works on the representation called And/Inverter Graph of the circuit, the BDD's propagation and Circuit-based SAT Solver are applied alternately to reduce the space of the miter circuit. If failed, CNF-based SAT Solver is used to solve the problem. The Algorithm combines the advantages of both BDD and SAT.Memory explosion is a boring problem while using BDD to verify. We focus on that the modification and optimization in design flow have a limited effect on the structure of a circuit. Therefore a lot of equivalent signals exist between conference circuit and implement circuit. As to this character, we proposed an effective cut based algorithm. Different from previous cut based methods, the algorithm takes in static cut's efficiency while dealing with multi-pairs of signals and dynamic cut's availability while dealing with one pair of signal. Compared with those cut based methods, this algorithm is faster and effective.Sequential circuit checking is more difficult than combinational circuit checking, especially to circuit with more latches. One of methods to decrease the complexity ofthe problem is using combinational technique by latch mapping. In the dessert, a new latch mapping technique for sequential equivalence checking is proposed. The algorithm combines random simulation, local BDD and target simulation to do latch mapping. Random simulation gives the initial match result rapidly. Techniques of local BDD and target simulation refined the result.Traditional formal method to verify sequential circuit is based on BDD and State traverse, such is prone to state explosion when state space increases. In this dissertation, a method that uses local BDD and symbolic backward justification is introduced. The algorithm takes Assume-And-Then-Verify as a strategy, and combines existing technique like cut and circuit structural similarity exploration, takes advantage of combinational checking technique. Besides these, some speedup skill is also described. The approach is much less vulnerable to a memory explosion than the traditional symbolic FSM traversal and is more suitable to check between two large scale sequential designs with more structural similarity.