Réflexions autour de la méthodologie de vérification des circuits multi-horloges : analyse qualitative et automatisation ; Reflections on the methodology for verifying multi-clock design : qualitative analysis and automation

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'émission 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 ...