Partenaires

Ampère

Nos tutelles

CNRS Ecole Centrale de Lyon Université de Lyon Université Lyon 1 INSA de Lyon

Nos partenaires

Ingénierie@Lyon



Rechercher


Accueil > Thèses et HDR > Thèses en 2011

Mingming REN - 27/072011 - INSA

publié le , mis à jour le

Mingming REN soutient sa thèse le 27 juillet 2011 à 10h30 - Amphi René Char à l’INSA de Lyon

Titre :

An Incremental approach for hardware Discrete Controller Synthesis

Jury :

  • Directeurs de thèse : Eric NIEL, Emil DUMITRESCU
  • Rapporteurs : Eric RUTTEN ; Jean-Michel COUVREUR
  • Examinateurs : Hervé MARCHAND ; Dominique BORRIONE

Résumé :

La synthèse de contrôleurs discrets (SCD) est appliquée pour générer automatiquement des contrôleurs matériels corrects par construction. Pour un système donné (un modèle à états), et une spécification de contrôle associée (une exigence comportementale), cette technique génère un contrôleur qui, composé avec le système initial, garantit la satisfaction de la spécification. La technique de SCD utilisée dans ce travail s’appuie sur les diagrammes de décision binaire (BDDs). Les contrôleurs générés doivent être compatibles avec les outils standards de synthèse matérielle de niveau RTL.
Deux problèmes principaux ont été examinés : l’explosion combinatoire et la génération effective du contrôleur matériel. La maîtrise de l’explosion combinatoire s’appuie sur des approches de type « diviser pour régner », exploitant la modularité du système ou du contrôleur. La plupart des approches existantes ne traitent pas la communication explicite entre différents composants du système. Le mécanisme de synchronisation le plus couramment envisagé est le partage des événements d’entrée, faisant abstraction des sorties. Nous proposons une technique de SCD incrémentale qui permet de traiter également les systèmes communicants. Une étape initiale d’abstraction modulaire est suivie par une séquence progressive de raffinements et de calculs de solutions approximatives de contrôle. La dernière étape de cette séquence engendre un contrôleur exact. Nous montrons que cette technique offre une efficacité améliorée en temps/mémoire par rapport à l’approche traditionnelle globale de la SCD.
La génération du contrôleur matériel s’appuie sur un traitement spécifique du non-déterminisme de contrôle. Une architecture de contrôle à boucle partiellement fermée est proposée, afin de permettre une conception hiérarchique. Une technique automatique transformant une équation de contrôle en vecteur de fonctions de contrôle est proposée et illustrée.
La SCD est ensuite appliquée et illustrée sur la correction de certaines erreurs de conception. L’efficacité des techniques proposées est illustrée sur un ensemble d’exemples de conception matérielle.

Voir en ligne : Texte complet de la thèse