Mes activités de recherche se situent dans le domaine de l'implantation efficace d'applications de traitement du signal et de l'image (TDSI) au sein de systèmes embarqués. Face à la complexité grandissante des applications implantées au sein des systèmes embarqués, et face à la nécessité de réduire les temps de mise sur le marché, des méthodes et les outils associés sont nécessaires pour automatiser le processus d'implantation de ces applications sur des plateformes embarquées. A l'interface entre les phases de conception des algorithmes de TDSI et d'implantation au sein des systèmes embarqués, la conversion en virgule fixe reste une tache longue, fastidieuse et source d'erreurs. L'objectif de nos travaux de recherche est de proposer une méthodologie efficace de conversion automatique en virgule fixe et de développer les outils associés. De plus, la mise en œuvre de techniques permettant d'optimiser l'implantation d'applications au sein de systèmes embarqués a été étudiée. Plus particulièrement, les applications de communication numérique, les aspects énergétiques et la représentation optimisée des données en virgule fixe ont été considérés. Dans le processus de conversion en virgule fixe, l'évaluation des effets de la précision finie sur les performances de l'application est l'un des problèmes majeurs. Différents travaux de recherche ont permis de définir une approche analytique d'évaluation de la précision basée sur la théorie de la perturbation. Cette approche détermine l'expression de la puissance du bruit de quantification pour les systèmes composés d'opérations dont le modèle de bruit peut être linéarisé. Pour traiter les systèmes intégrant des opérations dont le modèle de bruit n'est pas linéaire, une approche mixte combinant simulation et méthodes analytiques a été proposée. Différentes contributions pour l'automatisation du processus de conversion en virgule fixe ont été proposées. Elles concernent l'évaluation de la dynamique à travers des approches stochastiques, l'optimisation de la largeur des données dans le cas de la synthèse d'architectures et la définition d'une approche hiérarchique pour traiter des systèmes complexes. Une infrastructure logicielle a été développée pour réaliser la conversion en virgule fixe et évaluer efficacement la précision des calculs. Différents travaux ont été conduits sur l'implantation d'applications de communication numérique au sein de systèmes embarqués et sur la génération de blocs matériels dédiés. De plus, le concept d'adaptation dynamique de la précision a été proposé et une architecture reconfigurable et flexible, supportant l'ADP, a été développée.

Sur des architectures récentes, un programme numérique peut donner des réponses différentes en fonction du hardware et du compilateur. Ces incohérences des résultats viennent du fait que chaque calcul en virgule flottante est effectué avec des précisions différentes. Le but de cette thèse est de prouver formellement des propriétés des programmes opérant sur des nombres flottants en prenant en compte l’architecture et le compilateur. Pour le faire, nous avons proposé deux approches différentes. La première approche est de prouver des propriétés des programmes en virgule flottante qui sont vraies sur plusieurs architectures et compilateurs. Cette approche ne considère que les erreurs d’arrondi qui doivent être validées quels que soient l’environnement matériel et le choix du compilateur. Elle est implantée dans la plate-forme Frama-C pour l’analyse statique de code C. La deuxième approche consiste à prouver des propriétés des programmes en analysant leur code assembleur. Nous nous concentrons sur des problèmes et des pièges qui apparaissent sur des calculs en virgule flottante. L’analyse directe du code assembleur nous permet de considérer des caratéristiques dépendant de l’architecture ou du compilateur telle que l’utilisation des registres en précision étendue. Cette approche est implantée comme une sur-couche de la plate-forme Why pour la vérification déductive. / On some recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. These discrepancies of the results come from the fact that each floating-point computation is calculated with different precisions. The goal of this thesis is to formally prove properties about numerical programs while taking the architecture and the compiler into account. In order to do that, we propose two different approaches. The first approach is to prove properties of floating-point programs that are true for multiple architectures and compilers. This approach states the rounding error of each floating-point computation whatever the environment and the compiler choices. It is implemented in the Frama-C platform for static analysis of C code. The second approach is to prove behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. It is implemented above the Why platform for deductive verification

Les applications multimédia se composent généralement de blocs numériques exhibant des schémas de calcul flottant réguliers. Sur les processeurs sans support architectural pour l'arithmétique flottante, ils peuvent être profitablement transformés en opérateurs dédiés, s'ajoutant aux 5 opérateurs élémentaires (+, -, X, / et √) : en traitant plus d'opérations simultanément, ils permettent d'obtenir de meilleures performances. Cette thèse porte sur la conception de tels opérateurs, et les techniques de compilation mises en œuvre pour les sélectionner. Nous avons réalisé des implémentations optimisées pour un ensemble d'opérateurs dédiés : élévation au carré, mise à l'échelle, fused multiply-add, produit scalaire en dimension deux (DP2), addition/soustraction simultané et sinus/cosinus simultanés. En proposant de nouveaux algorithmes cherchant à maximiser le parallélisme d'instructions et détaillés ici, nous obtenons des accélérations d'un facteur allant jusqu'à 4.2 par appel. Nous détaillons également les changements apportés dans le compilateur pour effectuer la sélection. La plupart des opérateurs sont sélectionnés au niveau syntaxique. Cependant, pour certains opérateurs, nous avons dû améliorer l'analyse d'intervalles entiers pour prendre en compte les variables de type flottant, afin de prouver certaines conditions de positivité requises à leur sélection. Enfin, nous apportons la preuve en pratique de la pertinence de cette approche : sur des noyaux typiques du traitement du signal et sur certaines applications, nous mesurons une amélioration de performance allant jusqu'à 1.59x en comparaison avec la performance obtenue avec les seuls opérateurs élémentaires. / Media processing applications typically involve numerical blocks that exhibit regular floating-point computation patterns. For processors whose architecture supports only integer arithmetic, these patterns can be profitably turned into custom operators, coming in addition to the five basic ones (+, -, X, / and √), but achieving better performance by treating more operations. This thesis addresses the design of such custom operators as well as the techniques developed in the compiler to select them in application codes. We have designed optimized implementations for a set of custom operators which includes squaring, scaling, adding two nonnegative terms, fused multiply-add, fused square-add (x*x+z, with z>=0), two-dimensional dot products (DP2), sums of two squares, as well as simultaneous addition/subtraction and sine/cosine. With novel algorithms targeting high instruction-level parallelism and detailed here for squaring, scaling, DP2, and sin/cos, we achieve speedups of up to 4.2x for individual custom operators even when subnormal numbers are fully supported. Furthermore, we introduce the optimizations developed in the ST231 C/C++ compiler for selecting such operators. Most of the selections are achieved at high level, using syntactic criteria. However, for fused square-add, we also enhance the framework of integer range analysis to support floating-point variables in order to prove the required positivity condition z>= 0. Finally, we provide quantitative evidence of the benefits to support this selection of custom operations: on DSP kernels and benchmarks, our approach allows us to be up to 1.59x faster compared to the sole usage of basic ones.

RESUME A partir de lanalyse des incidents des FSOs de type CALM Soft Yoke de Vietsovpetro aux gisements White Tiger (Tigre Blanc) et Dragon, on saperçoit du besoin de développer des structures offshore (y compris les FPSOs) installées et opérées «en sécurité» dans les conditions spéciales des états de mer du Vietnam, où apparaissent de nombreux vents violents et de fréquents typhons tropicaux. Dans le cadre de cette thèse, une recherche générale sur les systèmes dancrage des FPSO a été réalisée en considérant divers problèmes : efforts hydrodynamiques du second ordre, réponses dynamiques aléatoires des systèmes dancrage des FPSO, analyses du dommage de fatigue aléatoire et estimation de la durée de vie des lignes dancrage. Plus spécialement, une étude plus approfondie avec un nouveau concept a été proposée pour estimer la fiabilité totale dun système de lignes d'ancrage des FSPO. La fiabilité totale a été déterminée selon les conditions de mer extrêmes (ULS), elle diminue avec le temps à cause de la prise en compte de l'accumulation du dommage en fatigue des lignes d'ancrage (FLS). Dans la dernière part de thèse, cette méthode a été appliquée aux conditions de mer sévères du Vietnam, surtout dans les états limites extrêmes, prenant en compte l'accumulation du dommage en fatigue. En application numérique, deux FSOs existants au Vietnam ont été analysés. Le contenu principal des études de la thèse a également contribué à réaliser un Projet National de Recherche du Vietnam (intitulé code KC.09.15/06-10), dont lun des membres est lauteur de cette thèse./ ABSTRACT From analyzing incidents of the CALM Yoke FSOs of Vietsovpetro in the White Tiger and Dragon fields, we can identify the need to develop offshore structures (including FPSO) installed and operated in safety in most severe Vietnamese sea states, with many and frequent strong winds and tropical typhoons. In this thesis, a general research on the FPSO mooring systems has been carried out by considering various problems: second order hydrodynamic efforts, random dynamic responses of the FPSO mooring systems, analyzing random damage of fatigue and estimating the durability of the mooring lines. In particular, a thorough study with a new concept was proposed to estimate the total reliability of FSPO mooring line systems. The total reliability was estimated for extreme sea conditions (ULS), which decreases with the time due to the accumulation of the damage by fatigue of the moorings lines (FLS). In the last part of thesis, this method was applied to the severe sea conditions of Vietnam, especially considering the ultimate limit states and taking into account the accumulation of the fatigue damage. For numerical application, two FSOs existing now in Vietnam were analyzed. The main studies in this thesis have also contributed to develop a National Research Project in Vietnam (entitled code KC.09.15/06-10), in which the author acts as a research team member.

Les réseaux euclidiens sont un outil particulièrement puissant dans<br />plusieurs domaines de l'algorithmique, en cryptographie et en théorie<br />algorithmique des nombres par exemple. L'objet du présent mémoire est dual : nous améliorons les algorithmes de réduction des réseaux,<br />et nous développons une nouvelle application dans le domaine<br />de l'arithmétique des ordinateurs. En ce qui concerne l'aspect algorithmique, nous nous intéressons aux cas des petites dimensions (en dimension un, où il s'agit du calcul de pgcd, et aussi en dimensions 2 à 4), ainsi qu'à la description d'une nouvelle variante de l'algorithme LLL, en dimension quelconque. Du point de vue de l'application, nous utilisons la méthode<br />de Coppersmith permettant de trouver les petites racines de polynômes modulaires multivariés, pour calculer les pires cas pour l'arrondi des fonctions mathématiques, quand la fonction, le mode d'arrondi, et la précision sont donnés. Nous adaptons aussi notre technique aux mauvais cas simultanés pour deux fonctions. Ces deux méthodes sont des pré-calculs coûteux, qui une fois <br />effectués permettent d'accélérer les implantations des fonctions mathématiques élémentaires en précision fixée, par exemple en double précision.<br /><br />La plupart des algorithmes décrits dans ce mémoire ont été validés<br />expérimentalement par des implantations, qui sont<br />disponibles à l'url http://www.loria.fr/~stehle.

L'arithmétique par intervalles permet de calculer et simultanément vérifier des résultats. Cependant, une application naïve de cette arithmétique conduit à un encadrement grossier des résultats. De plus, de tels calculs peuvent être lents.Nous proposons des algorithmes précis et des implémentations efficaces, utilisant l'arithmétique par intervalles, dans le domaine de l'algèbre linéaire. Deux problèmes sont abordés : la multiplication de matrices à coefficients intervalles et la résolution vérifiée de systèmes linéaires. Pour le premier problème, nous proposons deux algorithmes qui offrent de bons compromis entre vitesse et précision. Pour le second problème, nos principales contributions sont d'une part une technique de relaxation, qui réduit substantiellement le temps d'exécution de l'algorithme, et d'autre part l'utilisation d'une précision étendue en quelques portions bien choisies de l'algorithme, afin d'obtenir rapidement une grande précision. / Interval arithmetic is a means to compute verified results. However, a naive use of interval arithmetic does not provide accurate enclosures of the exact results. Moreover, interval arithmetic computations can be time-consuming. We propose several accurate algorithms and efficient implementations in verified linear algebra using interval arithmetic. Two fundamental problems are addressed, namely the multiplication of interval matrices and the verification of a floating-point solution of a linear system. For the first problem, we propose two algorithms which offer new tradeoffs between speed and accuracy. For the second problem, which is the verification of the solution of a linear system, our main contributions are twofold. First, we introduce a relaxation technique, which reduces drastically the execution time of the algorithm. Second, we propose to use extended precision for few, well-chosen parts of the computations, to gain accuracy without losing much in term of execution time.

L'objet est de comparer des algorithmes de multiplication de matrices à coefficients intervalles et leurs implémentations.Le premier axe est la mesure de la précision numérique. Les précédentes analyses d'erreur se limitent à établir une borne sur la surestimation du rayon du résultat en négligeant les erreurs dues au calcul en virgule flottante. Après examen des différentes possibilités pour quantifier l'erreur d'approximation entre deux intervalles, l'erreur d'arrondi est intégrée dans l'erreur globale. À partir de jeux de données aléatoires, la dispersion expérimentale de l'erreur globale permet d'éclairer l'importance des différentes erreurs (de méthode et d'arrondi) en fonction de plusieurs facteurs : valeur et homogénéité des précisions relatives des entrées, dimensions des matrices, précision de travail. Cette démarche conduit à un nouvel algorithme moins coûteux et tout aussi précis dans certains cas déterminés.Le deuxième axe est d'exploiter le parallélisme des opérations. Les implémentations précédentes se ramènent à des produits de matrices de nombres flottants. Pour contourner les limitations d'une telle approche sur la validité du résultat et sur la capacité à monter en charge, je propose une implémentation par blocs réalisée avec des threads OpenMP qui exécutent des noyaux de calcul utilisant les instructions vectorielles. L'analyse des temps d'exécution sur une machine de 4 octo-coeurs montre que les coûts de calcul sont du même ordre de grandeur sur des matrices intervalles et numériques de même dimension et que l'implémentation par bloc passe mieux à l'échelle que l'implémentation avec plusieurs appels aux routines BLAS. / This work aims at determining suitable scopes for several algorithms of interval matrices multiplication.First, we quantify the numerical quality. Former error analyses of interval matrix products establish bounds on the radius overestimation by neglecting the roundoff error. We discuss here several possible measures for interval approximations. We then bound the roundoff error and compare experimentally this bound with the global error distribution on several random data sets. This approach enlightens the relative importance of the roundoff and arithmetic errors depending on the value and homogeneity of relative accuracies of inputs, on the matrix dimension, and on the working precision. This also leads to a new algorithm that is cheaper yet as accurate as previous ones under well-identified conditions.Second, we exploit the parallelism of linear algebra. Previous implementations use calls to BLAS routines on numerical matrices. We show that this may lead to wrong interval results and also restrict the scalability of the performance when the core count increases. To overcome these problems, we implement a blocking version with OpenMP threads executing block kernels with vector instructions. The timings on a 4-octo-core machine show that this implementation is more scalable than the BLAS one and that the cost of numerical and interval matrix products are comparable.

L'objectif de ce travail de thèse est de développer une bibliothèque de modules IPs (Intellectual Properties) de simulateurs temps réel embarqués qui simulent différents éléments d'un système électrique. Ces modules ont été conçus pour être utiliser non seulement pour une validation HIL (Hardware-In-the-Loop) des commandes numériques mais aussi pour des applications de commande embarquées, où le module IP de simulateur et le contrôleur sont tous les deux implémentés et exécutés dans la même cible FPGA. Cette nouvelle classe de simulateurs temps réel devrait être de plus en plus incluse dans la prochaine génération de contrôleurs numériques. En effet, ces modules IPs de simulateurs temps réel embarqués peuvent être avantageusement intégrés dans les contrôleurs numériques pour assurer des fonctions comme l'observation, l'estimation, le diagnostic où la surveillance de la santé. Inversement aux cas de HIL, le principal défi lors de la conception de tels simulateurs est de faire face à leur complexité ayant à l'esprit que, dans le cas des systèmes embarqués, les ressources matérielles disponibles sont limitées en raison du coût. En outre, ce problème est renforcé par la nécessité des pas de simulation très petit. Ceci est généralement le cas lors de la simulation des convertisseurs de puissance.Pour développer ces modules IPs, des lignes directrices dédiés de conception ont été proposées pour être suivies pour gérer la complexité de ces simulateurs (solveur de modèle, solveur numérique, pas de simulation, conditionnement de données) tout en tenant compte des contraintes temporelles et matérielles/coût (temps de calcul limité, ressources matérielles limitées ...).Les modules IPs de simulateurs à développer ont été organisés en deux catégories principales: ceux qui sont consacrées aux éléments électromagnétiques d'un système électrique, et ceux dédiés à ses éléments commutés.La première catégorie regroupe les éléments où les phénomènes électriques, magnétiques sont modélisés en plus de phénomènes mécaniques (pour les parties mécaniques) et des phénomènes potentiellement thermiques. Trois cas sont traités: le simulateur temps réel embarqué d'une machine synchrone triphasée, celui d'une machine asynchrone triphasée et celui d'un alternateur synchrone à trois étages. En plus de cela, les avantages de l'utilisation de la transformation delta pour améliorer la stabilité du solveur numérique lorsque un petit pas de calcul et le codage virgule fixe (avec une précision de données limitée) sont utilisés, ont été étudiés.La deuxième catégorie concerne des éléments commutés tels que les convertisseurs de puissance où les événements de commutation sont considérés. Là encore, plusieurs topologies de convertisseurs ont été étudiées: un redresseur simple alternance, un hacheur série, un hacheur réversible en courant, un hacheur quatre quadrant, un onduleur monophasé, un onduleur triphasé, un redresseur à diodes triphasé et un redresseur MLI triphasé. Pour tous ces modules IPs de simulateurs, l'approche de modélisation ADC (Associated Discrete Circuit) est adoptée.Le module IP de simulateur temps réel embarqué du redresseur MLI a été appliqué dans un contexte d'une application embarquée. Cette dernière consiste en une commande tolérante aux défauts d'un convertisseur de tension coté réseau. Ainsi, ce module IP est associé à celui d'un simulateur temps réel d'un filtre RL triphasé et les deux sont embarqués dans le dispositif de commande du redresseur pour estimer les courants de lignes. Ces courants sont injectés dans le dispositif de commande dans le cas d'un défaut de capteur de courant. La capacité de cet estimateur de garantir la continuité de service en cas de défauts est validée par des tests HIL et expérimentalement. / The aim of this thesis work is to develop an IP-Library of FPGA-based embedded real-time simulator IPs (Intellectual Properties) that simulate different elements of an electrical system. These IPs have been designed to be used not only for Hardware-In-the-Loop (HIL) testing of digital controllers but also for low cost embedded control applications, where the simulator IP and the controller are both implemented and run altogether in the same FPGA device. This emerging class of real-time simulators is expected to be more and more included in the next generation of digital controllers. Indeed, such embedded real-time simulator IPs can be advantageously embedded within digital controllers to ensure functions like observation, estimation, diagnostic or health-monitoring. Conversely to the HIL case, the main challenge when designing such simulator IPs is to cope with their complexity having in mind that, in the case of embedded systems, the available hardware resources are limited due to the cost. Furthermore, this challenge is strengthened by the need of very short simulation time-steps which is typically the case when simulating power converters.To develop these IPs, dedicated design guidelines have been proposed to be followed to manage the complexity of these simulator IPs (model solver, numerical solver, time-step, data conditioning) with regards to the timing and the area/cost constraints (computation time limit, limited hardware resources …).The simulators IPs to be developed have been organized into two main categories: those dedicated to electromagnetic elements of an electrical system and those dedicated to their switching elements.The first category gathers elements where electric, magnetic phenomena are modelized in addition to mechanical phenomena (for moving systems) and potentially thermal phenomena. Three cases are dealt with: the embedded real-time simulator of a three-phase synchronous machine, the one of a three-phase induction machine and the one of a brushless synchronous generator. Also, the advantages of using delta transformation to improve the stability of the numerical solver when short simulation time-step and fixed-point (with limited data precision) are used, have been studied.The second category concerns switching elements such as power converters where switching events are considered. Here again, several converter topologies have been studied: a half-wave rectifier, a buck DC-DC converter, a bidirectional buck DC-DC converter, a H-bridge DC-DC converter, a single-phase H-bridge DC-AC converter, a three-phase voltage source inverter, a three-phase diode rectifier and a three-phase PWM rectifier. For all these IPs, the Associated Discrete Circuit (ADC) modeling approach is adopted.The embedded real-time simulator IP of the three-phase PWM rectifier has been applied in the context of an embedded application. The latter consists of a fault-tolerant control of a grid-connected voltage source rectifier. Thus, this simulator IP is associated with the one of a three-phase RL-filter and are both implemented within the rectifier controller to estimate the grid currents. These currents are injected in the controller in the case of a current sensor fault. The ability of this estimator to guarantee the service continuity in the case of faults is validated through HIL tests and experiments.

L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le "dilemme du fabricant de tables" (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'"approximation polynomiale rigoureuse", permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre "vérifieur ISValP" est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en "précision augmentée" pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de "double-arrondi", qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis.

Quand on veut évaluer ou manipuler une fonction mathématique f, il est fréquent de la remplacer par une approximation polynomiale p. On le fait, par exemple, pour implanter des fonctions élémentaires en machine, pour la quadrature ou la résolution d'équations différentielles ordinaires (ODE). De nombreuses méthodes numériques existent pour l'ensemble de ces questions et nous nous proposons de les aborder dans le cadre du calcul rigoureux, au sein duquel on exige des garanties sur la précision des résultats, tant pour l'erreur de méthode que l'erreur d'arrondi.Une approximation polynomiale rigoureuse (RPA) pour une fonction f définie sur un intervalle [a,b], est un couple (P, Delta) formé par un polynôme P et un intervalle Delta, tel que f(x)-P(x) appartienne à Delta pour tout x dans [a,b].Dans ce travail, nous analysons et introduisons plusieurs procédés de calcul de RPAs dans le cas de fonctions univariées. Nous analysons et raffinons une approche existante à base de développements de Taylor.Puis nous les remplaçons par des approximants plus fins, tels que les polynômes minimax, les séries tronquées de Chebyshev ou les interpolants de Chebyshev.Nous présentons aussi plusieurs applications: une relative à l'implantation de fonctions standard dans une bibliothèque mathématique (libm), une portant sur le calcul de développements tronqués en séries de Chebyshev de solutions d'ODE linéaires à coefficients polynômiaux et, enfin, un processus automatique d'évaluation de fonction à précision garantie sur une puce reconfigurable.