Search
Verification Environment for SoC - Demonstration of a Coverage Driven Verification Environment for UML Models of Systems-on-Chip
The DIPLODOCUS UML profile targets the partitioning of Systems-on-Chip early in the design flow, following the Y-Chart approach: application modeling, architecture modeling, mapping. DIPLODOCUS is supported by an open-source toolkit named TTool. One of the strengths of TTool is its capability to transform high level models into both simulation and formal models so as to obtain performance results and proofs of functional properties respectively. The version of TTool we presented at DATE 2010 featured two extreme cases: simulation and formal verification. The former produces only one possible system execution, the latter exhaustively explores the entire state space of the mapping model. Despite abstractions, formal verification of medium sized models pushes model-checkers to their limits. This year's demonstration presents a brand new strategy to enhance simulation with dynamic coverage of the state space, which may be guided interactively by the user or automatically conducted based on system requirements. For that purpose, we combine several techniques, including the static analysis of UML models, and also model checking techniques.