Contacts : Patricia Renault, Cécile Braunstein et Ramy Iskander

 

Contexte et objectif :

A partir d’une description haut niveau d’un bloc numérique, les outils automatiques de synthèse, de placement et de routage, permettent, quel que soit le procédé de fabrication visé, d’obtenir la vue physique du composant. Ces outils automatiques permettent la réutilisation d’une même description numérique dans différentes applications mais aussi pour divers procédés de fabrication.

Pour les IP analogiques, la situation est complètement différente. Il n’existe pas de méthode générique permettant de synthétiser une netlist à partir d’une description comportementale analogique. Les études existantes qui concernent la synthèse analogique, traitent toujours des problèmes particuliers comme un certain type de filtrage ou de conversion analogique-numérique.

Un des problèmes principaux de la synthèse analogique, qui n’est pas résolu jusqu’à présent, est la sélection et comparaison des architectures IP analogiques existants dans une bibliothèque d’IPs pour répondre aux spécifications souhaitées.

Au sein du LIP6, le projet CHAMS a pour but de modéliser des IP analogiques au niveau structurel (netlist de transistors). L’environnement de conception CHAMS fournit des procédures systématiques pour dimensionner la netlist d’un circuit à partir de paramètres électriques au niveau « circuit » connus (courant, régime des transistors). Cependant, la sélection d’une architecture répondant aux spécifications est actuellement à la charge du concepteur qui doit établir des comparaisons en simulant les architectures visées. Nous avons identifié une nouvelle méthode permettant de balayer un ensemble de combinaison des différents paramètres électriques afin d'obtenir les paramètres qui assurent une équivalence électrique entre différentes architectures. Cette nouvelle méthode, basée sur l’équivalence checking, déjà utilisé pour les circuits numériques, s'appuie sur l'utilisation de SMT Solver, pour représenter l'espace des solutions de manière formelle et plus compacte. Elle a été appliquée manuellement et validée sur deux exemples distincts. L’objectif de ce stage est d’automatiser la méthode proposée et de l’appliquer aux deux exemples déjà traités à la main et à trois autres exemples de circuits analogiques.

Travail à effectuer :

Le travail à effectuer consistera à :

• Etudier la méthode proposée à travers son application sur un inverseur et un amplificateur de Miller et en cascode.

• Etudier la méthode mise en œuvre dans CHAMS.

• Etudier le fonctionnement d’un SMT-solver et plus particulièrement son interfaçage avec CHAMS.

• Proposer une solution permettant d’automatiser cette méthode.

• Vérifier le bon fonctionnement de la méthode implémentée sur les deux circuits traités manuellement et sur trois nouveaux circuits analogiques.

Connaissances requises :

Ce stage mêle différents domaines : l’électronique analogique, le développement des outils de CAO ainsi que l’utilisation d’un SMT-solver.

La connaissance des langages C/C++ est nécessaire.

Encadrants

[1]. Ramy Iskander, Marie-Minerve Louërat and Andreas Kaiser, "Automatic DC Operating Point Computation and Design Plan Generation for Analog IPs", Analog Integrated Circuits and Signal Processing Journal, Vol. 56, Issue 1-2, pp. 93-105, August 2008.

[2] ITiwary, S. K.; Gupta, A.; Phillips, J. R.; Pinello, C. & Zlatanovici, R. “First steps towards SAT-based formal analog verification” ICCAD, IEEE, 2009, 1-8

[3] Cimatti, A.; Griggio, A. & Sebastiani, R. “Efficient generation of craig interpolants in satisfiability modulo theories” ACM Trans. Comput. Log., 2010, 12, 7