Une solution de gestion de puissance d’un système sur puce peut être définie par une architecture de faible puissance composée de multiples domaines d'alimentation et de leur stratégie de gestion. Si ces deux éléments sont économes en énergie, une solution efficace en énergie peut être obtenue. Cette approche nécessite l’ajout d’éléments structurels de puissance et de leurs comportements. Une stratégie de gestion doit respecter les dépendances structurelles et fonctionnelles dues au placement physique des domaines d'alimentation. Cette relation forte entre l'architecture et sa stratégie de gestion doit être analysée tôt dans le flot de conception pour trouver la solution de gestion de puissance la plus efficace. De récentes normes de conception basse consommation définissent des sémantiques pour la spécification, simulation et vérification d’architecture de faible puissance au niveau transfert de registres (RTL). Mais elles manquent une sémantique d’interface de gestion des domaines d'alimentation réutilisable ce qui alourdit l’exploration. Leurs sémantiques RTL ne sont pas aussi utilisables au niveau transactionnel pour une exploration plus rapide et facile. Pour combler ces lacunes, cette thèse étend ces normes et fournit une étude complète des possibilités d'optimisation de puissance basées sur la composition et la gestion des domaines d'alimentation pour des modèles fonctionnels transactionnels utilisant un environnement commun USLPAF. USLPAF comprend une méthodologie alliant conception et vérification des modèles transactionnels de faible consommation, ainsi qu’une bibliothèque de techniques de modélisation et fonctions prédéfinies pour appliquer cette méthodologie. / A SoC power management solution can be defined by a low-power architecture composed of multiple power domains and a power management strategy for power domains states control. If these two elements are energy-efficient, an energy-efficient solution can be obtained. This approach requires inferring power structural elements and their related behavior in the chip internal logic. A strategy adjusting the power domains states must respect structural and functional dependencies due to the physical power domains composition. This strong relationship between power architecture and its management strategy must be explored at early design stages to find the most energy-efficient solution. Low-power design standards have recently enabled low-power architecture exploration starting from the Register Transfer Level (RTL) by defining semantics to specify power architecture, simulate and check its behavior along with the initial functional one. But, these standards miss semantics for reusable power domain control interface making power management strategies exploration tedious. The RTL-based semantics defined by these standards constrain also their use at Transaction-Level of Modeling (TLM) for fast and easy exploration. This dissertation proposes extensions to low-power standards to fill these gaps. It provides a complete study of power optimization opportunities based on composition and management of power domains in Transaction-Level (TL) functional models within a common USLPAF framework. USLPAF includes a methodology that combines design and verification of TL low-power models. To apply this methodology, USLPAF incorporates a library of modeling techniques and built-in features.

À l'heure actuelle, les dispositifs embarqués regroupent une grande variété d'applications, ayant des fonctionnalités complexes et demandant une puissance de calcul de plus en plus importante. Ils évoluent actuellement de systèmes multiprocesseur sur puce vers des architectures many-core et posent de nouveaux défis au développement de logiciel embarqué. En effet, Il a classiquement été guidé par les performances et donc par les besoins spécifiques des plates-formes. Or, cette approche s'avère trop couteuse avec les nouvelles architectures matérielles et leurs évolutions rapprochées. Actuellement, il n'y a pas un consensus sur les environnements à utiliser pour programmer les nouvelles architectures embarquées. Afin de permettre une programmation plus rapide du logiciel embarqué, la chaîne de développement a besoin d'outils pour la mise au point des applications. Cette mise au point s'appuie sur des techniques d'observation, qui consistent à recueillir des informations sur le comportement du système embarqué pendant l'exécution. Les techniques d'observation actuelles ne supportent qu'un nombre limité de processeurs et sont fortement dépendantes des caractéristiques matérielles. Dans cette thèse, nous proposons EMBera~: une approche à base de composants pour l'observation de systèmes multiprocesseurs sur puce. EMBera vise la généricité, la portabilité, l'observation d'un grand nombre d'éléments, ainsi que le contrôle de l'intrusion. La généricité est obtenue par l'encapsulation de fonctionnalités spécifiques et l'exportation d'interfaces génériques d'observation. La portabilité est possible grâce à des composants qui, d'une part, ciblent des traitements communs aux MPSoCs, et d'autre part, permettent d'être adaptés aux spécificités des plates-formes. Le passage à l'échelle est réussi en permettant une observation partielle d'un système en se concentrant uniquement sur les éléments d'intérêt~: les modules applicatifs, les composants matériels ou les différents niveaux de la pile logicielle. Le contrôle de l'intrusion est facilité par la possibilité de configurer le type et le niveau de détail des mécanismes de collecte de données. L'approche est validée par le biais de différentes études de cas qui utilisent plusieurs configurations matérielles et logicielles. Nous montrons que cette approche offre une vraie valeur ajoutée dans le support du développement de logiciels embarqués. / Embedded software development faces new challenges as embedded devices evolve from Multiprocessor Systems on Chip (MPSoC) with heterogeneous CPU towards many-core architectures. The classical approach of optimizing embedded software in a platform-specific way is no longer applicable as it is too costly. Moreover, there is no consensus on the programming environments to be used for the new and rapidly changing embedded architectures. MPSoC software development needs debugging tools. These tools are based on observation techniques whose role is to gather information about the embedded system execution. Current techniques support only a limited number of processors and are highly dependent on hardware characteristics. In this thesis, we propose EMBera, a component-based approach to MPSoC observation. EMBera aims at providing genericity, portability, scalability and intrusion control. Genericity is obtained by encapsulating specific embedded features and exporting generic observation interfaces. Portability is achieved through components targeting common treatments for MPSoCs but allowing specialization. Scalability is achieved by observing only the elements of interest from the system, namely application modules, hardware components or the different levels of the software stack. Intrusion control is facilitated by the possibility to configure the type and the level of detail of data collection mechanisms. The EMBera approach is validated by different case studies using different hardware and software configurations. We show that our approach provides a real added value in supporting the embedded software development.

Le projet HODISS dans le cadre duquel s'effectue nos travaux adresse la problématique de la synchronisation globale des systèmes complexes sur puce (System-on-Chip ou SOCs, par exemple un multiprocesseur monolithique). Les approches classiques de distribution d'horloges étant devenues de plus en plus obsolètes à cause de l'augmentation de la fréquence d'horloge, l'accroissement des temps de propagation, l'accroissement de la complexité des circuits et les incertitudes de fabrication, les concepteurs s’intéressent (pour contourner ces difficultés) à d'autres techniques basées entre autres sur les oscillateurs distribués. La difficulté majeure de cette dernière approche réside dans la capacité d’assurer le synchronisme global du système. Nous proposons un système d'horlogerie distribuée basé sur un réseau d’oscillateurs couplés en phase. Pour synchroniser ces oscillateurs, chacun d'eux est en fait une boucle à verrouillage de phase qui permet ainsi d'assurer un couplage en phase avec les oscillateurs des zones voisines. Nous analysons la stabilité de l'état synchrone dans des réseaux cartésiens identiques de boucles à verrouillage de phase entièrement numériques (ADPLLs). Sous certaines conditions, on montre que l'ensemble du réseau peut synchroniser à la fois en phase et en fréquence. Un aspect majeur de cette étude réside dans le fait que, en l'absence d'une horloge de référence absolue, le filtre de boucle dans chaque ADPLL est piloté par les fronts montants irréguliers de l'oscillateur local et, par conséquent, n'est pas régi par les mêmes équations d'état selon que l'horloge locale est avancée ou retardée par rapport au signal considéré comme référence. Sous des hypothèses simples, ces réseaux d'ADPLLs dits "auto-échantillonnés" peuvent être décrits comme des systèmes linéaires par morceaux dont la stabilité est notoirement difficile à établir. L'une des principales contributions que nous présentons est la définition de règles de conception simples qui doivent être satisfaites sur les coefficients de chaque filtre de boucle afin d'obtenir une synchronisation dans un réseau cartésien de taille quelconque. Les simulations transitoires indiquent que cette condition nécessaire de synchronisation peut également être suffisante pour une classe particulière d'ADPLLs "auto-échantillonnés". / The HODISS project, context in which this work is achieved, addresses the problem of global synchronization of complex systems-on-chip (SOCs, such as a monolithic multiprocessor). Since the traditional approaches of clock distribution are less used due to the increase of the clock frequency, increased delay, increased circuit complexity and uncertainties of manufacture, designers are interested (to circumvent these difficulties) to other techniques based among others on distributed synchronous clocks. The main difficulty of this latter approach is the ability to ensure the overall system synchronization. We propose a clock distribution system based on a network of phase-coupled oscillators. To synchronize these oscillators, each is in fact a phase-locked loop which allows to ensure a phase coupling with the nearest neighboring oscillators. We analyze the stability of the synchronized state in Cartesian networks of identical all-digital phase-locked loops (ADPLLs). Under certain conditions, we show that the entire network may synchronize both in phase and frequency. A key aspect of this study lies in the fact that, in the absence of an absolute reference clock, the loop-filter in each ADPLL is operated on the irregular rising edges of the local oscillator and consequently, does not use the same operands depending on whether the local clock is leading or lagging with respect to the signal considered as reference. Under simple assumptions, these networks of so-called “self-sampled” all-digital phase-locked-loops (SS-ADPLLs) can be described as piecewise-linear systems, the stability of which is notoriously difficult to establish. One of the main contributions presented here is the definition of simple design rules that must be satisfied by the coefficients of each loop-filter in order to achieve synchronization in a Cartesian network of arbitrary size. Transient simulations indicate that this necessary synchronization condition may also be sufficient for a specific class of SS-ADPLLs.

<p>Les travaux de cette thèse s'inscrivent dans le cadre de la validation formelle et le contrôle réactif de calculs à haute performance sur systèmes-sur-puce (SoC). </p> <p>Dans ce contexte, la première contribution est la modélisation synchrone accompagnée d'une transformation d'applications en équations synchrones. Les modéles synchrones permettent de résoudre plusieurs questions liées à la validation formelle via l'usage des outils et techniques formels offerts par la technologie synchrone. Les transformations sont développées selon l'approche d'Ingénierie Dirigé par les Modèles (IDM). </p> <p>La deuxième contribution est une extension et amélioration des mécanismes de contrôle pour les calculs à haute performance, sous forme de constructeurs de langage de haut-niveau et de leur sémantique. Ils ont été défini afin de permettre la vérification, synthèse et génération de code. Il s'agit de déterminer un niveau d'abstraction de représentation des systèmes où soit extraite la partie contrôle, et de la modéliser sous forme d'automates à états finis. Ceci permet de spécifier et implémenter des changements de modes de calculs, qui se distinguent par exemple par les ressources utilisées, la qualité de service fournie, ou le choix d'algorithme remplissant une fonctionnalité. </p> <p>Ces contributions permettent l'utilisation d'outils d'analyse et vérification, tels que la vérification de propriétés d'assignement unique et dépendance acyclique, model checking. L'utilisation de techniques de synthèse de contrôleurs discrets est également traitée. Elles peuvent assurer la correction de faˆ on constructive: à partir d'une spécification partielle du contrôle, la partie manquante pour que les propriétés soient satisfaites est calculée. Grâce à ces techniques, lors du développement de la partie contrôle, la spécification est simplifiée, et le résultat est assuré d'être correct par construction. </p> <p>Les modélisations synchrone et de contrôle reposes sur MARTE et UML. Les travaux de cette thèse sont été partiellement implémentés dans le cadre de Gaspard, dédié aux applications de traitement de données intensives. Une étude de cas est présentée, dans laquelle nous nous intéressont à une application de système embarqué pour téléphone portable multimédia.</p>

Les systèmes embarqués actuels (téléphone portable, assistant personnel...) ne sont pas considérés<br />comme des hôtes de confiance car toute personne y ayant accès, sont des attaquants potentiels. Les données<br />contenues dans ces systèmes peuvent être sensibles (données privées du propriétaire, mot de passe, code d'un<br />logiciel...) et sont généralement échangées en clair entre le Système sur Puces (SoC – System on Chip) et la<br />mémoire dans laquelle elles sont stockées. Le bus qui relie ces deux entités constitue donc un point faible : un<br />attaquant peut observer ce bus et récupérer le contenu de la mémoire, ou bien a la possibilité d'insérer du code<br />afin d'altérer le fonctionnement d'une application s'exécutant sur le système. Afin de prévenir ce type d'attaque,<br />des mécanismes matériels doivent être mis en place afin d'assurer la confidentialité et l'intégrité des données.<br />L'approche conventionnelle pour atteindre cet objectif est de concevoir un mécanisme matériel pour chaque<br />service de sécurité (confidentialité et intégrité). Cette approche peut être implantée de manière sécurisée mais<br />empêche toute parallélisation des calculs sous-jacents.<br />Les travaux menés au cours de cette thèse ont dans un premier temps, consisté à faire une étude des<br />techniques existantes permettant d'assurer la confidentialité et l'intégrité des données. Dans un deuxième temps,<br />nous avons proposé deux mécanismes matériels destinés à la sécurisation des transactions entre un processeur et<br />sa mémoire. Un moteur de chiffrement et de contrôle d'intégrité parallélisé, PE-ICE (Parallelized Encryption and<br />Integrity Checking Engine) a été conçu. PE-ICE permet une parallélisation totale des opérations relatives à la<br />sécurité aussi bien en écriture qu'en lecture de données en mémoire. Par ailleurs, une technique basée sur une<br />structure d'arbre (PRV-Tree – PE-ICE protected Reference Values) comportant la même propriété de<br />parallélisation totale, a été spécifiée afin de réduire le surcoût en mémoire interne impliqué par les mécanismes de sécurité

Les systèmes sur puce intègrent sur un même substrat de silicium l'ensemble des organes nécessaires à la prise en charge des différentes fonctionnalités du système. Pour la partie dédiée aux traitements numériques, le microprocesseur central est souvent déchargé des applications critiques (traitement du signal et des images en général) par un accélérateur de traitement. C'est par rapport à l'architecture du coprocesseur que se pose la problématique de cette thèse. En effet, de nombreuses approches sont possibles pour ce dernier, et vouloir les comparer s'avère être une tâche complexe. Après avoir fait un état de l'art des différentes solutions architecturales de traitement flexibles, nous proposons un ensemble de métriques dans une optique de caractérisation. Nous illustrons alors notre méthode par la caractérisation et la comparaison d'architectures représentatives de l'état de l'art. Nous montrons que c'est par une exploitation efficace du parallélisme que les coprocesseurs peuvent améliorer significativement leurs performances. Or, malgré de réelles aptitudes, les accélérateurs ne sont pas toujours capables de tirer parti de ce potentiel. C'est pour cela que nous proposons une méthode générale de multiplexage matériel, qui permet d'améliorer les performances par l'exploitation du parallélisme dynamique (boucle et tâches). Par son application à un cas concret, un système baptisé Saturne, nous prouvons que par l'adjonction d'un contrôleur dédié au multiplexage matériel, les performances de l'accélérateur sont quasiment doublées, et ce avec un faible surcoût matériel.

La conception de systèmes embarqués modernes est de plus en plus complexe, car plus de fonctionnalités sont intégrées dans ces systèmes. En même temps, afin de répondre aux exigences de calcul tout en conservant une consommation d'énergie de faible niveau, MPSoCs sont apparus comme les principales solutions pour tels systèmes embarqués. En outre, les systèmes embarqués sont de plus en plus adaptatifs, comme l’adaptabilité peut apporter un certain nombre d'avantages, tels que la flexibilité du logiciel et l'efficacité énergétique. Cette thèse vise la conception sécuritaire de ces MPSoCs adaptatifs. Tout d'abord, chaque configuration de système doit être analysée en ce qui concerne ses propriétés fonctionnelles et non fonctionnelles. Nous présentons un cadre abstraite de conception et d’analyse qui permet des décisions d’implémentation plus rapide et plus rentable. Ce cadre est conçu comme un support de raisonnement intermédiaire pour les environnements de co-conception de logiciel / matériel au niveau de système. Il peut élaguer l'espace de conception à sa plus grande portée, et identifier les candidats de solutions de conception de manière rapide et efficace. Dans ce cadre, nous utilisons un codage basé sur l’horloge abstrait pour modéliser les comportements du système. Différents scénarios d'applications de mapping et de planification sur MPSoCs sont analysés via les traces d'horloge qui représentent les simulations du système. Les propriétés d'intérêt sont l’exactitude du comportement fonctionnel, la performance temporelle et la consommation d'énergie. Deuxièmement, la gestion de la reconfiguration de MPSoCs adaptatifs doit être abordée. Nous sommes particulièrement intéressés par les MPSoCs implémentés sur des architectures reconfigurables de hardware (ex. FPGA tissus) qui offrent une bonne flexibilité et une efficacité de calcul pour les MPSoCs adaptatifs. Nous proposons un cadre général de conception basésur la technique de la synthèse de contrôleurs discrets (SCD) pour résoudre ce problème. L’avantage principal de cette technique est qu'elle permet une synthèse d'un contrôleur automatique vis-à-vis d’une spécification donnée des objectifs de contrôle. Dans ce cadre, le comportement de reconfiguration du système est modélisé en termes d'automates synchrones en parallèle. Le problème de calcul de la gestion reconfiguration vis-à-vis de multiples objectifs concernant, par exemple, les usages des ressources, la performance et la consommation d’énergie est codé comme un problème de SCD . Le langage de programmation BZR existant et l’outil Sigali sont employés pour effectuer SCD et générer un contrôleur qui satisfait aux exigences du système. Finalement, nous étudions deux façons différentes de combiner les deux cadres de conception proposées pour MPSoCs adaptatifs. Tout d'abord, ils sont combinés pour construire un flot de conception complet pour MPSoCs adaptatifs. Deuxièmement, ils sont combinés pour présenter la façon dont le gestionnaire d'exécution conçu dans le second cadre peut être intégré dans le premier cadre de sorte que les simulations de haut niveau peuvent être effectuées pour évaluer le gestionnaire d'exécution. / The design of modern embedded systems is getting more and more complex, as more func- tionality is integrated into these systems. At the same time, in order to meet the compu- tational requirements while keeping a low level power consumption, MPSoCs have emerged as the main solutions for such embedded systems. Furthermore, embedded systems are be- coming more and more adaptive, as the adaptivity can bring a number of benefits, such as software flexibility and energy efficiency. This thesis targets the safe design of such adaptive MPSoCs. First, each system configuration must be analyzed concerning its functional and non- functional properties. We present an abstract design and analysis framework, which allows for faster and cost-effective implementation decisions. This framework is intended as an intermediate reasoning support for system level software/hardware co-design environments. It can prune the design space at its largest, and identify candidate design solutions in a fast and efficient way. In the framework, we use an abstract clock-based encoding to model system behaviors. Different mapping and scheduling scenarios of applications on MPSoCs are analyzed via clock traces representing system simulations. Among properties of interest are functional behavioral correctness, temporal performance and energy consumption. Second, the reconfiguration management of adaptive MPSoCs must be addressed. We are specially interested in MPSoCs implemented on reconfigurable hardware architectures (i.e., FPGA fabrics), which provide a good flexibility and computational efficiency for adap- tive MPSoCs. We propose a general design framework based on the discrete controller syn- thesis (DCS) technique to address this issue. The main advantage of this technique is that it allows the automatic controller synthesis w.r.t. a given specification of control objectives. In the framework, the system reconfiguration behavior is modeled in terms of synchronous parallel automata. The reconfiguration management computation problem w.r.t. multiple objectives regarding e.g., resource usages, performance and power consumption is encoded as a DCS problem. The existing BZR programming language and Sigali tool are employed to perform DCS and generate a controller that satisfies the system requirements. Finally, we investigate two different ways of combining the two proposed design frame- works for adaptive MPSoCs. Firstly, they are combined to construct a complete design flow for adaptive MPSoCs. Secondly, they are combined to present how the designed run-time manager by the second framework can be integrated into the first framework so that high level simulations can be performed to assess the run-time manager.

Les travaux présentés dans cette thèse portent sur la modélisation, la spécification et la vérification des modèlesdes Systèmes sur Puce (SoCs) au niveau d’abstraction transactionnel et à un niveau d’abstraction plus élevé.Les SoCs sont hétérogènes: ils comprennent des composants matériels et des processeurs pour réaliser le logicielincorporé, qui est en lien direct avec du matériel. La modélisation transactionnelle (TLM) basée sur SystemCa été très fructueuse à fournir des modèles exécutables des SoCs à un haut niveau d’abstraction, aussi appelésprototypes virtuels (VPs). Ces modèles peuvent être utilisés plus tôt dans le cycle de développement des logiciels,et la validation des matériels réels. La vérification basée sur assertions (ABV) permet de vérifier les propriétés tôtdans le cycle de conception de façon à trouver les défauts et faire gagner du temps et de l’effort nécessaires pourla correction de ces défauts. Les modèles TL peuvent être sur-contraints, c’est-à-dire qu’ils ne presentent pastous les comportements du matériel. Ainsi, ceci ne permet pas la détection de tous les défauts de la conception.Nos contributions consistent en deux parties orthogonales et complémentaires: D’une part, nous identifions lessources des sur-contraintes dans les modèles TLM, qui apparaissent à cause de l’ordre d’interaction entre lescomposants. Nous proposons une notion d’ordre mou qui permet la suppression de ces sur-contraintes. D’autrepart, nous présentons un mécanisme généralisé de stubbing qui permet la simulation précoce avec des prototypesvirtuels SystemC/TLM.Nous offrons un jeu de patrons pour capturer les propriétés d’ordre mou et définissons une transformationdirecte de ces patrons en moniteurs SystemC. Notre mécanisme généralisé du stubbing permet la simulationprécoce avec les prototypes virtuels SystemC/TLM, dans lesquels certains composants ne sont pas entièrementdéterminés sur les valeurs des données échangées, l’ordre d’interaction et/ou le timing. Ces composants nepossèdent qu’une spécification abstraite, sous forme de contraintes entre les entrées et les sorties. Nous montronsque les problèmes essentielles de la synchronisation entre les composants peuvent être capturés à l’aide de notresimulation avec les stubs. Le mécanisme est générique; nous mettons l’accent uniquement sur les concepts-clés,les principes et les règles qui rendent le mécanisme de stubbing implémentable et applicable aux études de casindustriels. N’importe quel language de spécification satisfaisant nos exigences (par ex. le langage des ordresmou) peut être utilisé pour spécifier les composants, c’est-à-dire il peut être branché au framework de stubbing.Nous fournissons une preuve de concept pour démontrer l’intérêt d’utiliser la simulation avec stubs pour ladétection anticipée et la localisation des défauts de synchronisation du modèle. / The work presented in this thesis deals with modeling, specification and testing of models of Systems-on-a-Chip (SoCs) at the transaction abstraction level and higher. SoCs are heterogeneous: they comprise bothhardware components and processors to execute embedded software, which closely interacts with hardware.SystemC-based Transaction Level Modeling (TLM) has been very successful in providing high-level executablecomponent-based models for SoCs, also called virtual prototypes (VPs). These models can be used early in thedesign flow for the development of the software and the validation of the actual hardware. For SystemC/TLMvirtual prototypes, Assertion-Based Verification (ABV) allows property checking early in the design cycle,helping to find bugs early in the model and to save time and effort that are needed for their fixing. TL modelscan be over-constrained, which means that they do not represent all the behaviors of the hardware, and thus,do not allow detection of some malfunctions of the prototype. Our contributions consist of two orthogonal andcomplementary parts: On the one hand, we identify sources of over-constraints in TL models appearing due tothe order of interactions between components, and propose a notion of loose-ordering which allows to removethese over-constraints. On the other hand, we propose a generalized stubbing mechanism which allows the veryearly simulation with SystemC/TLM virtual prototypes.We propose a set of patterns to capture loose-ordering properties, and define a direct translation of thesepatterns into SystemC monitors. Our generalized stubbing mechanism enables the early simulation with Sys-temC/TLM virtual prototypes, in which some components are not entirely determined on the values of theexchanged data, the order of the interactions and/or the timing. Those components have very abstract speci-fications only, in the form of constraints between inputs and outputs. We show that essential synchronizationproblems between components can be captured using our simulation with stubs. The mechanism is generic;we focus only on key concepts, principles and rules which make the stubbing mechanism implementable andapplicable for real, industrial case studies. Any specification language satisfying our requirements (e.g., loose-orderings) can be used to specify the components, i.e., it can be plugged in the stubbing framework. We providea proof of concept to demonstrate the interest of using the simulation with stubs for very early detection andlocalization of synchronization bugs of the design.

Les systèmes embarqués sur puce (SoC) envahissent notre vie quotidienne. Avec les progrès technologiques, ils intègrent de plus en plus de fonctionnalités complexes impliquant des charges de calcul et des tailles de mémoire importantes. Alors que leur complexité est une tendance clé, la consommation d’énergie est aussi devenue un facteur critique pour la conception de SoC. Dans ce contexte, nous avons étudié une approche de modélisation au niveau transactionnel qui associe à un modèle fonctionnel SystemC-TLM une description d’une structure de gestion d’un arbre d’horloge décrit au même niveau d’abstraction. Cette structure développée dans une approche de séparation des préoccupations fournit à la fois l’interface pour la gestion de puissance des composants matériels et pour le logiciel applicatif. L’ensemble des modèles développés est rassemblé dans une librairie ClkARCH. Pour appliquer à un modèle fonctionnel un modèle d’un arbre d’horloge, nous proposons une méthodologie en trois étapes : spécification, modélisation et simulation. Une étape de vérification en simulation est aussi considérée basée sur des contrats de type assertion. De plus, nos travaux visent à être compatibles avec des outils de conception actuels. Nous avons proposé une représentation d’une structure de gestion d’horloge et de puissance dans le standard IP-XACT permettant de produire les descriptions C++ des structures de gestion de puissance du SoC. Enfin, nous avons proposé une approche de gestion de puissance basée sur l’observation globale des états fonctionnels du système dans le but d’éviter ainsi des prises de décisions locales peu efficaces à une optimisation de l’énergie. / Embedded systems-on-chip (SoC) invade our daily life. With advances in semiconductor technology, these systems integrate more and more complex and energy-intensive features which generate increasing computation load and memory size requirements. While the complexity of these systems is a key trend, energy consumption has emerged as a critical factor for SoC designers. In this context, we have studied a modeling transactional level approach allowing a description of a clock tree and its management structure to be associated with a functional model, both described at the same abstraction level. This structure developed in a separation of concerns approach provides both the interface to the power consumption management of the hardware components and the application software. All the models developed are gathered in a C++ ClkArch library. To apply to a SystemC-TLM architecture model a clock tree intent with its control part, we propose a methodology based on three steps: specification, modeling and simulation. A verification step based on simulation is also considered using contracts of assertion type. This work aims to build a modelling approach on current design tools. So we propose a representation of a clock and power management structure in the IP-XACT standard allowing a C++ description of the SoC power management structures to be generated. Finally, a power management strategy based on the global functional states of the components of the system architecture is proposed. This strategy avoids local decision-making unsuited to optimized overall power/energy management.

Les systèmes embarqués modernes ont atteint un niveau de complexité qui fait qu'il n'est plus possible d'attendre les premiers prototypes physiques pour valider les décisions sur l'intégration des composants matériels et logiciels. Il est donc nécessaire d'utiliser des modèles, tôt dans le flot de conception. Les travaux présentés dans ce document contribuent à l'état de l'art dans plusieurs domaines. Nous présentons dans un premier temps de nouvelles techniques de vérification de programmes écrits dans des langages généralistes comme C, C++ ou Java. Dans un second temps, nous utilisons des outils de vérification formelle sur des modèles écrits en SystemC au niveau transaction (TLM). Plusieurs approches sont présentées, la plupart d'entre elles utilisent des techniques de compilations spécifiques à SystemC pour transformer le programme SystemC en un format utilisable par les outils. La seconde partie du document s'intéresse aux propriétés non-fonctionnelles des modèles~: performances temporelles, consommation électrique et température. Dans le contexte de la modélisation TLM, nous proposons plusieurs techniques pour enrichir des modèles fonctionnels avec des informations non-fonctionnelles. Enfin, nous présentons les contributions faites à l'analyse de performance modulaire (MPA) avec le calcul temps-réel (RTC). Nous proposons plusieurs connections entre ces modèles analytiques et des formalismes plus expressifs comme les automates temporisés et le langage de programmation Lustre. Ces connexion posent le problème théorique de la causalité, qui est formellement défini et résolu avec un algorithme nouveau dit de " fermeture causale ".