Loading...
Please wait, while we are loading the content...
Similar Documents
Vérification de propriétés logico-temporelles de spécifications SystemC TLM
| Content Provider | Semantic Scholar |
|---|---|
| Author | Ferro, Luca |
| Copyright Year | 2011 |
| Abstract | Au-dela de la formidable evolution en termes de complexite du circuit electronique en soi, son adoption et sa diffusion ont connu, au fil des dernieres annees, une explosion dans un tres grand nombre de domaines distincts. Un systeme sur puce peut incorporer une combinaison de composants aux fonctionnalites tres differentes. S'assurer du bon fonctionnement de chaque composant, et du systeme complet, est une tâche primordiale et epineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considerablement gagne en popularite ces dernieres annees : il s'agit d'une demarche de verification ou des proprietes logico-temporelles, exprimees dans des langages tels que PSL ou SVA, specifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution decrite dans cette these s'efforce de resoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance a partir de proprietes PSL est proposee : cette technique, inspiree d'une approche originale existante pour le niveau RTL, est ici adaptee a SystemC TLM. Une methode specifique de surveillance des actions de communication a haut niveau d'abstraction est egalement detaillee. Les possibilites offertes par la technique presentee sont significativement etendues en proposant, pour les proprietes ecrites en langage PSL, a la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un element essentiel lors des specifications a haut niveau d'abstraction. Tous ces concepts sont egalement implementes dans un outil prototype. Afin d'illustrer l'interet de la solution proposee, diverses experimentations sont effectuees avec des designs aux dimensions et complexites differentes. Les resultats obtenus permettent de souligner le fait que la methode de verification dynamique suggeree reste applicable pour des designs de taille realiste. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://tel.archives-ouvertes.fr/tel-00633069v2/document |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
