Verification Technology Of Equivalence Between Model And Verilog Code Based On Formal Method

With the rapid development of IC technology,IC chips have been integrated into all aspects of our lives,which has a great impact on the people’s livelihood,science and technology and military of all countries.The whole integrated circuit industry can be divided into two parts: industrial software industry and hardware manufacturing industry.The first step of IC design using industrial software is to describe the function of the circuit model by Verilog HDL.However,with the rapid increase of the scale of the integrated circuit,the Verilog program is more complex and it is more difficult to ensure the correctness of Verilog program.If the design is continued according to a Verilog program which does not meet the expected requirements of the circuit model,the integrated circuit manufactured will not meet the requirements.Therefore,it is necessary to verify the equivalence between the circuit model and the Verilog code.Formal verification is a popular technology to verify the equivalence in IC design.Its principle is to describe the properties of the circuit model by using the sequential logic language with formal semantics,and then use formal verification tools to detect Verilog program.PPTL is a formal logic system with full regular expression ability,which can easily describe the sequence,parallel and cycle repetition of the model.Based on PPTL,the runtime verification tool UMC4 M is developed.MSVL is a formal verification language based on PTL,which is a projection timing logic.It has the characteristics of rich syntax and high efficiency.And the existing V2 M converter can convert Verilog program into MSVL program with the same semantics.This paper presents a formal verification method based on pptl and MSVL to verify the equivalence between the circuit model and Verilog code in integrated circuit design,and the reliability of the verification method is proved by verifying several circuit model examples.The main work of this paper is as follows1)Through the research of PPTL and MSVL,a formal verification method based on PPTL and MSVL is proposed.On the one hand,the method describes the properties to be verified in the circuit model by using PPTL formula,on the other hand,the Verilog program is converted into MSVL program with the same semantics,and then the runtime verification technology is used to verify the satisfaction of MSVL program to PPTL formula.2)The paper studies how to extract the related properties from the combined logic circuit model and the sequential logic circuit model and describe it as PPTL formula.The key point of this method is property extraction.Only accurate and complete description of the circuit model properties into a standard PPTL formula can the reliability of the verification be guaranteed.3)Several circuit models are designed and implemented.Then,the equivalence of the circuit model and Verilog code is verified by the above verification method,which proves the feasibility of the verification method.