Research On Techniques Of A Functional Point Model-based Semi-formal Functional Verification

Functional verification is the process that ensures conformance of a design under verification(DUV)to its specification.Due to the rapidly growing of information technology and complexity of hardware designs,functional verification has become the critical path in the hardware design cycle regarding development costs and time.Simulation verification and Formal verification are two major techniques of functional verification.As an alternative,the semi-formal method makes a tradeoff between simulation and formal method,so it overcomes the defects of simulation and formal verification and becomes more and more popular.The formal functional model is the base of the semi-formal approach.The semiformal methods can be divided into implementation-based semi-formal approaches and specification-based semi-formal approaches.The former ones derive the formal model from design implementation.This causes poor scalability and practicality.The latter ones derive the formal model from specification.This leads beter scalability and practicality.This paper concentrates on the study of the specification-based semi-formal approach,which contains modeling functionality of design,generation of test vectors,automatic checking the behavioral correctness of DUVs and functional coverage metrics.The main acheivements of this paper are listed as follows:1.We propose an entity-based functional point model and the correspondingestspace functional coverage and global FSM functional coverage.This functional model can describe the functional behaviors and inner entities of design.The model has the functional point layer and the entity layer.The functional point layer adopts Stage Transition Graph Model to describe the functional points from specifications.The entity layer uses simple extended finite state machine to describe entities of the design.We prove the completeness and usabilily of the model.Finally,we use the functional model to describe the functionality of benchmark designs.The experiments show that the functional model can avoid the whole state space of the design,this leads usabilily of the model.2.We propose an automatic test pattern generation(ATPG)method to cover the testspace of the entity-based functional point model.The proposed ATPG method adopts the modified backjumping algorithm and functional property-based testspace coverage strategy to cover the testspace of the functional point model.We use the proposed ATPG method to verify the benchmark designs.The experiment results show that for the large scale of designs,the proposed ATPG method can increase the stage coverage and the transition coveage by 9% respectively,and increase the test-space coverage by 23%.3.We propose a global FSM-based multiply-functional-points scheduling strategy,which can cover the whole state space of the global FSM by scheduling parallel execution of multiply functional points in the functional point model.The experiment results show that compared with the constrainted random vetification,the proposed strategy can double the coverage of global FSM and speed up the convergence of the coverage of global FSM.Compared with the method proposed in [100],the proposed strategy can speed up the convergence of the coverage of global FSM by 17 times.Meanwhile,the proposed scheduling strategy can be integrated with the proposed ATPG method to achieve a better code coverage and a functional coverage.4.Based on the proposed functional point model and the ATPG approach,we develop an automatic verification tool,which can 1)Adopting the proposed ATPG approach to generate test vectors based on the STG model;2)Receiving the STG model based on the given graphical template;3)Allowing user to preset the corresponding verification configuration;4)Checking the behavioral correctness for DUV based on the STG model;5)Recording the simulation reports and outputting coverage reports.The automatic verification tool realizes the the proposed semi-formal verification and facilitates the process of modeling functionality of designs,so it can support the efficient and complete verification.We use our functional point model-based semi-formal verification method and the corresponding automatic verification platform to verify a data path-sensitive design FPU and a control path-sensitive design DMA.The experiment results show that our functional point model-based semi-formal verification method has good performance in completeness.Compared with the tranditional verification approach,the proposed semiformal verification method can save 40% verification cycle.Compared with the formal method,the proposed semi-formal verification method can avoid the problem of state explosion.The experiment results proves that our specification-based method scales well for industrial designs and ensure efficient and complete exploration of functionality for design.So,the proposed functional point model-based semi-formal verification method has a brilliant future for industrial designs.