L'analyse spectrale optique permet l'étude de la composition chimique des matériaux par l'interaction entre la matière et le rayonnement. Ces dernières années, la spectrométrie dans le domaine du proche infrarouge s'est considérablement développée pour satisfaire des besoins dans les domaines comme la médecine, de la détection de gaz ou encore l'industrie des polymères. Dans cette thèse nous nous sommes intéressé à un nouveau concept de spectromètre de Fourier statique faisant intervenir une structure de guide optique planaire courbe fuyante. Un modèle électromagnétique de cette structure courbe a été développé pour dimensionner le spectromètre. Ce modèle est basé sur une méthode de décomposition dans le domaine de Fourier, associée à une transformation conforme et utilisant des couches absorbantes. Les premiers spectromètres ont été réalisés en optique intégrée sur verre et caractérisés. Des résolutions spectrales de 11 nm et 14 nm ont été mesurées. Ces résultats sont encourageants pour continuer le développement du spectromètre.

La photolithographie optique assure en partie à la microélectronique la miniaturisation des circuits électroniques. Afin de faire face à la limite de résolution de l'équipement de photolithographie, les industriels ont mis au point des techniques d'amélioration de la résolution dont certaines sont basées sur l'utilisation de la modélisation numérique. Jusqu'au nœud technologique 45 nm, cette modélisation ne prenait pas en compte la présence de plusieurs empilements de matériaux sous la résine photosensible négligeant ainsi les phénomènes de réflexion, de diffraction et d'ondes stationnaires. Pour les nœuds 32 nm et suivants, ces phénomènes rendent difficile le contrôle de la forme et des dimensions des motifs résine notamment pour les niveaux dont l'exposition s'effectue sans couche antireflet. Cette thèse CIFRE entre le laboratoire Hubert Curien de Saint- Etienne et l'industriel STMicroelectronique de Crolles traite de la caractérisation, de la modélisation et de la simulation numérique des effets d'empilement sous la résine photosensible. Le premier chapitre regroupe un ensemble de pensées sur la microélectronique, son histoire et définit les notions essentielles de ce domaine et de la modélisation numérique. Les chapitres deux et trois donnent respectivement l'état de l'art de la photolithographie optique et des techniques de correction des effets de proximité optique. Le chapitre quatre présente l'étude expérimentale, de la conception des structures test à la caractérisation des effets d'empilement en passant par le protocole de création des groupes de données. La prise en compte de ces effets est l'objet du chapitre cinq avec l'état de l'art des techniques existantes suivi de la description de l'algorithme de construction de modèles développé dans cette thèse. Enfin l'application de la méthode des sources généralisées à la photolithographie optique est évaluée dans le chapitre six / In IC manufacturing, optical photolithography is one of key actors of electronic circuit miniaturization. To work around the photolithography resolution limit, manufacturers developed resolution improvement techniques, including some based on numerical modeling. For nodes larger than 45 nm, this modeling didn't take into account several stacks under the photoresist and that caused optical reflection, diffraction, and standing wave phenomena to be neglected. For 32 nm and smaller nodes, these phenomena make it di cult to control the shape and dimensions of resist patterns, especially for layers without an anti-reflecting coating during exposure. The CIFRE thesis from Hubert Curien Laboratories in Saint-Etienne and industrial STMicroelectronics from Crolles deals with wafer stack effect characterization, modeling, and numerical simulation. The first chapter gives my philosophy and history of IC manufacturing, and defines concepts in this field and concepts about numerical modeling. Chapter Two discusses state-of-the-art optical photolithography and Chapter Three discusses state-of-the-art optical proximity correction. Chapter Four emphasizes an experimental study from test pattern conception to wafer stack effect characterization, including data set building protocol. Chapter Five covers wafer stack effect management, first describing the current status of the industry followed by a description of the model building algorithm developed during this thesis. Finally, Chapter Six assesses the generalized source method applied to the photolithography process simulation

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.

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.