Ce travail porte sur l’étude expérimentale et numérique de l’écoulement des mousses humides dans un canal horizontal droit de section carrée avec ou sans singularités. Il est consacré tout particulièrement à déterminer les paramètres pertinents de l’écoulement dont la chute de pression longitudinale, les champs de vitesse de l’écoulement de mousse en proche parois, les épaisseurs de films liquides minces et épais en paroi et l’évolution de la contrainte pariétale pour une mousse humide dont la fraction gazeuse varie de 55 à 85% et la vitesse débitante de la mousse est 2, 4 puis 6 cm/s. Une fois ces paramètres déterminés en conduite horizontale droite, nous avons ensuite effectué des mesures sur différentes géométries représentant un élargissement brusque, une chicane verticale et écoulement de mousse autour d’un cylindre, dont le but est d’étudier la réorganisation de l’écoulement en vue de déterminer le comportement rhéologique des mousses en écoulement à l’aval et à l’amont des singularités. Finalement, une étude de simulation numérique (CFD) en utilisant les lois de comportement de type Bingham, pour fluides non newtoniens, a été effectuée afin de tester sa capacité de représenter des écoulements type mousse humide dans une conduite horizontale avec ou sans singularités. Nous avons vérifié tout d’abord l’évolution longitudinale de la pression statique qui est linéaire à l’amont comme à l’aval loin des zones influencées par les singularités. La chute de pression singulière reste à peu près constante pour une vitesse débitante donnée de la mousse. À partir de la technique de Vélocimétrie par Image de Particule (PIV), nous avons déterminé les composantes de vitesse au voisinage immédiat des singularités. Ces mesures nous ont permis de mettre en évidence l’existence de différents régimes d’écoulement, et de déterminer la réorganisation et le comportement rhéologique de l’écoulement de mousse autour des géométries étudiées. L’analyse des mesures d’épaisseur de films liquides, obtenues par la méthode conductimétrique, indique que la paroi reste mouillée par un film liquide suffisamment épais pour qu’on puisse appliquer la méthode électrochimique. Les signaux polarographiques obtenus avec la mousse présentent alors de fortes fluctuations. La comparaison de celles-ci avec les contraintes pariétales déduites à partir des mesures de la chute de pression montre bien une bonne concordance. L’étude numérique (CFD), effectuée pour une fraction volumique de gaz égale à 70% et qui s’écoule avec une vitesse débitante de 2 cm/s, montre que le modèle rhéologique de Bingham pourrait être bien adapté à ce genre de mousse humide évoluant en écoulement en bloc. / This work is an experimental and numerical study of aqueous foam flow inside a horizontal square duct, with and without flow disruption devices (fdd). It is especially devoted to determine the pertinent parameters of the flow: longitudinal pressure losses, velocity fields of foam flow near the walls, liquid film thickness (thick and thin), and the wall shear stress evolution, for an aqueous foam with a void fraction range between 55 and 85%, for a mean foam flow velocity of 2, 4 and 6 cm/s. Once they were determined, inside the horizontal channel, we carried out measurements over different geometries: half-sudden expansion, vertical fence and foam flow around a cylinder. The goal was to study the foam flow reorganization to well understand the rheological behavior of aqueous foam flow in the vicinities of different fdd. Finally, a numerical simulation (CFD), using the Bingham behavior model of non-Newtonian fluid, was undertaken to test its capacity to represent the aqueous foam flow inside the horizontal duct with flow disruption devices. First of all, we verified the static longitudinal pressure evolution, which varies linearly upstream and downstream far from the fdd. The singular pressure loss remains constant for a given mean foam velocity and a foam quality (void fraction). From the Particle Imaging Velocimetry (PIV) technique (2D), we determined the two velocity components in the immediate vicinities of the disruption devices. They allowed us to put into evidence the different foam flow regimes and to observe the foam flow reorganization and rheological behavior through the studied fdd. The slip-layer thickness analysis, obtained using the conductimetry method, shows that the wall presents a liquid film thick enough to apply an electrochemical technique (polarography). Thus, the polarographic signals, obtained for the foam flow, present important fluctuations. They were compared to the wall shear stress deducted from the measurement of pressure losses, showing a good similarity between them. The numerical study (CFD), carried out for aqueous foam flow with a void fraction of 70% and a mean foam flow velocity of 2 cm/s, shows that the Bingham rheological model can be adapted to this kind of aqueous foam flow which is flowing like a block.

De plus en plus de constructeurs proposent des accélérateurs de calculs à base de circuits reconfigurables FPGA, cette technologie présentant bien plus de souplesse que le microprocesseur. Valoriser cette flexibilité dans le domaine de l'accélération de calcul flottant en utilisant les langages de description de circuits classiques (VHDL ou Verilog) reste toutefois très difficile, voire impossible parfois. Cette thèse a contribué au développement du logiciel FloPoCo, qui offre aux utilisateurs familiers avec VHDL un cadre C++ de description d'opérateurs arithmétiques génériques adapté au calcul reconfigurable. Ce cadre distingue explicitement la fonctionnalité combinatoire d'un opérateur, et la problématique de son pipeline pour une précision, une fréquence et un FPGA cible donnés. Afin de pouvoir utiliser FloPoCo pour concevoir des opérateurs haute performance en virgule flottante, il a fallu d'abord concevoir des blocs de bases optimisés. Nous avons d'abord développé des additionneurs pipelinés autour des lignes de propagation de retenue rapides, puis, à l'aide de techniques de pavages, nous avons conçu de gros multiplieurs, possiblement tronqués, utilisant des petits multiplieurs. L'évaluation de fonctions élémentaires en flottant implique souvent l'évaluation en virgule fixe d'une fonction. Nous présentons un opérateur générique de FloPoCo qui prend en entrée l'expression de la fonction à évaluer, avec ses précisions d'entrée et de sortie, et construit un évaluateur polynomial optimisé de cette fonction. Ce bloc de base a permis de développer des opérateurs en virgule flottante pour la racine carrée et l'exponentielle qui améliorent considérablement l'état de l'art. Nous avons aussi travaillé sur des techniques de compilation avancée pour adapter l'exécution d'un code C aux pipelines flexibles de nos opérateurs. FloPoCo a pu ainsi être utilisé pour implanter sur FPGA des applications complètes.

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. / The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the ``Table Maker's Dilemma'' (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of ``Rigorous Polynomial Approximation'', allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel's lemma that we have formalized for both univariate and bivariate cases. In particular, our ``ISValP verifier'' is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of ``augmented-precision'' FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x²+y²) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the ``double-rounding'' phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.

De plus en plus de constructeurs proposent des accélérateurs de calculs à base de circuits reconfigurables FPGA, cette technologie présentant bien plus de souplesse que le microprocesseur. Valoriser cette flexibilité dans le domaine de l'accélération de calcul flottant en utilisant les langages de description de circuits classiques (VHDL ou Verilog) reste toutefois très difficile, voire impossible parfois. Cette thèse a contribué au développement du logiciel FloPoCo, qui offre aux utilisateurs familiers avec VHDL un cadre C++ de description d'opérateurs arithmétiques génériques adapté au calcul reconfigurable. Ce cadre distingue explicitement la fonctionnalité combinatoire d'un opérateur, et la problématique de son pipeline pour une précision, une fréquence et un FPGA cible donnés. Afin de pouvoir utiliser FloPoCo pour concevoir des opérateurs haute performance en virgule flottante, il a fallu d'abord concevoir des blocs de bases optimisés. Nous avons d'abord développé des additionneurs pipelinés autour des lignes de propagation de retenue rapides, puis, à l'aide de techniques de pavages, nous avons conçu de gros multiplieurs, possiblement tronqués, utilisant des petits multiplieurs. L'évaluation de fonctions élémentaires en flottant implique souvent l'évaluation en virgule fixe d'une fonction. Nous présentons un opérateur générique de FloPoCo qui prend en entrée l'expression de la fonction à évaluer, avec ses précisions d'entrée et de sortie, et construit un évaluateur polynomial optimisé de cette fonction. Ce bloc de base a permis de développer des opérateurs en virgule flottante pour la racine carrée et l'exponentielle qui améliorent considérablement l'état de l'art. Nous avons aussi travaillé sur des techniques de compilation avancée pour adapter l'exécution d'un code C aux pipelines flexibles de nos opérateurs. FloPoCo a pu ainsi être utilisé pour implanter sur FPGA des applications complètes. / Due to their potential performance and unmatched flexibility, FPGA-based accelerators are part of more and more high-performance computing systems. However, exploiting this flexibility for accelerating floating-point computations by manually using classical circuit description languages (VHDL or Verilog) is very difficult, and sometimes impossible. This thesis has contributed to the development of the FloPoCo software, a C++ framework for describing flexible FPGA-specific arithmetic operators. This framework explicitly separates the description of the combinatorial functionality of an arithmetic operator, and its pipelining for a given precision, operating frequency and target FPGA.In order to be able to use FloPoCo for designing high performance floating-point operators, we first had to design the optimized basic blocks. We first developed pipelined addition architectures exploiting the fast-carry lines present in modern FPGAs. Next, we focused on multiplication architectures. Using tiling techniques, we proposed novel architectures for large multipliers, but also truncated multipliers, based on the multipliers found in modern FPGA DSP blocks. We also present a generic FloPoCo operator which inputs the expression of a function, its input and output precisions, and builds an optimized polynomial evaluator for the fixed-point evaluation of this function. Using this building block we have designed floating-point operators for the square-root and exponential functions which significantly outperform existing operators. Finally, we also made use of advanced compilation techniques for adapting the execution of a C program to the flexible pipelines of our operators.