Research On Formal Verification Method For VLSI Design

With the increasing complexity of very large scale integration(VLSI),the works for design verification is getting more and more arduous and difficult.For complex VLSI designs,the verification process accounts for about two-thirds of the entire design cycle,and the number of professional verification engineers in design process is about twice of that of design engineers.Functional verification has become bottleneck of VLSI design.Traditional software simulation and hardware emulation cost a lot of time,and can't guarantee the correctness of the function completely.as one of complementary approaches,formal verification has attracted the interests of people increasingly.Formal verification uses rigorous mathematical reasoning to demonstrate that the design meets all or parts of its specification within less time, which is a feasible approach to overcome the bottleneck of verification.In this dissertation formal verification methods for VLSI are studied thoroughly.The major contributions are as follows:1) For equivalence checking of data intensive circuits,a word WGL(W~2GL),the improved model of WGL model,is proposed.WGL model is limited to word-level arithmetic operations representation for which node is bit-level variable.W~2GL model can express word-level arithmetic operation effectively.It is proved that an ordered and reduced W~2GL is minimal and canonical,and the variable ordering method is proposed,and the addition and multiplication algorithms for W~2GL are presented in the dissertation.Using these methods and algorithms the ordered, reduced and canonical W~2GL models can be constructed to carry on equivalence checking between pre-optimized and post-optimized RTL circuits.Experimental results show that for equivalence checking of data intensive circuits,compared with *BMD and WGL model,W~2GL model has the obvious superiority in both memory storage and CPU running time.2) For equivalence checking of complex circuits containing arithmetic and logic operations of both word-level and bit-level,a hybrid WGL(HWGL) model is proposed in the dissertation,which is expanded from W GL model.W GL model can effectively express word-level arithmetic operation.However,it is necessary to split the word-level variables into the bit-level variables when W~2GL model express world-level logic operation,which makes the expression more complex.HWGL model can effectively express arithmetic and logic operations of both word-level and bit-level.HWGL models of complex circuits can be constructed to carry on equivalence checking between pre-optimized and post-optimized circuits.The construction of HWGL model is independent of word length,and need less nodes and time.Experimental results show that for complex circuits containing word-level and bit-level variables,HWGL is more advantageous than W~2GL and *BMD.3) For property checking problem,on the basis of HWGL model a branch WGL (BWGL) model is proposed in the dissertation.BWGL model is expanded from HWGL,in which variable node belongs to HWGL node and branch node,Union node and Intersect node are added.BWGL model is applied to property checking. The property of design is described as linear time logic,and different checking procedure is chosen according to time slice to verify whether the property is satisfied. Property checking method based on BWGL is compared with VIS system based on BDD.Experimental results show that for processor verification,property checking based on BWGL is more effective than VIS system,which can verify completely in less time and with less memory.Moreover,property checking based on BWGL can verify the data path and controller simultaneously,which can save a great deal of time.