Research On The Formal Verification Of ASIP Architecture Level Design

Application Specific Instructions Set Processors(ASIP) is a kind of special processor designed for a particular type of applications.With the continuous development of ASIP design,the complexity of the design is also increasing,and the verification efforts on the correctness of design are increasingly prominently accordingly.Due to the diversity of instructions' behaviors and the flexibility of logical structures,it is very difficult to build a general method to verify the correctness of the ASIP design automaticly.So far,there is not any effective theory and methodology on the automatic verification of ASIP design at architecture level.On the problems mentioned above,the hierarchy characteristics of ASIP architecture design were analyzed deeply.A framework on the verification of ASIP architecture design,which is based on Petri Net and Model Checking theory and methodology,is presented in this thesis.The properties which an ASIP design needs to satisfy are divided into static properties and dynamic properties.Static properties are used to specify the requirements of structure and individual instructions' execution,while dynamic properties are used to specify the requirements of concurrent instructions.The main research works include:(1) Description of the ASIP architecture based on Petri net.Hardware Design based-on Petri Net(HDPN),an extended Petri net,is used to describe the structural and behavioral characteristics of ASIP architecture.The static properties which an ASIP design should obey are also proposed.(2) Verification of the dynamic properties based on Model Checking.Firstly, the model of ASIP architecture to be validated is constructed,and the dynamic properties which a processor should obey are extracted from customer-built requirements.Then model checker is used to check the consistency of the model and of the properties.The method is applied to a pipeline processor and an out-of-order processor to prove the availability.(3) Modeling method based on the hierarchical and local characteristic of ASIP design.In order to efficiently verify the design,the models' scale should be restricted.Two kinds of models,global design and local models are constructed in this method.The global design,in which many details are hidden to reduce the scale of the model,is used to check the validity of the interaction between the components. While local models,in which concrete designs of each individual component are described,are used to verify detailed specifications.In this situation,the other parts of the design are treated as outer environment,and the interface parameters of the model are set as stochastic values in the possible range.(4) The translation rules from HDPN based description to model checker based description.Based on the translation procedure,a verification framework which supports the validation on the correctness of structures and instructions' execution of an ASIP architecture design is constructedThe main contributions of this thesis are as follows:(1) Aiming to the design of ASIP architecture,a novel extended Petri Net model named HDPN is introduced.It can describe target architecture in a succinct and precise way.In HDPN,tokens are endowed with concrete information according to the specific design,but not only a black dot in traditional Petri Net.Therefore the elements in the Places are added with types.And transitions,which are used to describe the function units,are appended with interface parameters,execution conditions and concrete action description.Arcs,which are used to describe data path,are also appended with parameters.To sum up,as a modeling tool,HDPN can sufficiently describe the structural information and individual instructions' execution of the ASIP architecture.The method based on HDPN,taking advantage of it,can efficiently verify the static properties accordingly.(2) Model checking is applied to the verification of ASIP architecture. Modeling method based on hierarchical and local description is presented and used to abstract models from a pipeline processor and an out-of-order execution processor. These modeling methods are effective to avoid state space explosion.The dynamic properties used to check the correctness of a processor execution are also proposed.(3) The translation rules from HDPN description to the input language of model checker-NuSMV are presented.Therefore,an integrated framework for ASIP architecture verification is built.The properties for the verification are divided into static properties and dynamic properties.They are checked through the static property checking method based on HDPN and dynamic property checking method based on model checking,separately.