Gotowa bibliografia na temat „Langages de Construction de Matériel (HCLs)”

Les analyses statiques de pire temps d’exécution sont utilisées pour garantir les délais requis pour les systèmes critiques. Afin d’estimer des bornes précises sur ces temps d’exécution, ces analyses temporelles nécessitent des considérations sur la (micro)- architecture. Habituellement, ces modèles de micro-architecture sont construits à la main à partir des manuels des processeurs. Cependant, les initiatives du matériel libre et les langages de description de matériel de haut niveau (HCLs), permettent de réaborder la problématique de la génération automatique de ces modèles de micro-architecture, et plus spécifiquement des modèles de pipeline. Nous proposons un workflow qui vise à construire automatiquement des modèles de chemin de données de pipeline à partir de conceptions de processeurs décrites dans des langages de contruction de matériel (HCLs). Notre workflow est basé sur la chaine de compilation matériel Chisel/FIRRTL. Nous construisons au niveau de la représentation intermédiaire les modèles de pipeline du chemin de données. Notre travail vise à appliquer ces modèles pour prouver des propriétés liées à la prédictibilité temporelle. Notre méthode repose sur la vérification formelle. Les modèles générés sont ensuite traduits en modèles formels et intégrés dans une procédure existante basée sur la vérification de modèles pour détecter les anomalies de temps. Nous utilisons le langage de modélisation et de vérification TLA+ et expérimentons notre analyse avec plusieurs processeurs RISC-V open-source. Enfin, nous faisons progresser les études en évaluant l’impact de la génération automatique à l’aide d’une série de critères synthétiques
Static worst-case timing analyses are used to ensure the timing deadlines required for safety-critical systems. In order to derive accurate bounds, these timing analyses require precise (micro-)architecture considerations. Usually, such micro-architecture models are constructed by hand from processor manuals.However, with the open-source hardware initiatives and high-level Hardware Description Languages (HCLs), the automatic generation of these micro-architecture models and, more specifically, the pipeline models are promoted. We propose a workflow that aims to automatically construct pipeline datapath models from processor designs described in HCLs. Our workflow is based on the Chisel/FIRRTL Hardware Compiler Framework. We build at the intermediate representation level the datapath pipeline models. Our work intends to prove the timing properties, such as the timing predictability-related properties. We rely on the formal verification as our method. The generated models are then translated into formal models and integrated into an existing model checking-based procedure for detecting timing anomalies. We use TLA+ modeling and verification language and experiment with our analysis with several open-source RISC-V processors. Finally, we advance the studies by evaluating the impact of automatic generation through a series of synthetic benchmarks

Ce travail de thèse porte précisément sur la prise en charge du matériel embarqué dans la modélisation de l'application temps-réel. Afin d'améliorer le développement du matériel et de faciliter la communication des décisions architecturales au flot logiciel, nous avons adopté l'ingénierie dirigée par les modèles dans la conception, simulation et implantation de la plateforme matérielle. En effet, nous avons défini un langage de modélisation HRM (Hardware Resource Model) pour la description de plateformes matérielles sous différentes vues et à différents niveaux de détail. Nous avons ensuite conçu une méthodologie de modélisation du matériel en HRM pour assister tout utilisateur dans la construction de modèles de plateformes. Nous avons également développé un outillage complet et automatisé pour la simulation des plateformes matérielles ainsi modélisées. Enfin, nous décrivons un processus d'unification entre HRM et le standard d'implantation du matériel IP-XACT. Pour mieux prendre en charge le modèle de la plateforme matérielle dans la conception du système temps-réel, nous avons spécifiés des règles et des contraintes d'allocation qui régissent les placements des entités logicielles sur les ressources matérielles. Puis nous avons proposé des mécanismes d'adéquation pour adapter des configurations à priori inadéquates. Pour finir et illustrer l'agencement de toutes ces contributions dans le cadre d'un même processus de développement, nous avons développé une chenille de robots unicycles qui roulent sans glisser sur un plan horizontal. Il s'agit d'un système qui est à la fois temps-réel, embarqué, multi-tâches, distribué, répétitif et paramétrable
This PhD work focuses on the hardware support when modeling real-time systems. To improve the development of hardware and to communicate architectural intends to the software flow, we adopted the model driven engineering for design, simulation and implementation of hardware platforms. We have first defined a modeling language HRM (Hardware Resource Model) that describes hardware platforms with different views and at different levels of detail. Then, we developed a methodology based on HRM to help users in the construction of their platforms models. We have also developed automated tools for the simulation of these hardware models. Finally, we provide an efficient process of unification between HRM and the recent standard of hardware implementation IP-XACT. As our purpose is to take into consideration the hardware properties during the system design, we have specified rules and constraints that govem allocation of software entities onto hardware resources. After that, we proposed mechanisms to adapt inadequate configurations. Finally, we illustrate all these contributions within the same case study, which is a robots chain. It is realtime, embedded, multi-tasking, distributed, repetitive and configurable system

La modélisation du contenu des puces pour systèmes embarqués s'avère de plus en plus difficile puisque le développement des outils et des méthodologies de modélisation n'a pas su accompagner l'explosion de la complexité des systèmes. Les méthodes formelles ont su démontrer dans les dernières années leurs capacités de prévention et de détection d'erreurs, ainsi que leurs avantages dans l'expression univoque de demandes et dans la spécification de systèmes. Malgré cela, leur utilisation reste toujours restreinte en raison d'un manque de liens avec les méthodes existantes et la difficulté de leur utilisation. Dans ce document, on essaye de montrer dans quelle mesure la conception de systèmes embarqués peut profiter de l'utilisation de méthodes formelles. Pour cela, plusieurs exemples sont présentés qui démontrent comment l'utilisation des méthodes formelles peut être intégrée dans la conception conjointe tout en cachant - du moins en partie - leur complexité inhérente.

Pour tirer profits des avancées de la micro électronique, il est nécessaire que la productivité des concepteurs de systèmes électroniques évolue également selon la même tendance. Une piste de progrès certaine consiste à relever le niveau d'abstraction pour la spécification de ces systèmes et automatiser leur raffinement vers l'implémentation. Dans ce contexte, il est particulièrement intéressant d'envisager l'utilisation conjointe de l'outil CoFluent Studio, issu des recherches de l'équipe MCSE de l'école polytechnique de l'Université de Nantes, commercialisé par la société CoFluent Design et de l'outil GAUT développé par le LESTER de l'Université de Bretagne Sud. Le premier outil permet de modéliser et estimer les performances des systèmes électroniques à haut niveau d'abstraction, le second permet de raffiner une spécification algorithmique vers une implémentation matérielle. Toutefois, il est nécessaire de compléter ces démarches de développement par l'étude des niveaux d'abstraction inférieurs afin de vérifier si les performances estimées sont vérifiées pour les vues raffinées et pour optimiser l'implémentation du système. Dans ce contexte, nous proposons deux approches dans ce mémoire. La première repose sur l'identification d'un niveau d'abstraction que nous qualifions de transactionnel à grains fins. Nous étudions alors le problème de la modélisation de la fonctionnalité lors d’un raffinement vers ce type de modèle. Nous faisons également une seconde proposition d'adaptateur de communication permettant d'assembler des composants décrits au niveau transactionnel à grains fins mais aussi des composants décrits au niveau système. Nous illustrons ces propositions sur l'étude d'un modulateur MIMO+OFDM utilisé en communications numériques. Ce travail a été mené dans le cadre du projet PALMYRE, financé par CPER 2000-2006 de la région Bretagne
If we want to take advantage of technological evolutions, designer’s productivity has to increase in the same proportions as the component integration on integrated circuits. To take up this challenge, system level design solutions have to be set up. In this context, the joint use of CoFluent Studio distributed by CoFluent design, originally developed by the MCSE team of the Ecole polytechnique de l'Université de Nantes, and GAUT developed by the LESTER lab of the Université de Bretagne Sud is especially relevant. The first tool allows to model and estimate the performances of the systems at a high level of abstraction and the second allows to automatically refine an abstract algorithmic specification down to its hardware implementation. Nevertheless, these approaches require to be completed by the analysis of models of lower levels of abstraction, on the one hand to verify if the targeted performance estimated at higher levels is satisfied and on the other hand to optimize the implementation costs of the system. In this context, we propose two original contributions. Firstly, we propose a fine grain transactional level of abstraction which we use to study the impact of the fine grain data order in a system on the implementation cost of the system. Secondly, in continuity with the first proposal, we propose a communication wrapper which allows to interconnect fin grain transactional components just as easily as system level components. We illustrate these propositions on the study of a MIMO+OFDM transmitter. This work takes place in the PALMYRE project which was financed by the CPER 2000-2006 of the région Bretagne

Dans le cadre de la modélisation de systèmes complexes, la conception d'entrée ou appelée système représente le plus haut niveau d'abstraction du système global, ceci avant tout choix en terme d'implantation et de technologies. À ce tout premier stade de la conception, l'utilisation d'un langage formel de spécification est de plus en plus considéré comme le fondement d'un réel processus de validation en particulier dans le cas d'exigences de sûreté. Cette thèse met en lumière la nécessité d'une modélisation par raffinement: de la spécfication la plus abstraite vers un point de description proche de l'implémentation afin d'assurer (1) la traçabilité des besoins et des exigences, (2) une meilleure gestion du développement et (3) surtout une conception sûre des systèmes car générée par construction prouvée et ceci que ces sytèmes fassent appel à des technologies logicielles, numériques ou analogiques, voire autres. Le travail qui a été mené a consisté à mettre en perspective la taxinomie des langages ADL, le modèle de développement utilisé dans le cadre des composants électroniques et la méthode par raffinement, dite Méthode B. Ceci nous a permis de réaliser la plateforme BHDL Tool : plateforme de conception de circuits électroniques intégrant (1) une interface de description structurelle de composants électroniques, (2) un générateur de code VHDL et enfin (3) un traducteur en un langage formel pour les preuves de raffinement sous l'Atelier B.