Vérification formelle

Supports des cours:


Le but de ce TP est de vous permettre de vous exercer à la spécification formelle à l'aide d'un langage de logique temporelle, les SystemVerilog Assertions (SVA). L'exercise est divisé en trois parties:

  1. La formalisation d'une spécification textuelle (En préparation du TP; la spécification complète vous sera fourni au début du TP)
  2. La correction d'un composant mal implémenté (arbitre) en utitlisant un outil de vérification statique
  3. L'implémentation complète d'un composant (file d'attente) à partir d'une spécification formelle

Pour la syntaxe et la sémantique des différents opérateurs SVA, regarder les supports du cours. En plus, il y a un document pdf plus exhaustif dans le répertoire git du TP.

1. Spécifications

On va traiter deux composants: un arbitre de type "round robin" et une queue d'écriture. Dans la suite, vous trouvez la déscription informelle des deux composants.

1.A. Arbitre

Il s'agit d'un arbitre qui est censé de contrôler l'accès à une ressource commune (tel qu'un bus mémoire) à trois masters. Les masters signalent leurs demandes en mettant l'entrée req correspondante à 1, et l'arbitre donne la main à un des masters - suivant son algorithme d'arbitrage - en mettant la sortie gnt correspondante à 1. Une propriété de l'algorithme "round robin" est qu'il n'y a pas de priorité statique. Si il y a plusieurs requêtes simultanées, l'arbitre va donner la main à tour de rôle. Ce qui a pour conséquence que l'algorithme ne laisse personne mourir de faim (non-starvation en anglais): chaque requête va être servie finalement.

Exemple de fonctionnement

La figure montre un exemple de fonctionnement de l'arbitre. A partir du cycle 1, les trois masters font des requêtes simultanées. La première requête est acquise au cycle 2. Le deuxième et troisième master obtiennent la main dans les cycles 4 et 6. Noter que le premier master, après avoir laché sa requête (cycle 3), demande la main directement après (cycle 4). Mais, suivant le protocol "round robin", c'est le troisième master qui est servi d'abord.

Hypothèses sur l'environnement

Comme c'est le cas pour beaucoup de composants, le bon fonctionnement de l'arbitre dépend de certaines hypothèses sur l'environnement. Dans notre cas, on suppose que les masters suivent un protocol très simple:

H1: Une requête, une fois émise, ne doit pas être retirée avant qu'elle soit acquittée.
H2: Une requête, une fois acquittée, devra être retirée.

Noter que pour H2, une requête qui a été acquittée va rester active pendant le temps que le master se sert de la ressource avant de retirer la requête. Ce temps peut varier, mais il reste fini.

Propriétés à vérifier

On définit en suite les propriétés qu'une implémentation correcte doit respecter:

P1: Pendant le cycle suivant un reset, il n'y a pas d'acquittement.
P2: Il n'y a jamais plus d'un acquittement actif en même temps.
P3: Chaque requête sera acquittée (après un temps fini).
P4: L'acquittement reste stable jusqu'à ce que la requête correspondante soit relachée.
P5: S'il n'y a pas d'autres requêtes, une requête doit être traitée après un cycle au plus tard.
P6: Il n'y a pas d'acquittement sans requête.
P7: L'arbitrage est "fair".

Alors que la plupart de ces propriétés devrait être claire, la dernière est sûrement la plus difficile à formuler et à vérifier. Une possibilité pour exprimer P7 d'une façon plus précise est la suivante: Si un master i emet une requête, avant que celle-ci soit acquittée, l'arbitre peut acquitter au plus une requête pour chaque autre master j (j≠i).

1.B. Queue d'écriture

Il s'agit d'une queue d'écriture qui sert à découpler un master (tel qu'un processeur) et un esclave (tel qu'une mémoire). Le but est de permettre au master d'effectuer des écritures se suivant rapidement, même si la mémoire a un temps de réaction de plusieurs cycles. Vu que la taille de la queue est finie, cela exige que le master n'écrit pas en permanence, mais plutôt en petits paquets d'accès alternant avec des temps sans accès. A la base, la queue est du type first-in-first-out (FIFO). Les signaux we_s (write enable), adr_s (addresse), dat_s (data) et ack_s (acknowledge) correspondent à l'interface esclave qui va recevoir les requêtes du master (processeur). De l'autre côté se trouve l'interface master connectée à un esclave (une mémoire) et qui va émettre les requêtes qui ont été reçues par le master (le processeur). De plus, les signaux empty, full et elems donnent des informations sur l'état de la queue: état vide, état complet, et nombre de requêtes actuellement stoquées. La taille de notre queue sera de trois éléments. Les entrées et sorties d'addresses et de données ont une taille de huit bits, le compteur d'éléments a trois bits.

Exemple de fonctionnement

La figure montre un scénario d'utilisation de la queue. Après le reset, une première écriture dans la queue est effectuée (we_s actif, cycle 2) est elle est acquittée par la queue (ack_s actif) immédiatement. Suite à cette écriture, le status du module change (empty inactif, elems = 1 en cycle 3) et la requête est émise sur l'interface master (we_m actif) jusqu'à l'acquittement (ack_m actif, cycle 5). Ensuite se déroulent trois écritures en rafale (cycles 8 à 10) qui sont elles aussi relayées à l'interface master (cycles 9 à 21).

Hypothèses sur l'environnement

Pour le bon fonctionnement, il nous faut quelques hypothèses simples sur le comportement des modules qui se connectent sur les deux interfaces de la queue d'écriture. Pour la vérification, on va supposer que ces modules respectent bien le protocole pour effectuer et acquitter des accès en écritures:

H1: Chaque requête d'écriture sur l'interface esclave reste stable jusqu'à ce qu'elle soit acquittée.
H2: Chaque requête sur l'interface master sera acquittée.

H3: Il n'y a pas d'acquittement sur l'interface master sans demande d'accès.

Noter que pour H2, le temps entre une requête et l'acquittement peut varier, mais il reste fini.

Propriétés à vérifier

On définit ensuite les propriétés qu'une implémentation correcte doit respecter:

P1: Après un reset, la queue est vide.
P2: La queue est vide si et seulement si le nombre d'éléments est zéro.
P3: La queue est pleine si et seulement si le nombre d'éléments est trois.
P4: Si la queue n'est pas pleine, chaque requête entrante est acquittée immédiatement.
P5: La queue emet une requête si et seulement si elle n'est pas vide.
P6: Chaque requête entrante sera finalement emise sur l'interface master.
P7: Les requêtes entrantes sont emises dans l'ordre.
P8:
Toute requête entrante est acquittée en temps fini.
 

La propriété la plus difficile à formuler en SVA est P7. Une possibilité est de la décomposer selon le nombre d'éléments qui se trouvent dans la queue. Réfléchissez sur le moment où une requête entrante doit être émise si la queue est actuellement vide (contient 1,2,3 éléments). Une façon plus avancée est d'utiliser une variable locale comme compteur, qui va décrémenter chaque fois qu'une donnée est enlevée de la queue. Au moment où le compteur arrive à la valeur zéro, la donnée considérée devrait apparaître à la sortie.


2. Formalisation

L'objectif du premier exercice (en préparation du TP) est de comprendre la spécification textuelle de votre module et de la formaliser en SVA.

2.1 Témoins et Contre-exemples

Dans un premier temps, avant de passer à l'écriture du code SVA, on va regarder de plus prêt les hypothèses et propriétés. Pour chaque hypothèse et propriété, répondez aux questions suivantes:

  • Identifiez s'il s'agit d'une propriété de sûreté (safety) ou de vivacité (liveness)
  • Donnez - sous forme d'un dessin - une trace qui vérifie la propriété (témoin / witness)
  • Donnez une autre trace qui ne vérifie pas la propriété (contre-exemple / counter-example)

Si vous n'arrivez pas tout de suite à identifier le type d'une propriété, il est souvent utile de construire un contre-exemple d'abord. S'il existe un contre-exemple de longeur finie, il s'agit d'une propriété de sûreté, sinon de vivacité. Vous pouvez écrire plusieurs traces par propriété si vous jugez cela utile pour la compréhension.

2.2 SystemVerilog Assertions

Après avoir visualisé les témoins et les contre-exemples, passez à la formalisation des propriétés en SVA. Pour le moment, il suffit d'écrire les propriétés sur papier. La syntaxe exacte n'est pas important, il s'agit de capter au mieux l'intention de chaque propriété. Pour beaucoup de propriétés, il peut y avoir plusieurs façons de les spécifier en SVA. Il est même possible que la spécification textuelle soit imprécise ou ambiguë. Par exemple, l'expression "jusqu'à" peut être formalisé avec différents opérateurs SVA comme until ou until_with qui n'ont pas la même sémantique. Dans ce cas, il va falloir choisir ce qui vous semble le plus raisonable. La formalisation sert en faite à clarifier la spécification et à éliminer les ambiguïtés.

2.3 Comparaison avec la Spécification Finale

Au jour du TP, vous allez avoir accès au dépôt git pour récupérer la spécification en SVA ainsi que des parties d'implémentation en SystemVerilog. Allez dans votre répertoire personelle du cours se303 et effectuez les commandes suivantes:

git checkout master
git remote add tp-sva git@gitlab.enst.fr:se303/tp-sva.git
git remote update
git merge --allow-unrelated-histories tp-sva/master

Il y a deux dossiers (arbiter et wqueue) qui correspondent aux deux modules. Dans les deux cas, vous trouvez les propriétés SVA dans le dossier verif.


3. Deboggage avec qformal

Dans un premier temps, il s'agit de corriger une mauvaise implémentation de l'arbitre. Prenez le temps de regarder et comprendre la spécification avant de commencer le travail. Pour le moment, il existe une implémentation incomplète de la spécification dans le fichier src/arbiter.sv.

3.1 Simulation

Le dossier simu contient l'environnement de simulation. Si vous vous déplacez dans ce dossier, vous pouvez lancer Modelsim en tapant

make simu_gui

Cette commande va d'abord compiler les sources du module sous vérification et du test bench (qui se trouve dans le dossier tb_src). Pour les deux composants, le test bench va simuler aléatoirement des scénarios d'usage, en respectant les contraintes d'entrée (hypothèses). Cette simulation vous sert pendant le développement pour vous assurer que votre implémentation fait bien quelque chose qui n'est pas complètement faux. Mais attention: aucune vérification n'est effectuée pendant la simulation. Elle ne remplace donc pas la vérification formelle que vous devrez effectuer (voir instructions ci-dessous).

3.2 Vérification

Néanmoins, vous pouvez aussi lancer le processus de de vérification. Cela peut servir à effectuer un contrôle de la syntaxe de vos propriétés SVA. Pour cela, allez dans le dossier verif de votre projet et tapez

make check

pour la version en ligne de commande ou

make check_gui

pour lancer l'interface graphique de l'outil de vérification. Attention, l'outil est assez bavard et il n'est pas toujours facile de retrouver les messages d'erreurs de syntaxe dans le bruit ASCII que produit la vérification. Après quelques temps la dernière commande devrez vous amener à une fenêtre comme la suivante:

Dans l'onglet Properties vous trouvez le résultat de la vérification. Les propriété qui n'ont pas été validées sont marquées par un F rouge. En faisant un double click sur le nom de l'assertion, un contre-exemple va être généré ce qui vous sert à debogger votre code ou la spécification. Des warnings sont indiqués par un petit triangle jaune. Attention: Dans la version testée, l'actualisation du modèle après un changement des sources (ou de la spécification) ne se fait pas toujours (ou jamais) automatiquement. Pour recharger le modèle et relancer la vérificatioin, ouvrez longlet Transcript et tapez dans la shell

source check.tcl

Le but ultime est d'arriver à implémenter le composant en respectant la spécification formelle. Vous avez atteint votre but si toutes les propriétés passent la vérification (sans warning).


4. Implémentation de la file d'écriture

Dès que vous avez réussi à réparer l'arbitre, allez dans le répertoire wqueue où se trouve la spécification et l'environnement de simulation et de vérification pour le deuxième module, la file d'écriture. Comme pour l'arbitre, vous pouvez simuler le module pour voir son comportement. Pour s'assurer que vous avez bien implémenté votre module, utilisez la vérification formelle. Vous avez attaint votre but si toutes les propriétés passent la vérification (sans warning).

Même si l'implémentation (src/wqueue.sv) est presque vide, vous pouvez déjà lancer la vérification. Déplacez-vous dans le répertoire verif et tapez

make check

Vers la fin du rapport, vous trouvez les lignes suivantes:

# [00:00:01] Fired @1: wqueue_inst.P1_empty_after_reset
# [00:00:01] Fired @1: wqueue_inst.P2_empty_iff_zero
# [00:00:01] Fired @1: wqueue_inst.P3_full_iff_three
# [00:00:01] Fired @1: wqueue_inst.P4_quick_acknowledge
# [00:00:01] Fired @1: wqueue_inst.P5_issue_unless_empty
# [00:00:01] Fired @2: wqueue_inst.P7_in_order_1
# [00:00:01] <strong><span style="color:#B22222;">Vacuously Proven: wqueue_inst.P7_in_order_2</span></strong>
# [00:00:01] <strong><span style="color:#B22222;">Vacuously Proven: wqueue_inst.P7_in_order_3</span></strong>
# [00:00:01] <strong><span style="color:#B22222;">Vacuously Proven: wqueue_inst.P7_in_order_4</span></strong>
# [00:00:01] Status: Done 9/10, Update 9/10, Proof radius min=0, avg=0, Mem=0GB
# [00:00:01] Status: Done 9/10, Update 0/1, Proof radius min=0, avg=0, Mem=0GB
# [00:00:01] Status: Done 9/10, Update 0/1, Proof radius min=0, avg=0, Mem=0GB
# [00:00:01] Fired @3: wqueue_inst.P6_issue_eventually
# [00:00:01] Status: Done 10/10, Update 1/1, Proof radius min=N/A, avg=N/A, Mem=0GB
# [00:00:01] At end of run 3 engine processes were not yet connected
#
# ---------------------------------------
# Property Summary                  Count
# ---------------------------------------
# Assumed                               3
# Proven                                3
#   <strong><span style="color:#B22222;">Vacuous                             3</span></strong>
# Inconclusive                          0
# Fired                                 7
#   Fired with Warning                  7
# ---------------------------------------
# Total                                13
# ---------------------------------------

Alors, même avec un module vide, on arrive à prouver trois des assertions. Comment est-ce possible?

 

Fichier attachéTaille
Image icon qformal.png62.56 Ko
PDF icon Lecture slides2.62 Mo
PDF icon Vérification formelle2.61 Mo
PDF icon SystemVerilog Assertions528.45 Ko
PDF icon se303b-2018-verif.pdf551.6 Ko
PDF icon se303b-2018-sva.pdf525.73 Ko