Thesis defence of Diana Kalel (CDSI team): Advanced Structural and Semi-Formal Verification Flow for Clock Domain Crossing (CDC) in Asynchronous Multiclock Systems

Diana KALEL - CDSI team

Thesis directors / supervisors
Katell MORIN-ALLORY - Thesis director - Associate professor - Université Grenoble Alpes
Laurent FESQUET - Co-thesis director - Associate professor - Grenoble INP / Phelma, Université Grenoble Alpes
Jean-Christophe BRIGNONE - Co-thesis supervisor - Engineer - STMicroelectronics

Rapporteurs
Ayman WAHBA - Rapporteur - Full professor - Ain Shams University (Egypt)
Sébastien PILLEMENT - Rapporteur - Full professor - Ecole Polytechnique universitaire de Nantes

Composition of the jury
Laurent FESQUET - Co-thesis director - Associate professor - Grenoble INP / Phelma, Université Grenoble Alpes
Ayman WAHBA - Rapporteur - Full professor - Ain Shams University (Egypt)
Sébastien PILLEMENT - Rapporteur - Full professor - Ecole Polytechnique universitaire de Nantes
Vincent BEROULLE - Examinator - Full professor - Grenoble INP - UGA
Matthieu MOY - Examinator - Associate professor - Université Claude Bernard Lyon 1

Guests
Jean-Christophe BRIGNONE - Engineer - STMicroelectronics
Jérôme AVEZOU - Engineer - Synopsys

Title: Advanced Structural and Semi-Formal Verification Flow for Clock Domain Crossing (CDC) in Asynchronous Multiclock Systems
Keywords: CDC, Verification, formel, Clock Domain, Asynchronous, GALS
Abstract: During my PhD, we focused on improving the verification of asynchronous interfaces on multi-clock systems. Our mission was to optimize Clock Domain Crossing (CDC) verification on RTL to avoid potential bugs that may affect silicon integrity. We introduced novel aspects to elevate the quality of verification and successfully met their goals. We started by enhancing existing structural verification methods introducing the UPF-Aware CDC Verification Flow. We were also interested to integrate the dynamic functional verification with CDC static verification through the CDC SemiFormal Verification Flow. This led to the modeling of the "Universal Qualifier", a generic method to verify all types of CDC data synchronizers, and the "Hybrid Flow", a way to use assertions to accelerate the clock tree constraining for the CDC static verification. In addition, in collaboration with Accellera, our team pioneered the first IEEE standard for CDC models, which serve as concise CDC abstracted representations of blocks and sub-blocks for CDC hierarchical verification. In future work, we aim to integrate all proposed solutions into a coherent and unified flow. We also plan to address metastability injection and explore its potential in dynamic simulation and formal verification.

Titre : Développement d’un flot avancé de vérification structurelle et semi-formelle des chemins asynchrones pour les Systèmes Multi-horloges
Mots-clés : CDC, Formelle, Vérification, Domaine d'horloge, Asynchrone, GALS
Résumé : Pendant mon doctorat, nous nous sommes concentrés sur l’amélioration de la vérification des interfaces asynchrones sur les systèmes multi-horloges. Notre mission était d’optimiser la vérification de la traversée de domaine d’horloge (CDC) sur RTL pour éviter les bugs potentiels qui pourraient affecter l’intégrité du silicium. Nous avons introduit de nouveaux aspects pour élever la qualité de la vérification et avons atteint avec succès leurs objectifs. Nous avons commencé par améliorer les méthodes de vérification structurelle existantes en introduisant le flot de vérification CDC UPF-Aware. Nous avons également cherché à intégrer la vérification fonctionnelle dynamique avec la vérification statique CDC à travers le flot de vérification semiformelle CDC. Cela a conduit à la modélisation du "Qualificateur Universel", une méthode générique pour vérifier tous les types de synchroniseurs de données CDC, et du "Flot Hybride", une façon d’utiliser des assertions pour accélérer la contrainte de l’arbre d’horloge pour la vérification statique CDC. De plus, en collaboration avec Accellera, notre équipe a été pionnière dans la création de la première norme IEEE pour les modèles CDC, qui servent de représentations abstraites concises de blocs et de sous-blocs pour la vérification hiérarchique CDC. Dans les travaux futurs, nous visons à intégrer toutes les solutions proposées dans un flot cohérent et unifié. Nous prévoyons également de traiter l’injection de métastabilité et d’explorer son potentiel dans la simulation dynamique et la vérification formelle.