Formal Methods for Functional Verification of Cache-Coherent System-on-Chip

Abderahman Kriouile 1, 2
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Résumé : Les architectures des systèmes sur puce (System-on-Chip, SoC) actuelles intègrent de nombreux composants différents tels que les processeurs, les accélérateurs, les mémoires et les blocs d'entrée/sortie, certains pouvant contenir des caches. Vu que l'effort de validation basée sur la simulation, actuellement utilisée dans l'industrie, croît de façon exponentielle avec la complexité des SoCs, nous nous intéressons à des techniques de vérification formelle. Nous utilisons la boîte à outils CADP pour développer et valider un modèle formel d'un SoC générique conforme à la spécification AMBA 4 ACE récemment proposée par ARM dans le but de mettre en œuvre la cohérence de cache au niveau système. Nous utilisons une spécification orientée contraintes pour modéliser les exigences générales de cette spécification. Les propriétés du système sont vérifié à la fois sur le modèle avec contraintes et le modèle sans contraintes pour détecter les cas intéressants pour la cohérence de cache. La paramétrisation du modèle proposé a permis de produire l'ensemble complet des contre-exemples qui ne satisfont pas une certaine propriété dans le modèle non contraint. Notre approche améliore les techniques industrielles de vérification basées sur la simulation en deux aspects. D'une part, nous suggérons l'utilisation du modèle formel pour évaluer la bonne construction d'une unité de vérification d'interface. D'autre part, dans l'objectif de générer des cas de test semi-dirigés intelligents à partir des propriétés de logique temporelle, nous proposons une approche en deux étapes. La première étape consiste à générer des cas de tests abstraits au niveau système en utilisant des outils de test basé sur modèle de la boîte à outils CADP. La seconde étape consiste à affiner ces tests en cas de tests concrets au niveau de l'interface qui peuvent être exécutés en RTL grâce aux services d'un outil commercial de génération de tests dirigés par les mesures de couverture. Nous avons constaté que notre approche participe dans la transition entre la vérification du niveau interface, classiquement pratiquée dans l'industrie du matériel, et la vérification au niveau système. Notre approche facilite aussi la validation des propriétés globales du système, et permet une détection précoce des bugs, tant dans le SoC que dans les bancs de test commerciales.
Type de document :
Thèse
Logic in Computer Science [cs.LO]. Université Grenoble Alpes, 2015. English
Liste complète des métadonnées

Littérature citée [122 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01258784
Contributeur : Abderahman Kriouile <>
Soumis le : lundi 25 janvier 2016 - 22:44:46
Dernière modification le : lundi 29 janvier 2018 - 11:59:49
Document(s) archivé(s) le : vendredi 11 novembre 2016 - 16:51:50

Identifiants

  • HAL Id : tel-01258784, version 2

Collections

Citation

Abderahman Kriouile. Formal Methods for Functional Verification of Cache-Coherent System-on-Chip. Logic in Computer Science [cs.LO]. Université Grenoble Alpes, 2015. English. 〈tel-01258784v2〉

Partager

Métriques

Consultations de la notice

393

Téléchargements de fichiers

226