Description d'un outil de développement de systèmes experts (ODSE) conçu et réalisé en ADA. Le formalisme de description des connaissances (faits et règles), les mécanismes d'interférence mis en œuvre ainsi que l'implémentation du système sont donnes. Enfin, la thèse décrit l'utilisation de ODSE pour la réalisation d'un outil d'aide a la synthèse architecturale de c.i. VLSI (ASA). Les techniques utilisées par ASA (analyse de flots, ordonnancement, allocation de ressources) sont exposées ainsi que leur traduction dans le formalisme de ODSE. Enfin, les résultats d'utilisation de ASA pour la synthèse d'un filtre Leapfrog d'ordre 9 sont donnes

Dans cette thèse, nous proposons un flot de conception pour le développement d'applications de traitement du signal systématique implémentées sur FPGA. Nous utilisons une approche Ingénierie Dirigée par les Modèles (IDM) pour la mise en oeuvre de ce flot de conception, dont la spécification des applications est décrite en UML. La première contribution de cette thèse réside dans la création d'un métamodèle isolant les concepts utilisés au niveau RTL. Ces concepts sont extraits d'implémentations matérielles dédiées de tâches à fort parallélisme de données. Par ailleurs, ce métamodèle considère la technologie d'implémentation FPGA et propose différents niveaux d'abstractions d'un même FPGA. Ces multiples niveaux d'abstractions permettent un raffinement des implémentations matérielles.<br /><br />La seconde contribution est le développement d'un flot de compilation permettant la transformation d'une application modélisée à haut niveau d'abstraction (UML) vers un modèle RTL. En fonction des contraintes de surfaces disponibles (technologie FPGA), le flot de conception optimise le déroulement des boucles et le placement des tâches. Le code VHDL produit est directement simulable et synthétisable sur FPGA. À partir d'applications modélisées en UML, nous produisons automatiquement un code VHDL.<br /><br />Le flot de conception proposé a été utilisé avec succès dans le cadre de sécurité automobile ; un algorithme de détection d'obstacles a été automatiquement généré depuis sa spécification UML.

Les travaux présentés dans ce document portent sur la vérification<br />de modèles de systèmes sur puce, au niveau transactionnel (TLM).<br />Nous présentons le niveau transactionnel et ses variantes, et<br />rappelons en quoi ce nouveau niveau d'abstraction est aujourd'hui<br />nécessaire en plus du niveau de transfert de registre (RTL) pour<br />répondre aux contraintes de productivités et de qualités de plus en<br />plus fortes, et comment il s'intègre dans le flot de conception.<br /><br />Nous présentons un nouvel outil, LusSy, permettant la vérification<br />formelle de modèles transactionnels écrits en SystemC. Sa structure<br />interne s'apparente à celle d'un compilateur: Une partie frontale,<br />Pinapa, qui lit le programme source, une extraction de la<br />sémantique, Bise, dans notre formalisme intermédiaire \hpiom, une<br />série d'optimisations dans le composant Birth, et des générateurs<br />de code pour les outils de preuves pour Lustre et SMV.<br /><br />Lussy est conçu et écrit de manière à avoir aussi peu de limitation<br />que possible sur la forme du code SystemC accepté en entrée. \pinapa<br />utilise une approche innovante qui lui permet de s'affranchir de la<br />plupart des limitations dont souffrent les outils similaires.<br />L'extraction de la sémantique implémente plusieurs constructions TLM<br />qu'aucun autre outil disponible aujourd'hui ne gère. Il ne demande<br />pas d'annotation manuelle du code source, toute la chaîne étant<br />entièrement automatisée.<br /><br />Lussy est capable de prouver formellement des propriétés sur des<br />modèles de petites taille, et ses composants sont réutilisables pour<br />des outils de preuve compositionnelle, ou d'analyse de code autre<br />que le model-checking qui passeront mieux à l'échelle que l'approche<br />actuelle.<br /><br />Nous présentons les principes de chaque étape de la transformation,<br />ainsi que notre implémentation. Les résultats sont donnés pour des<br />exemples simples et petits, et pour une étude de cas de taille<br />moyenne, EASY. Les expérimentations avec Lussy nous ont permis de<br />comparer les différents outils de preuves que nous avons utilisés,<br />et d'évaluer l'efficacité des optimisations que nous avons<br />implémentées.

On étudie l'abstraction et la généricité dans les langages de programmation. On décrit les principaux outils de la programmation générique. On traite ensuite de la spécification des types et des fonctions et on étudie les methodes de vérification de programmes spécifiés algébriquement.

Indépendance d'un logiciel graphique par rapport à son contexte d'utilisation. Conception et réalisation d'un logiciel graphique basé sur le concept de "console virtuelle". La première génération de GRIGRI. La conception du logiciel GRIGRI. La réalisation du logiciel GRIGRI. Etude des deux types d'interpréteurs. Directives pour l'insertion du logiciel dans un contexte quelconque

ON propose un modèle de machine réseau logique. Définition d'un ensemble de fonction et de mécanisme élémentaires qui aident à la répartition dans l'exécution des programmes d'une application réseau.

Aujourd'hui, le fait que la mémoire constitue un goulot d'étranglement pour les performances des programmes est un truisme. Les compilateurs doivent donc optimiser les programmes afin d'éviter de recourir à la mémoire, et ceci en utilisant au mieux les registres disponibles dans le processeur à parallélisme d'instructions (ILP).<br /><br />Cette thèse réexamine le concept de la pression des registres en lui donnant une plus forte priorité par rapport à l'ordonnancement d'instructions, sans ôter à ce dernier ses possibilités d'extraction de parallélisme. Nous proposons de traiter le problème des registres avant la phase d'ordonnancement. Deux grandes stratégies sont étudiées en détail. La première consiste à analyser et manipuler un graphe de dépendance de données (GDD) pour garantir les contraintes de registres sans allonger son chemin critique (si possible). Nous introduisons la notion de saturation en registres qui est la borne exacte maximale du besoin en registres de tout ordonnancement valide, indépendamment des contraintes architecturales. Son but est d'ajouter des arcs au GDD pour que la saturation soit en dessous du nombre de registres disponibles. Réciproquement, la suffisance est le nombre minimal de registres dont il faut disposer pour produire au moins un ordonnancement valide pour le GDD. Si cette suffisance est au dessus du nombre effectif de registres, alors les accès à la mémoire sont inévitables.<br />Notre deuxième stratégie construit une allocation de registres directement dans le GDD en optimisant la perte du parallélisme intrinsèque.<br /><br />Cette thèse considère des blocs de base, des graphes acycliques de flots de contrôles et des boucles internes destinées au pipeline logiciel. Nos expériences montrent que nos heuristiques sont presque optimales. L'étude prouve que nous pouvons et devons traiter les contraintes de registres avant la phase d'ordonnancement tout en garantissant une liberté pour l'extraction et l'exploitation de l'ILP.

Par "approche langage" on entend désigner une approche qui s'exprime, soit dans un langage de programmation, soit par un langage de programmation.<br />Les approches qui s'expriment dans le langage ne font appel à aucun formalisme éloigné (e.g. sémantique). Le langage de programmation est l'unique cadre de travail pour exprimer le problème, le résoudre et appliquer la solution. Nous montrons :<br /><br />- comment la compilation des langages fonctionnels peut s'exprimer dans le langage lui-même par transformation de programme. Ce cadre unifié permet de décrire, prouver, comparer et classifier la plupart des mises en œuvre de langages fonctionnels,<br /><br />- deux optimisations de l'implémentation des langages fonctionnels (une analyse de globalisation et un GC étendu) qui reposent sur la syntaxe et le type des expressions.<br /><br /><br /> Pour les approches qui s'expriment par un langage de programmation, il s'agit de prévenir le problème ou d'assurer une propriété via l'utilisation d'un langage (ou d'une discipline de programmation). Nous illustrons ce style d'approche par trois exemples :<br /><br /><br />- les types graphes qui permettent de définir et vérifier le partage des structures de données à pointeurs,<br /><br />- un langage dédié au parallélisme qui garantit une analyse de coût précise et un choix automatique de la meilleure distribution,<br /><br />- un style de programmation par aspects qui permet d'imposer automatiquement des propriétés aux programmes.

Les systèmes embarqués sont des dispositifs électroniques et informatiques autonomes, dédiés à une tâche bien précise. Leur utilisation s'est désormais démocratisée à de nombreux domaines d'applications et en particulier au multimédia. Ce type d'application est caractérisé par un besoin important en puissance de calcul et en échange de données. Les architectures matérielles au cœur de ces systèmes sont généralement dotées d'accélérateurs chargés de l'exécution des noyaux de calcul intensif. Les architectures reconfigurables à gros grain (CGRA) sont particulièrement adaptées à l'accélération d'applications multimédia car elles répondent au mieux aux contraintes de performance, d'efficacité énergétique, de flexibilité et de coût de conception. En effet, ce type d'architecture est un compromis entre les processeurs à usage général, les architectures dédiées et celles reconfigurables à grain fin. Cette thèse traite de certains aspects liés aux problématiques de conception et de compilation d'applications pour CGRA. Nos travaux s'inscrivent dans une démarche d'adéquation applications multimédia / CGRA / conception et compilation basées sur la programmation par contraintes (CP). Notre méthodologie nous a permis, grâce à la CP, de modéliser et de résoudre un ensemble de problèmes combinatoires complexes. Le premier modèle présenté a trait à la fusion d'unités fonctionnelles reconfigurables sous contraintes architecturales et technologiques. Les deux autres modèles abordent les problèmes de : placement, ordonnancement et routage des données pour le déploiement d'une application sur CGRA. Notre approche permet, dans la majorité des cas, de prouver l'optimalité de la solution obtenue.

La loi de Moore sur semi-conducteurs approche de sa fin. L'evolution de l'architecture de von Neumann à travers les 40 ans d'histoire du microprocesseur a conduit à des circuits d'une insoutenable complexité, à un très faible rendement de calcul par transistor, et une forte consommation énergetique. D'autre-part, le monde du calcul parallèle ne supporte pas la comparaison avec les niveaux de portabilité, d'accessibilité, de productivité et de fiabilité de l'ingénérie du logiciel séquentiel. Ce dangereux fossé se traduit par des défis passionnants pour la recherche en compilation et en langages de programmation pour le calcul à hautes performances, généraliste ou embarqué. Cette thèse motive notre piste pour relever ces défis, introduit nos principales directions de travail, et établit des perspectives de recherche.