Publications

Thèses


< retour aux thèses

« Réflexions autour de la méthodologie de vérification des circuits multi-horloges : analyse qualitative et automatisation ».

Auteur : M. Kebaili
Directeur de thèse : K. Morin-Allory
Co-directeur de thèse : J.C. Brignone
Président du jury : B. Rouzeyre
Rapporteur(s) de thèse : E. Encrenaz-Tiphene, S. Pillement,
Examinateur(s) de thèse : R. Leveugle,
These de Doctorat Université Grenoble Alpes
Spécialité : Microélectronique
Soutenance : 25/10/2017
ISBN : 978-2-11-129230-7

Résumé

Depuis plusieurs années, le marché des circuits intégrés numériques requiert des systèmes de plus en plus complexes dans un temps toujours plus réduit. Afin de répondre à ses deux exigences, les industriels de la conception font appel à des fournisseurs externes proposant des circuits fonctionnant sur des signaux d'horloge dédiés. Lorsque ces derniers communiquent entre eux, les horloges d'emission et de réception ne sont pas les mêmes, on parle de « Clock Domain Crossing » (CDC). Les CDC correspondent à des communications asynchrones et peuvent provoquer des dysfonctionnements critiques. Par ailleurs, ces problèmes étant intermittents et complexes à analyser, ils ne peuvent pas être exhaustivement vérifiés avec des méthodes telles que l’analyse de timing ou la simulation fonctionnelle. Avec l'augmentation du nombre de CDC dans les circuits, les industriels de la conception assistée par ordinateur (EDA) ont proposé des solutions logicielles spécialisées dans la vérification statique des CDC. Cependant, les circuits développés étant en constante évolution, les outils ne sont pas en mesure de s’adapter. Pour pallier ces problèmes, la vérification industrielle des CDC est basée sur la spécification de contraintes et d'exclusions par l'utilisateur. Ces actions, qui se substituent aux outils, peuvent masquer des bugs. De plus, l’effort humain requis par cette approche n’est pas compatible avec le temps alloué au développement de circuits industriels. Nous avons donc cherché à automatiser la vérification en proposant des solutions basées sur des propriétés formelles. Les travaux ont consisté à analyser les différentes techniques de conception et de vérification des CDC à travers l’évaluation des principaux outils du marché. A partir des résultats obtenus, nous avons formalisé les problèmes pratiques et proposé des modèles permettant d’obtenir des résultats exhaustifs automatiquement. Les essais ont été réalisés sur un sous-système à base de processeurs (CPUSS) développé chez STMicroelectronics. L'adoption de nos modèles permet une vérification complète des CPUSS de manière automatique ce qui est essentiel dans un environnement industriel compétitif. En effet, le nombre d’informations devant être spécifiées par l’utilisateur a été réduit de moitié pour chacun des outils évalués. Par ailleurs, ces travaux ont montré que l’axe de développement des outils CDC avec l’ajout de fonctionnalités telles que les flots hiérarchiques ou l’injection de fautes n’améliore pas la qualité de résultats. Une collaboration ayant été mise en place avec les principaux fournisseurs outils, certaines solutions seront probablement intégrées aux outils dans les années à venir.

pdf pdf