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, quelle 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 d’IP analogiques existants dans une bibliothèque des IPs. Actuellement, la sélection d’une architecture répondant aux spécifications est à la charge du concepteur qui doit établir des comparaisons en simulant les architectures visées.

Au sein du LIP6, le projet CHAMS a pour but de modéliser un IP analogique 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). Il permet d'obtenir pour une architecture donnée d'un circuit, un graphe bipartite décrivant la suite des calculs à effectuer afin de trouver l'ensemble des paramètres du circuit. Pour chaque jeu de paramètres, le concepteur doit relancer l'ensemble des calculs. Nous voulons tirer parti de la combinaison du graphe bipartite et de l'utilisation d'un SMT solver pour accélérer la construction de l'espace des solutions pour un ensemble de spécification électrique donnée. En effet, en suivant le graphe bipartite, on peut décomposer l'exploration en bloc de base, ce qui permet dans certains cas de simuler des blocs petits et génère des instances SMT plus petites et plus simples que sur le composant en entier.

Travail à effectuer :

Le travail à effectuer consistera à :

• Etudier la méthode mise en œuvre dans CHAMS et plus particulièrement le graphe bipartite.

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

• Proposer une méthode permettant au SMT-solver de commander l’évaluation de CHAMS.

• Appliquer cette méthode manuellement sur les trois circuits analogiques.

• Réaliser un prototype logiciel de la méthode proposée.

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.

Références

[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