Based On The Mdd And Multi-value Gste Algorithm Of Multiple Variables

With the rapid development of LSI, electronic circuit design has been paid wideattention and has made some progress. But it still can’t catch up with the developmentpace of LSI and holds back the development of the electronic circuit industry. Thetraditional circuit verification could not meet the needs of LSI. In order to explore morerapid and larger verification algorithms and verification tools, formal verificationmethods come into being.This thesis does a lot of work on the research and implementation of generalizedsymbolic trajectory evaluation algorithm. It mainly achieves verification tools basedgeneralized symbolic trajectory evaluation algorithm. Among the existed verificationtools, both VIS developed by Berkeley and the popular cospan are all tools whichdescribe the nature of verification based on CTL and LTL language. However,generalized symbolic trajectory evaluation algorithm is a tool which describes thenature of verification based on assertion map. generalized symbolic trajectoryevaluation makes up for the defects existed in a number of verification problems offormal verification such as VIS and Cospan. This thesis designs a tool which makes upfor the blank where generalized symbolic trajectory evaluation algorithm is not used inthe field of formal verification and improves the types of formal verification tools. Thus,People have more choices in solving different problems and can choose a suitable toolto solve a certain problem by comparing the complexity of time and space.This thesis firstly gives a brief introduction of the background and history of thedevelopment of generalized symbolic trajectory evaluation algorithm. Second, give anintroduction of VIS verification tool, and introduces the verification tools designed byourselves, and then introduces the key and difficult problems in the implementation ofGSTE algorithm, as well as the innovation in studying and implementing verificationtools based on generalized symbolic trajectory evaluation algorithm. In the process ofcircuit design and verification, the most important thing is to find out whether the circuitdesign meets the requirements designers image. The generalized symbolic trajectoryevaluation algorithm uses the abstraction of the model and the nature to judge whether the model meets the nature of the method to verify the correctness of circuit design. Thecore of the algorithm is to find out the fixed point and the error points. If the algorithmfinds out the fixed point, the circuit meets the requirements designers mentioned. If thealgorithm finds out the error point, find out the error path according to the designedbacktracking algorithm and prompt the user to follow this path. In the process of thecircuit design, the results will appear which does not meet the designers.In the course of the study, there are still some problems existed in the discoverytools in solving some large-scale circuit. You will encounter some problems ofinsufficient time and space. These issues are also very difficult to be solved by today’spopular verifying software. The improvement of tool design technology and codingtechnology improvement can not solve this problem completely. To solve the problem,the basic method is the improvement of algorithm. If the improved algorithm cancontrol time complexity in the Polynomial time range, we can really complete LSIverification within a limited time. In the end, give the next improvement schemes andsuggestions based on generalized symbolic trajectory evaluation algorithm verificationtool so as to better improve the verification tool and well adapt to the developmentspeed of LSI.