Génie Électrique

Synthèse et vérification
Génie ÉlectriqueAnnée 3, Semestre S9
Cycle ingénieur
3 crédits ECTS3GES9SYV
Objectifs
  • Ce module traite de la modélisation de systèmes - sur le flan formel et pratique -, en vue notamment de leur vérification, et des techniques de synthèse de tels systèmes sur des cibles de type circuit numériques.
Liste des ECModélisation et vérification de systèmes réactifs
Modélisation en SystemC
Synthèse logique pour circuits microélectroniques numériques
Horaire encadré32 h
Travail personnel16 h
Évaluation50% Modélisation et vérification de systèmes réactifs
50% Synthèse logique pour circuits microélectroniques numériques
Pré-requis2GES8PRO - Programmation
2GES8CSN - Conception de systèmes numériques
2GES7VHD - Langage de description matériel (VHDL)
ResponsableJocelyn SEROT
18/08/2008
Génie ÉlectriqueModélisation et vérification de systèmes réactifs
Objectifs
  • Ce cours est une introduction aux concepts et techniques utilisés pour vérification de systèmes réactifs, en particulier ceux fondés sur la vérification de modèle (model-checking).
Compétences
  • Connaitre les principaux fondements théoriques des techniques de validation par vérification de modèle (théorie des automates, logiques temporelles)
  • Comprendre le principe des techniques de vérification par model-checking
  • Savoir appliquer ces techniques sur des exemples simples
Description
  • Vérifier : pourquoi, comment .
  • Elements de théorie des automates et des langages
  • Elements de logique temporelle (LTL, CTL)
  • Introduction au model-checking LTL
Horaire encadré14h (8h CM + 6h TD)
ÉvaluationExamen final, Écrit
Bibliographie

Model Checking, Clarke, E.M.; Grumberg, O.; Peled, D.A., MIT Press, 1999

Introduction to automata theory, languages and computation, Hopcroft, J.E.; Motwani R.; Ullman J.D., Addison-Wesley, 2003

Modélisation et Vérification des Systèmes Réactifs, Sérot, J., Cours en ligne : http://cust-interne.univ-bpclermont.fr/Enseignement/Ge/serot/cours

EnseignantsJocelyn SEROT
13/11/2009
Génie ÉlectriqueModélisation en SystemC
Objectifs
  • Cette UE est une initiation au langage SystemC pour la modélisation, la simulation et la synthèse de système numériques
Compétences
  • Connaitre les bases du langage SystemC, son domaine d'utilisation
  • Savoir utiliser ce langage dans le cadre d'un flot de conception de systèmes numériques
Description
  • Présentation du langage
  • Mise en œuvre sur un cas simple
Horaire encadré12h (4h CM + 8h TP)
ÉvaluationExamen final, Travail pratique
Support
  • Chaine de développement SystemC
EnseignantsJocelyn SEROT
27/05/2009
Génie ÉlectriqueSynthèse logique pour circuits microélectroniques numériques
Objectifs
  • Maitriser les différentes étapes de la conception d'un circuit microélectronique numérique
  • Modélisation VHDL RTL pour synthèse
Compétences
  • Maitriser l'étape de synthèse logique des circuits intégrés
  • Connaitre les techniques de modélisation VHDL RTL pour Synthèse automatique
  • Savoir analyser les performances des ASIC
  • Connaitre les outils/enjeux/defis de la conception des SoC
Description
  • Flots de conception pour la synthèse logique d'ASIC, caractérisation et performances de la logique CMOS, analyse de timing
  • Langage VHDL RTL pour la synthèse d'ASIC
  • Nouvelles techniques et outils pour l'intégration de Systèmes On Chip
Horaire encadré6h (6h CM)
ÉvaluationExamen final, Écrit
EnseignantsAlexis LANDRAULT, André PICCO
04/03/2010