Refinement Based On Gste Verify

With the increasing complexity and tight time-to-marker 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 methods are applied to actually construct a mathematical proof for the correctness of the design. So it can improve the verification's correctness and assure market requirement. In addition, formal verification, as one of complementary approaches, has been put forward to solve these problems.With lots of previous work on formal verification on large digital IC design, study and extend GSTE method which is one of the currently most important formal verification methods deeply to reduce the false negative further and improve the correctness by using GSTE method in integrate circuit verification.On study methods, the paper introduces the basic theory and technology of STE verification algorithm and analyzes the strongpoint and shortage in detail. For extending STE verification specification using graphical theory, introducing the concept of assertion graph and implement assertion based verification algorithm, the paper analyzes them in detail. Then import concept of the GSTE and compare the advantages and weaknesses between STE and GSTE. GSTE inherits the abstract behavior of STE. It means it takes with the false negative problems. The paper analyzes the reason that makes the false negative problems and puts forward an improved algorithm on GSTE's SMC algorithm. At last use FORTE to verify the improved algorithm. The result shows the improved algorithm make progress in reducing the false negative and checking fault. If someone is not familiar with the circuit, they can use the improved algorithm of GSET to verify the circuit correctness. For others, they can extend the loop by hands.At the same time, for the automation of the verification tool, bring forward a way named automatic insertion of fault tolerant. We notice that in the practical designing flow, if the verification returns fault, for the persons who have not taken part in the design, how to find the designing fault and mend them is very difficult. However, the modification of most designing circuits is only to modify a part of the circuit structures. How to resolve the problem more efficiently and detailed is the challenge to make sure the correctness of the circuit designing.