Ce travail de thèse présente une méthode originale pour la simulation symbolique des circuits décrits au niveau algorithmique. Tout d'abord, la description VHDL du circuit est modélisée sous le forme d'un ensemble d'équations récurrentes (SER) qui décrivent l'état du système à un instant donné en fonction des états précédents. Après une extraction automatique du SER du circuit, l'algorithme de simulation VHDL est exécuté pendant un nombre fixe de cycles déterminé par le concepteur. Pendant la simulation, un scénario de test et une simplification par règles de substitution sont appliqués pour obtenir les expressions symboliques ou numériques de chaque objet du circuit (registre, signal ou port de sortie). Trois modes de test (raisonnement, exécution et mixte) sont définis et expliqués en se basant sur la distinction entre la partie opérative et la partie contrôle de circuit. Le simulateur symbolique et le compilateur sont implémentés avec l'aide du système Mathematica. <br />Une méthodologie de vérification autour de la simulation symbolique avec SER est proposée. Plusieurs paradigmes de vérification (la correspondance de forme, la démonstration de théorèmes et SAT) sont employés sur les résultats de la simulation symbolique pour valider ou prouver les propriétés du circuit. La méthodologie est montrée sur deux circuits de taille réelle (un filtre numérique et une mémoire) et sur de nombreux cas académiques.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00009776 |
| Date | 18 July 2005 |
| Creators | Al-Sammane, G. |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0023 seconds