Transparents

Thème 3
Conception et vérification
d’architectures de systèmes
sur puce
Conception et simulation
Frédéric Pétrot
Vérification
Laurence Pierre
Conception et vérification
d’architectures de systèmes sur puce
Frédéric Pétrot
Laurence Pierre
•  Permanents : Dominique Borrione, Nicolas Fournel,
Stéphane Mancini, Katell Morin-Allory, Olivier Muller,
Frédéric Rousseau, Hamed Sheibanyrad
•  Etudiants en thèse : 13
•  Post-doctorants : 3
•  Ingénieurs : 4
Journée scientifique TIMA - 14/2/2014
2
Thème "Conception et vérification
d'architectures de systèmes sur puce"
Axe Conception
(System Level Synthesis)
Frédéric PETROT
http://tima.imag.fr/sls/
Thématiques Equipe SLS
•  Architecture
– 
– 
– 
– 
Multi-many cores
Réseaux sur puce
Hiérarchie mémoire
Reconfigurable
•  CAO
–  Simulation de systèmes numériques
–  Synthèse d’architecture
–  Synthèse de systèmes
•  Logiciel
–  Noyau de système d’exploitation
Journée scientifique TIMA - 14/2/2014
4
Thématiques Equipe SLS
•  Architecture
– 
– 
– 
– 
Multi-many cores
Réseaux sur puce
Hiérarchie mémoire
Reconfigurable
•  CAO
–  Simulation de systèmes numériques
–  Synthèse d’architecture
–  Synthèse de systèmes
•  Logiciel
–  Noyau de système d’exploitation
Journée scientifique TIMA - 14/2/2014
5
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Problématique du
« Memory Wall »
Journée scientifique TIMA - 14/2/2014
Stratégies proposées
•  Stratégies complémentaires de pré-chargement:
•  En ligne → adaptation dynamique
–  Avantage : systèmes et interactions pris en compte
–  Inconvénients : décision « locale » fonction du passé
•  Hors-ligne → compilation et optimisation
–  Avantage : connaissance application, optimisation globale
–  Inconvénient : caractère dynamique non pris en compte
Construction d'une boîte à outils « conceptuelle »
pour maîtriser la problématique de la gestion des
données
Journée scientifique TIMA - 14/2/2014
Optimisation accès mémoire
•  Contexte des unités de traitement
d'image (kernel)
•  Concepteur focalisé sur applicatif,
transferts de données optimisés
automatiquement
Journée scientifique TIMA - 14/2/2014
Optimisation accès mémoire
•  Stratégie : insertion
étape d'optimisation
accès données dans flot
de synthèse de haut
niveau (HLS)
•  Principes de base
validés, outil prototype
[DATE2012]
Journée scientifique TIMA - 14/2/2014
Pré-chargement adaptatif
Journée scientifique TIMA - 14/2/2014
Cache auto-paramétrable
Journée scientifique TIMA - 14/2/2014
Résultats
Adaptation
Cache nD-AP
SPT
Plate-forme de prototypage
Mesure de performance
Journée scientifique TIMA - 14/2/2014
Bilan « Gestion des données »
•  Bilan
–  Collaborations : Telecom-Paristech, LETI/
DACLE, Persyval, LCIS, Politecnico Turino
–  Outils prototypes, plates-formes d'évaluation
•  Perspectives
–  Autres classes d'applications
–  Intégration dans système multi-processeurs
–  Démonstration sur application complète
Journée scientifique TIMA - 14/2/2014
Thématiques Equipe SLS
•  Architecture
– 
– 
– 
– 
Multi-many cores
Réseaux sur puce
Hiérarchie mémoire
Reconfigurable
•  CAO
–  Simulation de systèmes numériques
–  Synthèse d’architecture
–  Synthèse de systèmes
•  Logiciel
–  Noyau de système d’exploitation
Journée scientifique TIMA - 14/2/2014
22
La synthèse d’architecture revisitée
•  Les FPGA offrent un bon compromis consommation/
vitesse d’exécution pour la conception d’accélérateurs
matériels
–  Traitement audio & vidéo,
–  Calculs financiers
–  …
•  Mais leur utilisation suppose une bonne connaissance des
outils (même avec des outils de synthèse d’architectures)
–  Espace de conception immense
–  Intervention manuelle
 Limitée aux experts
Journée scientifique TIMA - 14/2/2014
23
La synthèse d’architecture revisitée
•  Objectif : rendre accessible au plus grand nombre la
réalisation d’accélérateurs matériels
•  Caractéristiques du flot de conception idéal pour des
utilisateurs peu experts
–  Produire des circuits rapides
… et cela rapidement
… à partir de description algorithmique peu bridée
→ incluant du flot de contrôle
–  Respecter les contraintes matérielles
→ surface et fréquence
–  Génération automatisée (≈ compilation)
Journée scientifique TIMA - 14/2/2014
24
Le flot de conception souhaité
•  Indépendant du concepteur, avec ajout de contraintes
et de statistiques d’exécution
Flot souhaité
Flot actuel
→
Journée scientifique TIMA - 14/2/2014
25
Diriger l’exploration …
•  Il existe de solutions optimales au sens de Pareto
Journée scientifique TIMA - 14/2/2014
26
Diriger l’exploration …
•  Il existe de solutions optimales au sens de Pareto
–  Idem avec des contraintes
Journée scientifique TIMA - 14/2/2014
27
Diriger l’exploration …
•  Il existe de solutions optimales au sens de Pareto
–  Idem avec des contraintes
–  Mais il existe un ensemble de solutions satisfaisantes
Journée scientifique TIMA - 14/2/2014
28
Diriger l’exploration …
•  De la solution initiale avec un maximum de partage des opérateurs
Journée scientifique TIMA - 14/2/2014
29
Diriger l’exploration …
•  De la solution initiale avec un maximum de partage des opérateurs
•  Progression itérative
–  Transformations (ajout d’opérateurs, déroulement de boucles, …)
–  Evaluation des transformations possibles (estimateurs rapides)
Journée scientifique TIMA - 14/2/2014
30
Diriger l’exploration …
•  De la solution initiale avec un maximum de partage des opérateurs
•  Progression itérative
–  Transformations (ajout d’opérateurs, déroulement de boucles, …)
–  Evaluation des transformations possibles (estimateurs rapides)
•  Vers une solution satisfaisante, respectant les contraintes
Journée scientifique TIMA - 14/2/2014
31
Propriétés de la méthode
•  Algorithme « glouton »
→ Faible complexité algorithmique
→ Convergence garantie
même sous contraintes de ressources
•  Emploi d’estimations → rapidité
•  Respect strict des contraintes de ressources
•  Possibilité d’extension à d’autres types de contraintes
Journée scientifique TIMA - 14/2/2014
32
Modifications apportées
Description d’entrée
(langage C)
Description RTL
(VHDL, …)
Journée scientifique TIMA - 14/2/2014
33
Modifications apportées
Détection des annotations
Description d’entrée
(langage C)
Calibration
Virtex 5, Virtex 7
Description RTL
(VHDL, …)
Génération du
Circuit
correspondant
Graphe hiérarchique
Annotations
Sélection de la meilleure transformation :
- Meilleur gain en latence
- Plus faible coût en ressources
Ajout d’opérateurs & ports
Remplacement RAM & ROM
Déroulement de boucles
Câblage de condition
Journée scientifique TIMA - 14/2/2014
34
Résultats
•  Outil AUGH (Autonomous UGH)
•  8 applications de test (décodeur MJPEG, IDCT 2D,
benchmark CHSTone)
•  Cible matérielle : FPGA Xilinx xc7v585t-3
Exemple de progression
pour l’IDCT 2D
•  Comparaison avec Vivado HLS
–  Vivado HLS : 59 secondes (1 synthèse – exploration manuelle)
–  Notre outil (AUGH) : 17 secondes (47 itérations)
Journée scientifique TIMA - 14/2/2014
35
Conclusion
•  Méthode et outils AUGH
– 
– 
– 
– 
Génération autonome d’accélérateurs matériels
Flot de synthèse d’architecture de faible complexité
Respect strict des contraintes de ressources
Intégration possible dans un flot et dans des outils
–  Accessible aux personnes peu expertes
–  Logiciel open source
→ http://tima.imag.fr/sls/research-projects/augh
•  Perspectives
–  Vers le « Cloud-FPGA »
Journée scientifique TIMA - 14/2/2014
36
Thématiques Equipe SLS
•  Architecture
– 
– 
– 
– 
Multi-many cores
Réseaux sur puce
Hiérarchie mémoire
Reconfigurable
•  CAO
–  Simulation de systèmes numériques
–  Synthèse d’architecture
–  Synthèse de systèmes
•  Logiciel
–  Noyau de système d’exploitation
Journée scientifique TIMA - 14/2/2014
37
Simulation native de
systèmes matériel/logiciel
•  Many-cœurs :
une tendance
et une réalité
(source
ITRS 2011)
•  Deux besoins
–  Portage/Déploiement de code sur infrastructure ad-hoc
–  Exploration de choix d’architecture
•  Deux problèmes
–  Simulation rapide grand nombre processeurs
–  Capacité estimation temporelle
Journée scientifique TIMA - 14/2/2014
38
Simulation native de
systèmes matériel/logiciel
•  Problème des espaces d’adressage
Journée scientifique TIMA - 14/2/2014
39
Simulation native de
systèmes matériel/logiciel
•  Problème des espaces d’adressage
Journée scientifique TIMA - 14/2/2014
40
Simulation native de
systèmes matériel/logiciel
•  Solution (inespérée)
Support matériel à la virtualisation
–  Exécution usuelle sauf interruptions, appels systèmes, accès
adresses mémoire spécifiés
–  Possède sa propre table de pages
–  Changement de « mode » matériel et atomique
–  Disponible chez les principaux constructeurs: x86, Power,
Sparc, Mips, ARM (Cortex A15), …
Journée scientifique TIMA - 14/2/2014
41
Simulation native de
systèmes matériel/logiciel
•  Virtualisation de l’espace
mémoire
–  Exécution usuelle sauf
interruptions, appels systèmes,
accès adresses mémoire
spécifiés
–  Possède sa propre table de pages
–  Changement de « mode »
matériel et atomique
–  Disponible chez les principaux
constructeurs: x86, Power, Sparc,
Mips, ARM (Cortex A15), …
Journée scientifique TIMA - 14/2/2014
42
Simulation native de
systèmes matériel/logiciel
•  Virtualisation de l’espace
mémoire
–  Traduction connue statiquement
–  Logiciel et modèles SystemC
utilisent espace d’adressage cible
–  Accès mémoire par logiciel traduits
par HW
–  Adresses « en dur » possibles:
(uint8_t *)0xA0001000 =
0xFF
–  Implanté en KVM
–  Totalité de l’espace d’adressage
disponible
–  Accès à coût zéro
Journée scientifique TIMA - 14/2/2014
43
Simulation native de
systèmes matériel/logiciel
•  Résultats expérimentaux
Journée scientifique TIMA - 14/2/2014
44
Conclusion
•  Simulation native HAV
– 
– 
– 
– 
– 
Manière de procéder totalement nouvelle
Démontrée sur des exemples simples
Peut être cible de la traduction binaire statique
En train d’être étendu au multiprocesseur massif
Intégration possible dans un flot et dans des outils
•  Perspectives
–  Amélioration des modèles temporels
–  Introduction de modèles d’énergie, de température, …
–  Industrialisation
Journée scientifique TIMA - 14/2/2014
45
Conclusion SLS
•  Recherche autour de problèmes concrets
–  Reconnaissance du monde académique
–  Stratégie de distribution Open Source
–  Vers l’industrialisation :
– Création de 2 startups en cours
– 2 brevets autour des NoCs
– Partenariats industriels
Journée scientifique TIMA - 14/2/2014
46
Thème "Conception et vérification
d'architectures de systèmes sur puce"
Axe Vérification
(Verification and modeling of Digital Systems)
Laurence PIERRE
http://tima.imag.fr/vds/
Vérification
•  Vérification formelle (ou semi-formelle)
–  Répondre à la question: le système
respecte-t-il le comportement attendu ?
Spécification
satisfaite ?
Système
Exigences / Spécification
Journée scientifique TIMA - 14/2/2014
48
Vérification
Circuit
•  Vérification
formelle
:
description
–  Spécification formelle
+
Simulator
Simulation results
(+ property violation)
• Formal
Méthodes déductives (démonstrateurs de
specification
théorèmes)
Stimuli
•  Techniques algorithmiques
(equivalence
checking, model checking)
•  Vérification semi-formelle :
–  Spécification formelle + vérification
dynamique (en cours de simulation)
Journée scientifique TIMA - 14/2/2014
49
❶
Vérification de composants
au niveau RTL
http://tima.imag.fr/vds/Horus/
Journée scientifique TIMA - 14/2/2014
50
Principe de base
PSL properties
Design under test
Design under test
Horus
PSL monitors
Verification infrastructure
Journée scientifique TIMA - 14/2/2014
51
Principe de base
PSL properties
Design under test
Design under test Synthesis
+ analysis
infrastructure
Horus
FPGA prototyping
and debug
PSL monitors
Embedded
checkers
Journée scientifique TIMA - 14/2/2014
Safety
52
Principe de base
PSL properties
Design under test
ls
ti
u
o
s
le
s
n
a
d
t
r
fe
s
n
Tra
ED (Dolphin)
L
S
t
e
H
S
A
M
S
Design under test
PSL monitors
Verification infrastructure
Journée scientifique TIMA - 14/2/2014
53
Exemple
•  Interface de réseau HDLC (Thales)
–  RxDataAvail ne peut pas être à 1 entre
deux trames
assert ALWAYS ({not EndOfFrame ; EndOfFrame} !
|-> next!(not RxDataAvail until! StartOfFrame);
Journée scientifique TIMA - 14/2/2014
54
Accélération d’assertions
PSL properties
Design under test
Design under test
EndOfFrame!
PSL monitors
Journée scientifique TIMA - 14/2/2014
55
Accélération d’assertions
PSL properties
Test generator
Design under test
Design under test
PSL monitors
Enhanced verification infrastructure
Journée scientifique TIMA - 14/2/2014
56
Accélération d’assertions
PSL properties
Design under test
Apis
Temporal constraints
for the inputs (PSL)
Journée scientifique TIMA - 14/2/2014
57
Accélération d’assertions
PSL properties
Design under test
Apis
Temporal constraints
for the inputs (PSL)
Synthorus2
Test generator
Journée scientifique TIMA - 14/2/2014
58
Accélération d’assertions
PSL properties
Design under test
Apis
Temporal constraints
for the inputs (PSL)
Synthorus2
Test generator
Design under test
Journée scientifique TIMA - 14/2/2014
59
Compilation de propriétés
•  Synthèse de circuits corrects par
construction :
–  Modèles pour des vérifications modulaires
C1
à vérifier
C2
Environnement réel
Journée scientifique TIMA - 14/2/2014
60
Compilation de propriétés
•  Synthèse de circuits corrects par
construction :
–  Modèles pour des vérifications modulaires
Golden model issu
de propriétés
(Synthorus2)
C1'
à vérifier
C2
Journée scientifique TIMA - 14/2/2014
61
Compilation de propriétés
•  Synthèse de circuits corrects par
construction :
–  Golden models (contrôle, protocoles)
•  Exemple : arbitre de bus AHB
Journée scientifique TIMA - 14/2/2014
62
❷
Vérification des
communications dans les
réseaux sur puce (NoCs)
http://www-tima.imag.fr/vds/NoCs
Journée scientifique TIMA - 14/2/2014
63
Approche
•  Vérification de bonne conception au
niveau algorithmique (NoC)
–  Modèle généraliste dans un theorem prover
(ACL2), instanciable pour chaque NoC
–  Théorèmes : "tout message arrivé a atteint la
bonne destination", "aucun message n’est perdu"
•  Vérification complémentaire au niveau
implémentation (routeur)
–  Modèles de propriétés généralistes
Journée scientifique TIMA - 14/2/2014
64
Approche
Journée scientifique TIMA - 14/2/2014
65
Niveau implémentation
•  Propriétés générales - classification
Journée scientifique TIMA - 14/2/2014
66
Mise en oeuvre
•  Applications :
–  HERMES (PUCRS, Brazil)
–  NOSTRUM (http://www.ict.kth.se/nostrum/)
•  Infrastructure
sur FPGA :
Journée scientifique TIMA - 14/2/2014
67
❸
Vérification de SoC
au niveau système
http://tima.imag.fr/vds/Isis/
Journée scientifique TIMA - 14/2/2014
68
Vérification d’assertions ESL
•  Vérification de propriétés
transactionnelles de plateformes HW/SW
Journée scientifique TIMA - 14/2/2014
69
Exemple
•  Plateforme de traitement de signal radio
(Thales)
I/O
SW
Communication
channel
Coprocessor
Journée scientifique TIMA - 14/2/2014
70
Exemple
•  Propriétés :
–  Interaction DDC/DMA : si le DDC (digital down
converter) a des données à transférer, le DMA initie
bien le transfert mémoire
–  Interaction DMA/SW : le DMA génère bien une
interruption entre 2 demandes de transferts mémoire
–  Pas de donnée perdue par le SW : il ne peut pas y
avoir deux transferts consécutifs du DMA à la même
adresse en mémoire avant une lecture du processeur
à cette adresse
–  ...
Journée scientifique TIMA - 14/2/2014
71
Revérification au niveau RTL
•  Raffinement des assertions
Journée scientifique TIMA - 14/2/2014
72
Vérifications sur le SW
•  Instrumentation de code C avec des
composants de vérification (SdF, sécurité)
PSL properties
Source code
Ex.
always (send_to_HW(addr2,0x0,0x3) !
-> eventually! interrupt=1)
Instrumented code
Software
monitors
Journée scientifique TIMA - 14/2/2014
73
Merci de votre attention…
Questions ?
Journée scientifique TIMA - 14/2/2014
74

Download Report