Soutenance mémoire
Depuis l’avènement de l’informatique au milieu du vingtième siècle, son usage dans nos sociétés n’a cessé de grandir. Elle occupe aujourd’hui une place importante dans notre quotidien : ordinateur de bureau, ordinateur personnel, smartphone, smart TV, etc. Il devient de plus en plus indispensable pour les individus d’avoir accès à un système informatique et à un réseau de communications, que ce soit pour le travail, pour les déplacements, pour les achats de premières nécessités ou pour les loisirs. L’accès aux systèmes informatiques est alors un facteur d’intégration sociale, entre autres, de par la transition des réseaux sociaux vers le numérique. Cette augmentation massive des systèmes informatiques est, de plus, généralisée dans tous les pays du globe.
L’utilisation grandissante de l’informatique se traduit notamment par de nombreux systèmes embarqués. Bien qu’invisibles pour la plupart des utilisateurs, ils occupent une large partie de cas d’usage de l’informatique au quotidien : ABS ou régulateur pour l’automobile, capteurs optiques pour la maintenance de réseaux ferroviaires, routeurs pour les réseaux de téléphonie, moniteurs de glucose ou de tension pour les suivis médicaux, etc. L’émergence de l’Internet des Objets (IoT), dont la plupart des nœuds du réseau sont des systèmes embarqués, a grandement renforcé leur utilisation. La conception du système est spécifique à chaque application, elle nécessite une optimisation qui lui est propre. De nombreux travaux s’intéressent à la conception de « petits » systèmes, consommant un minimum de ressources matérielles et énergétiques. On pourrait penser que l’objectif est de réduire la consommation liée aux utilisations existantes (sobriété technologique). Mais il s’agit en fait, d’une volonté des industries de création de nouvelles utilisations de systèmes embarqués. Comme le montre ces travaux [KRP16], la vente de systèmes électroniques n’a cessé d’augmenter depuis les 30 dernières années (dans cette étude l’échelle d’un pays, la Suède). Par exemple, dans le domaine de l’automobile, depuis les années 70 les constructeurs ont peu à peu remplacé des systèmes de contrôle mécaniques par des systèmes électroniques [Lar14]. Ainsi, en 1977 les composants électroniques constituaient 5% du prix du véhicule, dans les années 2010 ils constituent 40% du prix. Récemment, ces « petits » systèmes trouvent toute leur utilité dans le Edge Computing, consistant à traiter les données au plus proche du point d’acquisition, qui s’inscrit dans la démarche de l’Internet des Objets. En effet, une application typique de Edge Computing n’a pas besoin d’une grande rapidité de traitement, mais nécessite une faible consommation énergétique.
Méthodes formelles
Ensembles
N et N∗ sont respectivement les ensembles des entiers naturels et des entiers naturels non nuls. R+ et R+∗ sont respectivement les ensembles des réels positifs ou nuls et réels strictement positifs. B = {⊥, ⊤} est le domaine booléen.
Les opérateurs usuels +, −, <, ≤, >, ≥ et = sont appliqués sur les vecteurs de dimension n dans Nn , Rn+ et Rn+∗ , et sont les extensions point par point de leurs homologues dans N, N∗, R+ et R+∗. Les opérateurs logiques usuels ∧, ∨ et ¬ sont appliqués aux éléments de B.
Logiques temporelles
Des logiques temporelles ont été introduites pour décrire des comportements temporels des modèles formels. Les logiques Linear Temporal Logic (LTL) et Computation Tree Logic (CTL) permettent de décrire des propriétés sur le temps logique. LTL décrit des propriétés sur les exécutions. Elle a été introduite dans [Pnu77], nous rappelons ici uniquement sa syntaxe :
Définition 6 (Syntaxe LTL). Soit un ensemble de variables propositionnelles AP. L’ensemble des formules LTL sur AP est défini de manière inductive :
— si p ∈ AP alors p est une formule LTL ;
— si φ et ψ sont des formules LTL alors ¬φ, φ ∨ ψ, Xψ et φUψ sont des formules LTL.
X et U se lisent respectivement « Next » et « Until ».
Des opérateurs additionels peuvent être construit à partir de ces opérateurs fondamentaux. Sans être exhaustif, nous utiliserons deux opérateurs logiques additionnels ∧ (conjonction) et ⇒ (implication), ainsi qu’un opérateur temporel additionnel G qui se lit « Globally » (toujours). La logique CTL introduite par [CES86], décrit des propriétés sur les arbres d’exécutions. Enfin, une extension de la logique CTL a été proposé par [AD94], la logique Timed Computation Tree Logic (TCTL), qui permet de décrire des propriétés sur le temps dense. Nous ne rappelons pas leurs définitions ici.
Conception de circuits
Formats de données
En arithmétique des ordinateurs, il existe deux représentations principales des nombres réels : la représentation en virgule fixe et la représentation en virgule flottante. La représentation en virgule fixe attribue un nombre de bits à la partie entière et un nombre de bits à la partie décimale.
Définition (Représentation en virgule fixe). La représentation en virgule fixe est en fait une représentation entière avec un facteur de mise à l’échelle fixe. En base 2, une représentation par le nombre entier k, avec un facteur de mise à l’échelle s, encode le nombre k ∗ 2−s .
On nomme la puissance du bit de poids fort Most-Significant Bit (MSB) et celle du bit de poids faible Least-Significant Bit (LSB). Une représentation en virgule fixe sur n bits, avec un facteur de mise à l’échelle s, a un MSB de n − s − 1 et un LSB de −s. Pour encoder un réel négatif, on utilisera une représentation signée comme pour la représentation d’entier relatif (généralement le complément à deux). La représentation en virgule flottante n’a pas un nombre de bits fixes pour la partie entière et la partie décimale.
Définition (Représentation en virgule flottante). La représentation en virgule flottante est composée de trois valeurs : le signe s (égal à −1 ou 1), la mantisse m et l’exposant e. En base 2, cette représentation encode le nombre s ∗ m ∗ 2e . Deux formats, fixés par la norme IEEE 754, sont généralement utilisés :
— simple précision : sur 32 bits, avec 1 bit pour le signe, 23 bits pour la mantisse et 8 bits pour l’exposant.
— double précision : sur 64 bits, avec 1 bit pour le signe, 52 bits pour la mantisse et 11 bits pour l’exposant.
|
Table des matières
Introduction
1 Prérequis
1.1 Méthodes formelles
1.1.1 Ensembles
1.1.2 Système de Transition
1.1.3 Bisimulation
1.1.4 Logiques temporelles
1.2 Conception de circuits
1.2.1 Formats de données
1.2.2 Circuit logique programmable
2 Un modèle formel pour les circuits pipelinés
2.1 Modéliser un circuit synchrone
2.1.1 Automates temporisés
2.1.2 Extension des Réseaux de Petri avec du temps
2.1.3 Notre choix
2.2 Réseau de Petri
2.2.1 Définition
2.2.2 Sémantique d’entrelacement
2.2.3 Sémantique à pas maximaux
2.2.4 Expressivité
2.3 Réseau de Petri Temporisé
2.3.1 Tir en trois phases
2.3.2 Définition
2.3.3 Comparaison tir atomique / tir en trois phases
2.4 Réseau de Petri Temporisé avec reset et transitions retardables
2.4.1 Définition
2.4.2 Exemple
2.5 Réseau de Petri Temporisé avec transitions retardables
2.5.1 Reset explicite
2.5.2 Définition
3 Propriétés des Réseaux de Petri Temporisés avec transitions retardables (DTPNs)
3.1 Expressivité des DTPNs par rapport aux classes à intervalles
3.1.1 Définitions des différentes classes
3.1.2 Expressivité des classes DTPN et DTPNdt
3.1.3 Les classes en temps dense
3.1.4 Les classes en temps discret
3.2 Une sémantique symbolique pour les DTPNs
3.2.1 Le délai dynamique
3.2.2 Les états symboliques
3.2.3 La sémantique symbolique
3.3 Expressivité des RTPNs
3.3.1 Sémantique symbolique pour les RTPNs
3.3.2 Définition d’un Automate Temporisé
3.3.3 Traduction vers un automate temporisé à une horloge
3.3.4 Corollaires sur le langage
3.4 Complexité théorique et pratique
3.4.1 Problèmes d’accessibilité
3.4.2 Calcul du successeur symbolique
3.5 Algorithmes d’exploration de l’espace d’états symboliques
3.5.1 Successeur d’un état
3.5.2 Successeurs d’un état symbolique
3.5.3 Graphe d’états symboliques
4 Synthèse de pipeline d’un circuit synchrone
4.1 Définition du problème
4.1.1 Qu’est-ce qu’un circuit synchrone ?
4.1.2 Le pipeline
4.1.3 Le pliage
4.2 Synthèse de pipeline
4.2.1 Bibliographie
4.2.2 Algorithme glouton
4.2.3 Leiserson & Saxe
4.3 Synthèse de pipeline à partir d’un modèle RTPN
4.3.1 Bibliographie
4.3.2 Modélisation d’un circuit synchrone par un RTPN
4.3.3 Construction du pipeline
4.3.4 Résultats expérimentaux
4.4 Synthèse de pliage
4.4.1 Bibliographie
4.4.2 Synthèse de pliage avec RTPN
4.4.3 En pratique
5 Application : compilation Simulink vers VHDL
Conclusion
