TP: Model Checking avec VIS¹

Version : v 1.0 2009/12/20 de C. Braunstein.

Plan

Mise en place

Code Verilog, premier pas avec VIS

Robustesse d'un multiplieur

Model Checking : convertisseur de protocole VCI-PI

Mise en place

Le model checker VIS est installé sur les postes enseignements. Pour pouvoir l'utiliser vous devez mettre à jour votre path.

Si vous êtes en bash :

export PATH=$PATH:/opt/vis-2.1/bin/

Si vous êtes en csh, tcsh... :

setenv PATH $PATH:/opt/vis-2.1/bin/

1 Code Verilog, premier pas avec VIS

L'ensemble des commandes et leur description se trouvent à l'adresse suivante : http://vlsi.colorado.edu/~vis/doc/html/commands.html.

1.1 Un simple arbitre, compilation, naviguation dans VIS

Le schéma suivant montre une architecture composée de 3 contrôleurs et un arbitre. Le fichier Verilog correspondant se trouve ici.

Description du contrôleur

• Un contrôleur demande un jeton à l'arbitre. Il a une unique sortie pass_token, il donne le jeton (pass_token = 1) si :

  1. Il a le jeton et qu'il a fini son traitement

  2. Il a l'autorisation d'avoir le jeton mais il n'en veut pas.

• Un « OU » des sorties des contrôleurs produit le signal active.

• Si active = 0 aucun jeton n'est disponible, aucun contrôleur ne peut être selectioné.

Description de l'arbitre :

• Tous les ticks d'horloge l'arbitre change d'état de A →B→C→A ...

• La sortie sel = X si aucun contrôleur ne passe le jeton

• Sinon la sortie équivaut à l'état de l'arbitre.

Question 1 : Compiler le fichier verilog arbiter.v en fichier blif-mv à l'aide de l'outil vl2mv.

Question 2 : Lancer VIS. Lire la description blif-mv.

• Combien y a t'il de modèles différent dans la hierarchie ?

• Quels sont leur noms ?

• Combien y a t'il d'instance du modèle contrôleur ?

Question 3 : Faites un « cd » pour vous retrouver au niveau du controllerA dans la hierarchie.

• Combien de signaux d'entrées et de sorties a le controlleur ?

• Combien de variable BDD ?

• Combien as t'il d'état accessibles ?

1.2 Ecire un peu de code

Question 1 : Modifier le modèle pour avoir maintenant un quatrième contrôleur.

Question 2 : Modifier l'arbitre pour prendre en compte le quatrième contrôleur.

Question 3 : Vérifier vos changemement par simulation.

Tips : Pour obtenir le format des vecteurs de tests, taper la commande simulate, puis récuperer la sortie, la mettre dans un fichier et modifier se fichier avec vos propres vecteurs de test.

2 Robustesse d'un multiplieur

Dans cet exercice, nous allons considérer une architecture basique d'un multiplieur et voir si celle-ci résiste à des attaques aux rayons alphas. Une attaque aux rayons alpha entraine des bit-flips dans des éléments mémorisant (registres). C'est à dire qu'un registre contenant un 1 peut après une attaque contenir un 0, cela peut évidemment conduire a un comportement érronné du système (cite ...). Un bit-flip est une faute transitoire : le registre qui fait un bit-flip ne le fait pas en permanence.

L'objectif ici est de tester la robustesse du circuit. Pour cela, il va falloir modéliser l'injection de faute dans le système puis comparer le circuit résultant au circuit sans faute (appellé « golden model »). La comparaison se fera par equivalence checking.

2.1 Le multiplieur

Un fichier Verilog du multiplieur se trouve ici

Question 1 : Compiler le fichier Verilog multipler.v en fichier blif-mv à l'aide de l'outil vl2mv.

Question 2 : Dessinez l'automate de contrôle du multiplieur. Vous pouvez vous aider du fichier multi.pat qui est l'ensemble des vecteur de test qui réalise la multiplication de 12 x 2.

Question 3 : Écrire la plateforme de vérification qui réalise la composition synchrone de 2 multiplieurs.

Pour vérifier votre plateforme, vous réaliserez d'abord la composition d'un multiplieur avec lui-même, dans la suite en remplacera le deuxième multiplieur par le multiplieur fauté.

Question 4 : Écrire une propriété CTL pour vérifier l'équivalence des 2 multiplieurs, vérifier la propriété avec VIS.

2.2 Modélisation d'une faute

Nous allons modéliser le changement de valeur dans un registre pour un cycle donné.
Nous allons d'abord traiter le cas où la faute apparait dans un seul registre uniquement au cycle 1. Cela représente le cas où le système ne faisait rien, un bombardement est survenu puis l'environnement à demander un calcul et aucun autre bombardement n'arrivera.

Question 1 : Comment modéliser l'occurence d'une faute à un cycle donné pour un registre donné ?

2.3 Test de Robustesse

Pour chaque test de robustesse, on réalisera le calcul d'équivalence séquentielle entre le golden model et le modèle fauté.

Question 1 : Modéliser la faute dans un bit du registre operandB. Le circuit est-il robuste à cette faute ?

Question 2 : Modéliser la faute pour le registre accumulation. Le circuit est-il robuste à cette faute ? Pourquoi ?

Question 3 : Modéliser la faute dans un bit du registre operandA. Comparer les résultats selon si la faute est placé dans les bit de poids forts ou faibles.

Question 4 : Si on considère qu'après l'occurrence d'une faute au cycle 1 il n'y en aura plus, peut-on écrire une propriété qui montre que notre système sera correcte au bout d'un certain laps de temps ?

3 Model Checking : convertisseur de protocole VCI-PI

3.1 La plateforme VCI-PI

Dans l'exercice suivant, nous allons maintenant écrire l'architecture d'un convertisseur de protocole et quelques propriétés de sa spécification. L'exemple choisit est le convertisseur de protocole, VCI-PI. Ce convertisseur s'inscrit dans une architecture composé d'un maître et d'un esclave VCI communiquant à travers le bus PI. Chacun des IP VCI envoie des donnée sur le bus à l'aide de convertisseur de protocoles. Les schéma ci-dessous représente la plateforme de test.

Les wrappers sont transparents : du point de vue de l'initiateur VCI le wrapper maître joue le rôle de la cible et réciproquement, du point de vue de la cible VCI, le wrapper esclave joue le rôle de l'initiateur.

Le transfert de traduction d'un est illustré sur cette figure et procède de la manière suivante:

1. L'initiateur VCI envoie une requête au wrapper maître.

2. Le wrapper maître demande l'accès au bus via l'arbitre de bus (BCU).

3. Le BCU donne l'accès au wrapper maître (3a) et sélectionne le wrapper cible (3b).

   (4,5) Le wrapper maître envoie chaque cellule VCI au wrapper cible via le bus PI (en deux phases : adresse/données).

6. Le wrapper esclave traduit la cellule PI en une requête VCI et la transmet à la cible VCI.

7. La cible VCI répond au wrapper cible.

   (8,9) Le wrapper cible transmet la réponse du wrapper maître via le bus PI.

10. La réponse PI est traduite en réponse VCI et est ensuite transmise l'initiateur VCI.

3.2 Le wrapper maître

Le fonctionnement du wrapper se décompose en deux parties : la prémisse, qui attend une demande de l'interface VCI, demande et attend l'accès au bus ; la seconde partie correspond à l'échange de donnée proprement dite. Dans le but d'utiliser au maximum la fonctionnalité pipeline du PI bus,l'échange de donnée a un fonctionnement en trois phases réalisées par un pipeline, décrit de la manière suivante :

1. [AD] Envoie l'adresse de la requête k sur l'interface PI et reçoit la requête (k+1) sur l'interface VCI;

2. [DT] Envoie ou reçoit la donnée PI correspondant à la (k-1)ième requête VCI ;

3. [RSP] Envoie la réponse sur l'interface VCI correspondant à la (k-2)ième requête VCI.

Le protocole VCI envoie dans une cellule l'adresse et la donnée en même temps, alors que le protocole du PI bus décompose ce transfert en deux cycles. C'est pourquoi le premier étage du pipeline du wrapper reçoit l'adresse et la donnée k+1 en même temps qu'il envoie l'adresse k-1. La fin d'une transmission est marquée par l'activation du signal cmd_eop lors de l'envoi de la dernière cellule du paquet requête.

Dans le cas décrit dans la figure précédente, nous faisons l'hypothèse que l'environnement se comporte de façon idéale : toutes les requêtes d'écriture ou de lecture au PI bus et toutes les requêtes réponses à l'initiateur VCI seront satisfaites en un cycle.

Le code de la plateforme et du wrapper se trouvent ici

3.3 Spécification de la plateforme

Question 1 : Compiler et charger la plateforme dans VIS.

Question 2 : Vérifier les premières propriétés du fichier wrapper_a.ctl

Question 3 : Vérifier la propriété ... Expliquez le contre-exemple.

Question 4 : Que peut-on faire pour que la propriété passe ?

Question 5 : Ecrire Un fichier contenant la contrainte d'équité adéquate, refaire passer la propriété.

3.4 Compléxification du wrapper maître

Le comportement optimal n'admet aucun événement qui peut ralentir la progression du wrapper. Nous allons maintenant considérer l'événement suivant : l'esclave peut répondre qu'il n'est pas prêt à traiter la nouvelle requête (le bus PI peut maintenant émettre la valeur WAIT sur le signal pi_ack.

Le chronnogramme d'une transaction est alors le suivant :

Question 1 : Modifier la description du wrapper pour prendre en compte ces événements.

Question 2 : Reprendre la spécification CTL précédente, quels sont les propriétés qui ne passe plus ?

Question 3 : Ajouter les conditions d'équités. Quels sont les propriétés qui ne passent toujours pas ?

Question 4 : Comment doit-on les modifiées ?

3.5 Statistiques

Question 1 : Quel est la taille du FSM des 2 plateformes ?

Question 2 : Combien de variables BDD ont chacune des plateformes ?

Question 3 : En combien de temps passe la propriété globale ? Essayer avec un réordonnancement dynamique des variables BDD.

Question 4 : Conclusion ?