La conception d'une plate-forme matérielle pour un noeud de réseaux de capteurs (RdC) est un véritable défi car elle est soumise à des contraintes sévères. La consommation d'énergie est souvent considérée comme la contrainte la plus forte donnée la petite taille et les besoins d'autonomie d'un noeud. De nos jours, les noeuds s'appuient sur des microcontrôleurs (MCUs) faible consommation disponibles dans le commerce. Ces MCUs ne sont pas adaptés au contexte de RdC car ils sont basés sur une structure de calcul généraliste et ils consomment trop d'énergie par rapport au budget d'énergie d'un noeud. Dans cette thèse, nous proposons un flot de conception complet, depuis le niveau système, se basant sur le concept de micro-tâches matérielles avec coupure de la tension d'alimentation (Power Gating). Dans cette approche, l'architecture d'un noeud est constituée d'un ensemble de micro-tâches matérielles qui sont activées selon un principe événementiel, chacune étant dédiée à une tâche spécifique du système (ex. la couche MAC, le routage, etc.). Ces micro-tâches sont gérées par un ordonnanceur matériel (System Monitor) qui est automatiquement généré à partir d'une description système, dans un langage spécifique (DSL), du graphe des tâches d'un noeud de RdC. En combinant la spécialisation du matériel et la technique du power gating, nous réduisons considérablement les énergies dynamique et statique d'un noeud de RdC. Les résultats montrent que des gains en énergie dynamique de 1 à 2 ordres de grandeur sont possibles par rapport aux mises en oeuvre à base des MCUs (ex. le MSP430). De plus, des gains de 1 ordre de grandeur en énergie statique sont également obtenus grâce à l'utilisation du power gating.

Le nombre de transistors dans une puce augmente constamment en suivant la conjecture de Moore, qui dit que le nombre de transistors dans une puce double tous les 2 ans. On arrive donc aujourd’hui à des systèmes d’une telle complexité que l’exploration architecturale ou le développement, même parallèle, de la conception de la puce et du code applicatif prend trop de temps. Pour réduire ce temps, la solution généralement admise consiste à développer des plateformes virtuelles reproduisant le comportement de la puce cible. Avoir une haute vitesse de simulation est essentiel pour ces plateformes, notamment pour les systèmes many-cœurs à cause du grand nombre de cœurs à simuler. Nous nous focalisons donc dans cette thèse sur la simulation native, dont le principe est de compiler le code source directement pour l’architecture hôte, offrant ainsi un temps de simulation que l’on peut espérer optimal. Mais un certain nombre de caractéristiques fonctionnelles spécifiques au cœur cible peuvent ne pas être présentes sur le cœur hôte. L’utilisation de l’assistance matérielle à la virtualisation (HAV) comme base pour la simulation native vient renforcer la dépendance de la simulation du cœur cible par rapport aux caractéristiques du cœur hôte. Nous proposons dans ce contexte un moyen de simuler les caractéristiques fonctionnelles spécifiques du cœur cible en simulation native basée sur le HAV. Parmi les caractéristiques propres au cœur cible, l’unité de calcul à virgule flottante est un élément important, bien trop souvent négligé en simulation native conduisant certains calculs à donner des résultats différents entre le cœur cible et le cœur hôte. Nous nous restreignons au cas de la simulation compilée et nous proposons une méthodologie permettant de simuler correctement les opérations de calcul à virgule flottante. Finalement la simulation native pose des problèmes de passage à l’échelle. Des problèmes de découplage temporel amènent à simuler inutilement certaines instructions lors de procédures de synchronisation entre des tâches s’exécutant sur les cœurs cibles, conduisant à une réduction de la vitesse de simulation. Nous proposons des solutions pour permettre un meilleur passage à l’échelle de la simulation native. / The number of transistors in one chip is increasing following Moore’s conjecture which says that the number of transistors per chip doubles every two years. Current systems are so complex that chip design and specific software development for one chip take too much time even if software development is done in parallel with the design of the hardware architecture, often because of system integration issues. To help reducing this time, the general solution consists of using virtual platforms to reproduce the behavior of the target chip. The simulation speed of these platforms is a major issue, especially for many-core systems in which the number of programmable cores is really high. We focus in this thesis on native simulation. Its principle is to compile source code directly for the host architecture to allow very fast simulation, at the cost of requiring "equivalent" features on the target and host cores.However, some target core specific features can be missing in the host core. Hardware Assisted Virtualization (HAV) is used to ease native simulation but it reinforces the dependency of the target chip simulation regarding the host core capabilities. In this context, we propose a solution to simulate the target core functional specific features with HAV based native simulation.Among target core features, the floating point unit is an important element which is neglected in native simulation leading to potential functional differences between target and host computation results. We restrict our study to the compiled simulation technique and we propose a methodology ensuring to accurately simulate floating point computations while still keeping a good simulation speed.Finally, native simulation has a scalability issue. Time decoupling problems generate unnecessary code simulation during synchronisation protocols between threads executed on the target cores, leading to an important decrease of simulation speed when the number of cores grows. We address this problem and propose solutions to allow a better scalability for native simulation.

Cette thèse porte sur la modélisation des systèmes-sur-puce au niveau transactionnel, une approche connue sous le nom de prototypage virtuel. Les prototypes virtuels sont d'un grand intérêt industriel parce qu'ils permettent de démarrer certaines activités (telles que le développement du logiciel embarqué) plus tôt dans le flot de conception. Du fait que cette approche est relativement nouvelle, un grand nombre de problèmes de modélisation sont encore ouverts. En particulier, il est essentiel de comprendre à quel point un modèle donné est proche du système hypothétique qu'il est sensé représenter. C'est un problème difficile car nous n'avons pas les moyens de réaliser une comparaison objective, vu que le système modélisé n'est pas disponible physiquement au moment de la modélisation. Nous avons besoin d'une méthodologie pour traiter ces difficultés, qui s'étendent au-delà de simples exigences objectives et de l'analyse de besoin fonctionnel. Dans ce contexte, l'industrie cherche des directives de modélisation claires, fondées sur l'expérience et l'identification des pratiques actuelles et des problèmes récurrents. Dans cette thèse, nous présentons une étude compréhensive d'un large éventail de considérations techniques impliquées dans le flot de conception du logiciel et du matériel qui constituent un système-sur-puce typique. Nous utilisons ces connaissances pour identifier une source particulière de divergence entre le modèle et le système modélisé. Nous montrons que cette divergence masque certains bogues du logiciel sur le prototype virtuel. Nous mettons en évidence la pratique de modélisation à l'origine de cette situation. Deuxièmement, nous essayons d'identifier des problèmes liés à l'utilisation du langage de modélisation dans les pratiques actuelles. Nous prétendons que, d'une part, ces problèmes sont dûs à la confusion entre les concepts de la modélisation transactionnelle et leur implémentation dans le langage standard de l'industrie ; et d'autre part que ce n'est qu'en menant des comparaisons avec un autre langage que l'on pourrait quantifier leur étendue. Pour ce faire, nous proposons un cadre d'application spécialement conçu pour guider l'étude des concepts fondamentaux de la modélisation transactionnelle. Entre autres, nous introduisons une nouvelle méthode pour la modélisation du temps dans les simulateurs à événements discrets. Cette méthode dévoile la différence entre une action instantanée et une tâche avec durée. Ensuite, elle l'exploite de plusieurs manières : pour enrichir les outils de visualisation de traces ; pour dériver une définition claire de chevauchement de tâches ; pour accélérer la simulation à moindre effort, en parallélisant l'exécution d'actions se déroulant à des temps simulés différents ; et pour révéler des bogues subtiles en tenant compte du fait que les actions à des temps simulés différents ne sont pas forcément synchronisées. / This thesis deals with modeling of Systems-on-a-Chip (SoC) at the Transactional Level (TLM), an approach also known as virtual prototyping. Virtual prototypes are of special industrial interest because they allow some activities (such as embedded software development) to start earlier in the design flow. Because this approach is relatively new, several modeling issues are still open. In particular, there is an increasing need for understanding how close a given model is to the hypothetical system it is intended to represent. This is a difficult problem specially because we lack a way to perform an objective comparison, since the modeling activity is prior to the physical existence of the modeled system. A methodology is required to address these concerns, going beyond classical objective and functional quality requirements. In this context, the industry searches for clear modeling guidelines based on experience and the identification of the current modeling practices and known recurring problems. In this thesis, we present a comprehensive study of a range of technical considerations involved in the design flow of the hardware and software that constitutes a typical SoC. We use this knowledge to identify one particular source of divergence between the model and the modeled system. We show that this divergence causes some software bugs to become hidden in the virtual prototype and we correlate this situation to the corresponding modeling practice. Secondly, we attempt to identify language-dependency issues in the modeling practices. We claim that it is only by confronting with an alternative language that we could measure the extent to which common modeling issues were caused by mixing up conceptual transaction-level modeling with its implementation in the current industry standard language. Therefore, we propose a complete experimentation framework specifically designed to help in the study of fundamental concepts beneath TLM. Amongst other features, this framework introduces a novel approach to modeling time in discrete-event simulators that distinguishes between instantaneous actions and tasks that take time. We show that this notion can be exploited to enrich trace visualization tools; to derive a clear definition of overlapping tasks; to effortlessly achieve an important simulation speedup by enabling parallel execution of actions occurring at different simulation times; and to expose subtle bugs by removing the constraint that actions at different simulation times are necessarily synchronized.

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.

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".

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.

L'exploration de l'espace de conception au niveau système est effectuée tôt dans le flot de conception des systèmes embarqués et des systèmes sur puce. L'objectif est d'identifier un partitionnement matériel / logiciel approprié qui réponde à un ensemble de contraintes concernant la fonctionnalité, la performance, la surface de silicium, la consommation d'énergie, etc. Lors des étapes de conception précoces, des modèles de système précis, tels que des modèles RTL, peuvent être encore indisponibles. Par ailleurs, la complexité de ces modèles présente l'inconvénient d'être exigeant et lent dans la vérification. Il est communément admis que le seul remède à ce problème est l'abstraction, ce qui a engendré l'apparition de plates-formes virtuelles basées sur des techniques telles que la modélisation au niveau transactionnel. Étant non fonctionnels, les modèles \textit{approximately timed} vont encore plus loin en faisant l'abstraction de données simplement selon leur présence ou absence et en introduisant des instructions symboliques. La méthodologie DIPLODOCUS et son profil UML correspondant réalisent les abstractions susmentionnées. La méthodologie s'appuie sur l'approche en Y, qui traite des fonctionnalités (appelées application) et leur réalisation (appelée architecture) de manière orthogonale. La sémantique formelle de DIPLODOCUS ouvre conjointement la voie à la simulation et à la vérification formelle, ce qui a été démontré préalablement a ce travail. Cette thèse propose des améliorations à la méthodologie qui permettent la vérification des propriétés fonctionnelles et non fonctionnelles. Au début, nous nous concentrons sur la façon dont les propriétés fonctionnelles sont exprimées. Puisque la vérification des modèles de haut niveau est habituellement réalisée avec la logique temporelle, nous suggérons une façon plus intuitive qui correspond au niveau d'abstraction du modèle qui doit être vérifié. Le langage graphique, mais formel nommé TEPE est la première contribution de ce travail. Pour atteindre un niveau élevé de confiance en vérification dans un délai raisonnable, le modèle doit être exécuté efficacement. La deuxième contribution vise donc une sémantique d'exécution pour les modèles DIPLODOCUS et une stratégie de simulation qui s'appuie sur l'abstraction. L'avantage est qu'une granularité grossière du modèle d'application se traduit directement par une augmentation de la vitesse de simulation. Comme troisième contribution, nous présentons un compromis entre la couverture limitée de la simulation et l'exhaustivité des techniques formelles. Lorsqu'il s'agit de modèles complexes, l'exhaustivité peut être entravée par le problème d'explosion combinatoire. En raison de l'abstraction de données, les modèles d'application DIPLODOCUS comportent des opérateurs non-déterministes. La simulation à couverture élargie vise à exploiter un sous-ensemble, ou bien l'intégralité, des valeurs des variables aléatoires. Par conséquent, une analyse statique des modèles DIPLODOCUS est effectuée et les informations caractérisant la partie significative de l'espace d'état de l'application sont propagées au simulateur. Enfin, nous fournissons des preuves de l'applicabilité des contributions par le biais d'une étude de cas dans le domaine du traitement du signal. Il sera démontré que les propriétés courantes se traduisent aisément en TEPE. Par ailleurs, la simulation rapide et sa couverture élargie fournissent des indications pertinentes qui sont susceptibles d'aider le développeur à configurer une plate-forme radio logicielle.

Le secteur Semi-conducteurs avec l'avènement de fabrication submicroniques coule dessous de 45 nm ont commencé à relever de nouveaux défis pour continuer à évoluer en fonction de la loi de Moore. En ce qui concerne l'adoption généralisée de systèmes embarqués une contrainte majeure est devenu la consommation d'énergie de l'IC. En outre, les technologies de mémoire comme le standard actuel de la technologie de mémoire intégré pour la hiérarchie de la mémoire, la mémoire SRAM, ou le flash pour le stockage non-volatile ont des contraintes complexes extrêmes pour être en mesure de produire des matrices de mémoire aux nœuds technologiques 45 nm ci-dessous. Un important est jusqu'à présent mémoire non volatile n'a pas été adopté dans la hiérarchie mémoire, en raison de sa densité et comme le flash sur la nécessité d'un fonctionnement multi-tension.Ces thèses ont fait, par le travail dans l'objectif de ces contraintes et de fournir quelques réponses. Dans la thèse sera présenté méthodes et les résultats extraits de ces méthodes pour corroborer notre objectif de définir une feuille de route à adopter une nouvelle technologie de mémoire non volatile, de faible puissance, à faible fuite, SEU / MEU-résistant, évolutive et avec similaire le rendement en courant de la SRAM, physiquement équivalente à SRAM, ou encore mieux, avec une densité de surface de 4 à 8 fois la surface d'une cellule SRAM, sans qu'il soit nécessaire de domaine multi-tension comme FLASH. Cette mémoire est la MRAM (mémoire magnétique), selon l'ITRS avec un candidat pour remplacer SRAM dans un proche avenir. MRAM au lieu de stocker une charge, ils stockent l'orientation magnétique fournie par l'orientation de rotation-couple de l'alliage sans la couche dans la MTJ (Magnetic Tunnel Junction). Spin est un état quantical de la matière, que dans certains matériaux métalliques peuvent avoir une orientation ou son couple tension à appliquer un courant polarisé dans le sens de l'orientation du champ souhaitée.Une fois que l'orientation du champ magnétique est réglée, en utilisant un amplificateur de lecture, et un flux de courant à travers la MTJ, l'élément de cellule de mémoire de MRAM, il est possible de mesurer l'orientation compte tenu de la variation de résistance, plus la résistance plus faible au passage de courant, le sens permettra d'identifier un zéro logique, diminuer la résistance de la SA détecte une seule logique. Donc, l'information n'est pas une charge stockée, il s'agit plutôt d'une orientation du champ magnétique, raison pour laquelle il n'est pas affecté par SEU ou MEU due à des particules de haute énergie. En outre, il n'est pas dû à des variations de tensions de modifier le contenu de la cellule de mémoire, le piégeage charges dans une grille flottante.En ce qui concerne la MRAM, cette thèse a par adresse objective sur les aspects suivants: MRAM appliqué à la hiérarchie de la mémoire:- En décrivant l'état actuel de la technique dans la conception et l'utilisation MRAM dans la hiérarchie de mémoire;- En donnant un aperçu d'un mécanisme pour atténuer la latence d'écriture dans MRAM au niveau du cache (Principe de banque de mémoire composite);- En analysant les caractéristiques de puissance d'un système basé sur la MRAM sur Cache L1 et L2, en utilisant un débit d'évaluation dédié- En proposant une méthodologie pour déduire une consommation d'énergie du système et des performances.- Et pour la dernière base dans les banques de mémoire analysant une banque mémoire Composite, une description simple sur la façon de générer une banque de mémoire, avec quelques compromis au pouvoir, mais la latence équivalente à la SRAM, qui maintient des performances similaires.

Les architectures des systèmes sur puce (System-on-Chip, SoC) actuelles intègrent de nombreux composants différents tels que les processeurs, les accélérateurs, les mémoires et les blocs d'entrée/sortie, certains pouvant contenir des caches. Vu que l'effort de validation basée sur la simulation, actuellement utilisée dans l'industrie, croît de façon exponentielle avec la complexité des SoCs, nous nous intéressons à des techniques de vérification formelle. Nous utilisons la boîte à outils CADP pour développer et valider un modèle formel d'un SoC générique conforme à la spécification AMBA 4 ACE récemment proposée par ARM dans le but de mettre en œuvre la cohérence de cache au niveau système. Nous utilisons une spécification orientée contraintes pour modéliser les exigences générales de cette spécification. Les propriétés du système sont vérifié à la fois sur le modèle avec contraintes et le modèle sans contraintes pour détecter les cas intéressants pour la cohérence de cache. La paramétrisation du modèle proposé a permis de produire l'ensemble complet des contre-exemples qui ne satisfont pas une certaine propriété dans le modèle non contraint. Notre approche améliore les techniques industrielles de vérification basées sur la simulation en deux aspects. D'une part, nous suggérons l'utilisation du modèle formel pour évaluer la bonne construction d'une unité de vérification d'interface. D'autre part, dans l'objectif de générer des cas de test semi-dirigés intelligents à partir des propriétés de logique temporelle, nous proposons une approche en deux étapes. La première étape consiste à générer des cas de tests abstraits au niveau système en utilisant des outils de test basé sur modèle de la boîte à outils CADP. La seconde étape consiste à affiner ces tests en cas de tests concrets au niveau de l'interface qui peuvent être exécutés en RTL grâce aux services d'un outil commercial de génération de tests dirigés par les mesures de couverture. Nous avons constaté que notre approche participe dans la transition entre la vérification du niveau interface, classiquement pratiquée dans l'industrie du matériel, et la vérification au niveau système. Notre approche facilite aussi la validation des propriétés globales du système, et permet une détection précoce des bugs, tant dans le SoC que dans les bancs de test commerciales. / State-of-the-art System-on-Chip (SoC) architectures integrate many different components, such as processors, accelerators, memories, and I/O blocks. Some of those components, but not all, may have caches. Because the effort of validation with simulation-based techniques, currently used in industry, grows exponentially with the complexity of the SoC, this thesis investigates the use of formal verification techniques in this context. More precisely, we use the CADP toolbox to develop and validate a generic formal model of a heterogeneous cache-coherent SoC compliant with the recent AMBA 4 ACE specification proposed by ARM. We use a constraint-oriented specification style to model the general requirements of the specification. We verify system properties on both the constrained and unconstrained model to detect the cache coherency corner cases. We take advantage of the parametrization of the proposed model to produce a comprehensive set of counterexamples of non-satisfied properties in the unconstrained model. The results of formal verification are then used to improve the industrial simulation-based verification techniques in two aspects. On the one hand, we suggest using the formal model to assess the sanity of an interface verification unit. On the other hand, in order to generate clever semi-directed test cases from temporal logic properties, we propose a two-step approach. One step consists in generating system-level abstract test cases using model-based testing tools of the CADP toolbox. The other step consists in refining those tests into interface-level concrete test cases that can be executed at RTL level with a commercial Coverage-Directed Test Generation tool. We found that our approach helps in the transition between interface-level and system-level verification, facilitates the validation of system-level properties, and enables early detection of bugs in both the SoC and the commercial test-bench.