Le prix Seymour Cray "jeunes chercheurs" 99 a été attribué à Karim Dioury et Antony Lester pour leurs travaux sur les outils et méthodes de vérification des circuits intégrés CMOS submicroniques. K. Dioury et A. Lester sont deux chercheurs du LIP6 qui ont effectué leur thèse au sein du département ASIM. Ils sont également les fondateurs de la société AVERTEC, créée en 1998 avec l'aide de la Direction des Relations Industrielles de l'université pour commercialiser ces résultats.

Les procédés de fabrication CMOS permettent aujourd'hui d'intégrer plusieurs dizaines de millions de transistors sur une seule puce. Les outils et méthodes de conception permettant de maîtriser une telle complexité constituent actuellement le principal frein à l'exploitation effective de cette capacité d'intégration. Pour ce qui concerne en particulier la phase de vérification finale avant fabrication, la complexité de ces véritables "systèmes intégrés" ne permet plus d'utiliser les méthodes de simulation, car elles ne fournissent pas une vérification exhaustive. Il faut donc recourir à des méthodes de vérification formelle, indépendantes des stimuli. A. Lester a principalement travaillé sur une méthode d'abstraction fonctionnelle permettant d' obtenir une description comportementale à partir du schéma en transistors (YAGLE). Karim Dioury a développé une méthode de vérification temporelle statique hiérachique (HITAS).

K. Dioury et A. Lester ont bénéficié de la plate-forme de développement constituée par la chaîne de CAO-VLSI Alliance, qui leur a fourni un environnement d'expérimentation "en grandeur réelle". Ils ont également hérité de l'expertise accumulée dans le laboratoire, puisque les premières recherches sur l'abstraction fonctionnelle et la vérification temporelle ont démarré en 1990 sous la direction de Alain Greiner, aboutissant aux thèses de Amjad Hajjar et Marc Laurentin, qui ont jeté les bases de la méthode de vérification. Arrivant sur un terrain déjà bien défriché, K.Dioury et A.Lester ont su résoudre des problèmes algorithmiques difficiles qui n'avaient pas été résolus par leurs prédécesseurs, et amener la méthode à un point où elle est réellement utilisable pour des circuits très complexes.

La coopération étroite avec BULL, dans le cadre de plusieurs projets européens a été un autre facteur de succès : Les équipes de développement de BULL utilisent depuis plusieurs années les outils prototype d'abstraction fonctionnelle et de vérification temporelle développés au LIP6, et ont contribué à orienter la recherche vers les "vrais problèmes". BULL est aujourd'hui le premier client de la société AVERTEC, et les deux outils logiciels qui mettent en œuvre les méthodes proposées par A. Lester et K. Dioury ont été utilisés avec succès par BULL pour vérifier un circuit de 18 millions de transistors.

Antony Lester a effectué sa thèse sous la direction de Pirouz Bazargan. Son principal apport réside dans l'identification formelle des éléments mémorisants au cours du processus d'abstraction fonctionnelle, et sur la possibilité de traiter des circuits mixtes contenant des parties analogiques. La soutenance est prévue fin 99.

Karim Dioury a effectué sa thèse sous la direction de Marie-Minerve Louerat. Il a proposé une méthode hiérarchique multi-niveaux pour la vérification temporelle, qui permet de prendre en compte les résistances et les capacités électriques des fils d'interconnexion. Il a soutenu sa thèse fin 98.

Cette distinction montre que, dans un domaine de recherche très appliquée, il est important de pousser la recherche jusqu'au prototypage et à l'expérimentation en grandeur réelle. Le fait que les deux lauréats soient les fondateurs de la société AVERTEC prouve également que qualité scientifique et valorisation industrielle ne sont pas contradictoires.

Prof. Alain Greiner