Skip to Content

Verification Environment for SoC - Demonstration of a Coverage Driven Verification Environment for UML Models of Systems-on-Chip

0
Your rating: None
Tool Name (abbreviation): 
Verification Environment for SoC
Author(s): 
Daniel Knorreck, ...
(unregistered) Author(s): 
Ludovic Apvrille (Telecom ParisTech)
Renaud Pacalet (Telecom ParisTech)

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.

Project Information
Project Acronym: 
TTool
Project Description: 
TTool is an open-source toolkit that supports several UML2/SysML profiles, including AVATAR, TURTLE and DIPLODOCUS. The main idea behind TTool is that graphical models of Systems-on-Chip may be formally verified and simulated at the push of a button. The designer does not need any expertise neither in simulation nor in formal techniques. To this end, UML diagrams are automatically translated into an intermediate specification expressed in a formal language, which serves as starting point for deriving formal specifications (in LOTOS, UPPAAL) and simulation code. In the case of DIPLODOCUS models, three building blocks (mapping, application, architecture) are leveraged to generate simulation code (C++) or formal specifications. TTool embraces a module which allows the designer to control simulation in real time by performing step wise execution, saving and restoring simulation states as well as providing live feedback to UML diagrams.
Tag your tool
Keywords: 
Formal Verification
Simulation
UML
Profile
System-on-Chip
High Level Model
Coverage
TTool
DIPLODOCUS