A Research For Functional Modeling Of Module Which Changed Parallel Signal To Serial With Different Model Checking Technologies

Analog verificationation technology is used in traditional industrial circuit verification which the results of verification are directly related with its choice of test vectors. Because of the increasing of circuit’s scale, how to select the right test vectors is harder and harder, and the test coverage is getting lower and lower. In recent years,formal verification techniques gradually become a hot research. It uses mathematical methods rather than the test vectors in traditional analog verificationation, and to achieve verification purposes, it uses specification which is specifying the property of the circuit, model of the circuit and translation. The characteristics of formal verification is it’s faster, full coverage of test and so on. However, because of the state explosion problems, the verified scale of formal verification is not large. It currently can’t meet the requirements of industrial LSI ’ s verification, and only universities and labs of large companies use it as a research.In this paper, both temporal logic model checking techniques and GSTE technology are used to verify the properties of a real industrial circuit provided by Changhong company. According to the study to verification of the real industrial circuit,this paper aims to explore if formal verification techniques could be used to the practical industrial applications.Firstly, a brief introduction about the traditional analog verificationation technology and formal verification techniques are given, and the advantages and disadvantages of both are compared. Then it gives a detail introduction to the GSTE algorithm and temporal logic used in the paper. In the part of GSTE, the paper focuses on its concept of model, assertion graph and strong satisfiability; in part of temporal logic, the paper firstly introduces the related contents of LTL, then leads to the introduction of the rules of CTL, a compared about the difference and interworking points is given in the end of this part. All of these introductions provide a theoretical basis for the later.Before the beginning of verifying, the paper firstly gives an introduction to the related verification tools: VIS and Whale. And as case studies, it uses Counter and FIFOto show how to extract properties, how to build the CTL formula and assertion graph,and how to use tools to verify.For the module of Changhong, it firstly presents the features and the standards of internal implementation, and then according to the standards of implementation, it extracted four typical properties. At last, through the analysis of the relevant points of the properties and the law of some properties expressed in the module of Changhong,we use both temporal logic model checking technology and GSTE technology to verify all the properties, and build the CTL formulas and assertion graphs. For some properties mentioned in the paper, it verified from both positive and negative proposition which enriched the means of verification. At the end of this paper, both technology used in the paper are compared form many aspects.