Analyse formelle du protocole ACE : cohérence de caches des systèmes sur puce

Abderahman Kriouile 1 Wendelin Serwe 1, *
* Corresponding author
1 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) d'aujourd'hui 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. Etant donné 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 ACE, récemment proposée par ARM dans le but de mettre en \oe uvre la cohérence de cache au niveau système.
Liste complète des métadonnées

https://hal.inria.fr/hal-00876665
Contributor : Wendelin Serwe <>
Submitted on : Friday, October 25, 2013 - 10:59:44 AM
Last modification on : Monday, October 5, 2015 - 4:58:26 PM
Document(s) archivé(s) le : Monday, January 27, 2014 - 12:56:51 PM

Identifiers

  • HAL Id : hal-00876665, version 1

Collections

Citation

Abderahman Kriouile, Wendelin Serwe. Analyse formelle du protocole ACE : cohérence de caches des systèmes sur puce. École d'été Temps-Réel 2013, Aug 2013, Toulouse, France. pp.130-133, 2013, Actes de l'École d'été Temps-Réel 2013. <hal-00876665>

Share

Metrics

Record views

246

Document downloads

536