Description
Date depot: 1 janvier 1900
Titre: Modeling and Formal Verification of Power Management for the Design of Systems-on-Chip
Directeur de thèse:
Renaud PACALET (LTCI (EDMH))
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Power Management has become one major factor when designing Systems-on-Chip (SoC) targeting mobile devices. Basically, methodologies for designing SoC rely on 3 main steps. In the first step the application is modeled with a mixture of several high level languages (Matlab, Simulink, Java, C++, etc.). Then, in the second step, software and hardware functions are separated from each other: this phase is called Design Space Exploration. In the third step, the selected hardware platform defined at the previous step is developed apart from the software code, and finally all are integrated together.
LabSoC has introduced a platform dedicated to the Design Space Exploration step at high level of abstraction. This platform includes a UML profile - called DIPLODOCUS that implements the Y-methodology, with three main stages: application modeling, architecture modeling and mapping. The DIPLODOCUS profile is implemented by an open-source toolkit named TTool. The main DIPLODOCUS objective is to help designers to find suitable hardware architecture satisfying functional and non functional properties of the system to model. To attend this objective, it uses fast simulation and formal verification techniques.
DIPLODOCUS approach can efficiently take into account performance constraints, however power consumption issues are insufficiently addressed. In our research work, we intend to integrate power consumption criteria in DIPLODOCUS. Now, we are working on the extension of DIPLODOCUS UML diagrams, using meta-models, to allow designers to effectively capture the behavior of power management and power controller.
Doctorant.e: Ben Abdallah Feriel