Research On Formal Verification Methods For Integrated Circuit Based On PSA

Today’s society is a world which people have to face a lot of information, What helpspeople to deal with those information is the industry of the integrated circuit(IC), It is a greatchallenge of the design in the IC that the systerm must to meet to the use’s demands. In theflowing of the design of IC, How to ensure the IC’s complentment and correntment of thechip’s functiong is more and more a key point. The verification methods which currently usedin the industry of IC are not meeting the demand of the design work. It has more importantsignificance that we can ensure correntment of the IC in the errly phase of the flowing ofdesign. Because the formal verification mathods have the fearures, One it can abstract the IC’sfunction at high level. Anther it has a good description of the model of the IC. It is especiallysutable for the work of verification in design of early phase. Research on formal verificationmethods have the actual significance. In this paper, We based on the polynomial symbolicalgebra to study on those problems, Especially major to the arithmetic intensive digital IC wedo some work:(1) In order to achieve model checking of the digital chip, We propose a method of thebound model checking(BMC) based on the polynomial theory. In that method, First, We givean unified description for the circuit function based on the polynomial theory. In order todescription the circuit function with the the polynomial theory, We develop the traditiondescription method of the control logic of the circuit. We use the polynomial to representationthe atomic proposition and transform the boolean characteristic function into a set ofpolynomial. So, We can describe the circuit function with the polynomial. Secend, We give arelation model about the high level language. With the model we transfer the designspecification to the description with the relation model, and extract the target property, and awe get the description of the property with polymomial. At the same time, We get an unifieddescription with the polymomial about the he circuit function and target property. Based onthose two points, we can tramsfer the tradition BMC problem into a problem of the theoremproving, and with calculating the set of polynomial’ well triangular column to solve thetheorem proving. The method in the thesis can do BMC direct at the high level abstractcontrast the tradition method.(2) In order to verification the datapaths of the digital chip function’s equivalance which is between the RTL level description and optimized RTL description, We propose a newmethod about the datapath based on polynomial theory. First, We prove the equivalencerelationship between the zero set of polynomial sets and the equivalence of datapath. Theequivalence of the two datapaths mean that the circuit has a same output with the same input.When we see the circuit as a black box. So, We can see the solution set of polynomial as thepoint of a multidimensional space. Based on the theory of algebra cluster, We prove theequivalence relationship between the equivalence of datapath and the zero set of polynomialsets from the view of the algebra. Secend, We give the algebra method to judge the equal of thetwo zero sets of polynomial sets, And we use the theory of polynomial idea and the wellbehaved basid of the idea to judge that problem. Based on those two points, We propose theequivalence algorithm about the high level datapath.(3) In order to enhance the speed of the verification, We propose a module method aboutthe digital chip verification based on polynomial theory. First, We describe the structure of thecircuit based on a module form. Secend, We propose a method to calculate the function ofcircuit from the view of the module point. starting from the gate circuit or the circuitcomponent and get the structure information from the module description, We can recursivecalculate every circuit node’ function which have the form of the Grobner of the eliminatinideal about the polynomial ste based on the theory of the theory of eliminatin and expandment.At last, We get the the function of whole circuit. Based on those two points, We propose analgebra algorithm of the circuit verification based on module form.We build a experiment systerm with Maple and study those algorithms. The he result ofthe experiment shows that the verification efficiency of the method based an the PSA is betterthan the the tradition method towards the arithmetic intensive IC.