Research Based On The Gste Theory Of Abstraction And Refinement

In recent years, due to the increasing scale of the circuit and the improving integration, very-large scale integration (VLSI) has become more and more complex, and the design process itself is difficult to ensure the logical design's correctness. At the same time, because the IC errors caused by design process make the loss enormous, and because of no repairing chip technology, it is impossible to amend VLSI errors, to design and build high-reliability integrated circuit system has become a key issue. As an important part for guaranteeing the design properly, the certification is playing an important role increasingly, and raises more and more attention and interest. The subject based on the theory of GSTE, researches abstraction and refined technology to deal with the application of the theory, wishes to resolve the efficiency caused by the abstraction as well as the reunification issue of verifing the accuracy, do the differential abstraction for the variable set by the variable division technology in order to reduces the state space, use the parameterized state space to compress processing in order to effectively expess the state of the relevant variables set. Apply BDD technology to implement GSTE theory authentication algorithm.As the formal verification method is based on the searching state approach, there is problem of limited processing capacity, and it can not verify the large-scale electronic circuitry. At present, abstraction and refinement processing introduced by most formal verification tools, deal with the state explosion problem. In research methods, firstly, describe new formal verification methodes to address the state explosion problem, and analysis their ideas and problems of the methods briefly. Secondly, learn how to model verifing the circuit for the formal verification method, and focuse on understanding the current main formal verification methods: STE and GSTE, analysis their definition of the circuit model and the specification verified respectively, as well as validation of their authentication algorithm, according to their principles and methods of simulation verification, analysis their strengths and weaknesses, compare and analysis among them. Understand the abstraction treatment methods furtherly, as well as symbol processing techniques of the circuit; and analysis the abstract processing and refinning processing of STE and GSTE. Though the above theoretical study and analysis, in this paper, imposes the improved algorithm based on abstraction processing and state parameters representation of GSTE and in the process of verification, divides the variable of the certification specifation, only verifies assertion-related variables so that it reduces the number of states effectively. At the same time, in the verification process, introduce the paremetic method to express the state space effectively and compress the state space as much as possible. Apply the BDD technology to implement GSTE authentication algorithm. Adoptions of these technologies improve capabilities of the GSTE simulation verification processing effectively, as well as its verification process.