Research And Application Of Verification Method For Peripheral Controller Based On Model Checking

In the financial sector,the embedded product becomes more and more complex and more widely used,but the stability of embedded products has not been effectively resolved,so there will be a security risk in the normal financial transactions,which tend to give people the inconvenience in daily financial transactions or even loss of property.In order to solve this problem,this paper analyzes and studies the verification method of peripheral controller based on model checking,and improves the stability of embedded products to the maximum extent,which has certain application value.The main work of this paper is as follows:The hardware design verification method and the research sta tus of the model detection at home and abroad are summarized.The related technologies of hardware verification methods are studied,including verification methodology analysis,key technologies based on SystemVerilog verification,and related technical an alysis of model checking hardware verification.Model detection modeling method research.Including the transformation of state model use case model,state model into nuSMV model research method and transformation rules;research on the design method of mo del checking attributes,including attribute extraction method,attribute decomposition method,and the design method of the property;finally,the example analysis,with the actual development project of a currency-counting machine as a platform,contact type image sensor controller for use case modeling,state modeling,nuSMV modeling,using model checking to verify and produce counterexamples,a counterexample modify contact image sensor control device,the final design of a contact type image sensor con troller with good stability.The research of model detection attribute design method.The forward extraction method and the reverse extraction method are put forward to solve the problem that the system attribute extraction is not comprehensive enough,the state explosion causes the sharp increase of attributes,and the problem of attribute description can not be achieved.The CIS(Contact Image Sensor,contact image sensor)controller is designed and verified.Use case modeling,state diagram modeling,unS MV modeling,Verilog modeling for the CIS controller,a method based on model checking to verify,design modifications according to the model checking tool provides a counterexample,until the design meet the requirements,solve the instability,image acqu isition in the actual project and the problem of poor quality.This thesis designed by using contact image sensor controller to complete the verification method based on model checking,to solve the contact image sensor image acquisition controller unstable project,poor image quality problems in the fields of hardware design verification based on model checking will be used more and more.