Research On Key Technologies Of Model-Driven System-Level Functional Verification For System-on-Chip

With the advance of system-on-chip (SoC) technology, the complexity of SoC is sharply increasing. In order to deal with the increasing complexity, reduce the market-time, one fundamental methodology is to enable engineers to reuse existing design and raise levels of abstraction. Currently, research organizations, main EDA tools' providers are starting to integrate model-driven design methodology into their design flows for SoC. The new design methodology raises the new challenges for verification. The existing functional verification methods and technologies (simulation-based and formal) can not meet with the new verification requirements for the model-driven SoC design methodology. New theories and technologies must be proposed.Model-driven verification approach, which combines the ideas of the simulation-based and the formal verification, is proposed and rapidly getting popular. It is based on united description model. The well-defined functional coverage metrics, model-based abstraction techniques, model-based test generation techniques, formal verification techniques are used in this approach to perform quantitative analysis for verification completeness of the different abstract levels, especially for the behavior-level and transaction-level design.For the existing problems of the model-driven functional verification for SoC, this thesis mainly studies its key technologies. Due to the states exploration problem, formal verification approach is difficult to be applied in the system-level functional verification for SoC after IP Cores have been integrated into a system. In this desertion, this thesis mainly studies simulation-based functional verification approach. The SoC system functional verification needs consider the environment factors. This thesis studies the model-based specification approach, system-level behavior scenarios construction approach, and the risk evaluation approach, providing quantization for the system-level functional verification strategy. The simulation-based method has two key problems: how to generate test program and how to schedule test program. This thesis studies the model-base test generation approach and its relational scheduling technology. Based on functional specification and test generation, this thesis studies how to accelerate and improve the system-level formal verification approach for SoC, especially for behavior consistence verification between model-level and transaction-level design. Lastly, this thesis studies how to create executable model based on specification, execute simulation, and accelerate the function verification.In the model-driven functional verification framework, this thesis studies the key system funcational verification technologies and gets the following results.(1) Nowday, design constraints are difficultly modeled under the current united description model of SoC. In the dissertation, we have extended model-based SoC functional specification method by integrating OCL and its real-time extension into the SoC specification model, supporting modeling the constraint for SoC design. The improved specification model can be used to describe design more accurately and support SoC functional verification.(2) A novel model-based system-level design behavior construction and risk evaluation method is proposed. Behavior scenarios construction, design metric and risk evaluation provide useful means for identifying potentially troublesome SoC system-level behavior scenarios and IP components that require careful development and allocation of more testing and verification effort. In the dissertation, we have proposed an environment-driven and model-based system-level design behavior construction and risk evaluation method. Our method mainly includes five processes. Firstly, we model the SoC function for environment by use cases and actors. Secondly, we add constraints and probability annotations for use cases and scenarios. Thirdly, based on the annotated models, we create the system-level behavioral scenarios and get scenarios set. Fourthly, we analysis the trace of scenarios, get the associated components and channel sets, compute their risk factors. Lastly we compute the scenarios risk factors and evaluate the whole system risk. In this progress, we can not only construct system behavior scenarios, identify the critical scenarios and components, but also evaluate their risk, which can be used to guide the verification policy.(3) A novel environment-driven and model-based transaction test generation method is presented in this thesis. Based on the behavioral scenarios and the environment' input for SoC, test case generation algorithm generates directed transaction test programs for SoC system-level behavioral verification. The method reduces the number of the input stimulus for SoC system-level functional verification and increases the test program's efficiency. The effective scheduling of transactions has a great potential for SoC functional verification. Petri nets have proven to be a promising technique for solving scheduling problem. In this dissertation, we have presented a transaction scheduling method based on the extended Petri net model. We also extended our transaction scheduling method under TAM resource constraints. The proposed method can evaluate the scheduling behavior earlier, support many kinds of scheduling schemas, reuse the generated transactions and provide input stimulus for some complex behaviors simulation-based verification of SoC.(4) Extended hierarchical interface automata based consistence verification method and program slicing and aspect-oriented code instrument based consistence verification method are proposed in this thesis. In model-driven design methodology for SoC, consistence verification between deferent abstraction levels is the key technology to make sure the correctness that lower design can implement the upper specification. For consistence verification problem between model-level and transaction-level, we have presented two methods. One is the EHIA (Extended Hierarchy Interface Automata) based method. Another is static program slicing and aspect-oriented code instrument method. In EHIA-based method, we have defined the operational semantics for extended hierarchy interface automata and modeled SoC as an EHIA net. By computing and searching status space, verify the behavioral consistence. In the program slicing and aspect-oriented code instrument based method, we firstly decompose transaction-level design by static program slicing. Then we instrument aspect-oriented code into the decomposed program to monitor events. After executing simulation, we get events' traces, which can be used to verify the consistence of scenario specifications.(5) This thesis impoved the simulation-based verification method based on Petri nets for SoC. Eealy functional verification and making sure the correctness of SoC have very important effect for SoC follow-up design. Petri nets have formal and simulation verification ability. In this dissertation, we have extended Petri net model for creating system-on-chip high-level executable model, which can support early verification for SoC design.This thesis designs and implements a SoC funcational verification environment prototype base on component--SoC-CBVE. It integrates the proposed transaction test program generation mechanism, transaction scheduling method and behavior scenarios consistence verification method between model level and transaction level. Based on the proposed extended Petri net model, a modeling and simulation prototype--PTSE is implemented. The initial experiments carried out on the prototypes with practical designs have shown that the prototypes are practical and can be used to find errors in designs.