Une Méthodologie De Conception Automatique De Modèles Formels Pour Des Descriptions Systemc

Résumé: La conception des systèmes embarqués par des langages de description de haut niveau rend leur vérification de plus en plus nécessaire. Le processus de vérification devient de plus en plus difficile lorsque on utilise des IPs (intellectual property) existantes pour la conception de ces systèmes. Ces IPs sont souvent hétérogènes et peuvent être de plusieurs sources, leur conception et leur intégration doivent être vérifiées. La vérification par simulation est largement utilisée, mais elle ne permet généralement pas d’obtenir une couverture exhaustive des erreurs. Il est donc important d’utiliser les techniques de la vérification formelle. Étant donné que nous visons des systèmes décrits par SYSTEMC qui ne présente pas de propriétés formelles, il est donc nécessaire de traduire ces descriptions SYSTEMC en modèles formels. Dans cet objectif, nous présentons dans cette thèse une méthodologie qui permet de générer automatiquement des modèles formels SIGNAL pour des descriptions non formels SYSTEMC. Le choix de SIGNAL est motivé par le fait qu’aujourd’hui ce langage est connecté à plusieurs outils de vérification formelle et que ses descriptions sont similaires à ceux de SYSTEMC. Le processus de génération est réalisé en deux étapes complémentaires : l’extraction structurelle et l’extraction comportementale. Enfin, nous illustrons la méthodologie proposée via le filtre FIR (Finite Impulse Response).

Publié dans la revue: