A Research Approach To Model Abstraction Based On Assertion Graph

The growing of integrated circuit design’s complexity and the acceleration of chipreplacement rate make it more and more difficult to verify the integrated circuit chip.The traditional chip verification is based on simulated verification. Because of its longcycle, it can not be verified with use case in full coverage. Formal verification is thatusing a mathematical method to prove if the properties, described by a specificationlanguage, satisfy the existing system model, so the method is completeness and avoidthe shortcomings of the simulation-based verification. Nevertheless, the approach issensitive to computational complexity. It just verifies the smaller chip model, because ofthat the large scale designs will lead to the state explosion problem. To get betterperformance, it is necessary to abstract the model and keep its original functionality.This is the only way to ensure the correctness of model abstraction.This topic starts from the basic theory of formal verification, discusses modelabstraction and some verification platform and extends the platform and implements theabstraction technology to achieve the purpose of accelerating the verification process.This thesis firstly introduces formal verification methods、modal logic and thebasic theory of model abstraction. Secondly it analyzes generalized symbolic trajectoryassignment as an extension of STE, GSTE, and discusses its extended part e.g.-regular properties, assertion graph, in detail. Next this thesis will give a briefintroduction to the VIS platform such as model checking method and specificationlanguage CTL, and complete comparison of scope of expression between the CTL andAssertion Graph to make it possible to complete the comparison test of invariantproperty. After the above study and comparative analysis, we introduce an implementedversion of GSTE, Whale, and extend the non-blocking assignments on its platform VIS.Through verifying the status transition of register transfer level model and consistencybetween output data and input data of UART, the method has been proven to be fullcoverage for the test case and be important significant in actual issue.For the problem of state explosion, the thesis introduce model partitioningtechnique in model abstraction to GSTE verification method and adopt model abstraction techniques based on the assertion graph to get important performancepromotionn in process of verifying the invariant properties, Through comparing theperformance with various verification algorithm in VIS. Prove that GSTE will reducethe number of steps to the fixed point by model abstraction, and get faster speed whenverify invariant properties of the cases without counter examples.