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 deux parties:

1. La formalisation d’une spécification textuelle
2. L’implémentation d’un composant à partir d’une spécification formelle

Pour la syntaxe et la sémantique des différents opérateurs SVA, regarder les supports du cours.

0. Préparation

Pour cette exercise, la classe est divisée en groupes de quatre (deux binômes). Vous trouvez le dépôt git de votre groupe dans le tableau suivant:

Groupe	Répo
1	tp-sva-groupe1
2	tp-sva-groupe2
3	tp-sva-groupe3
4	tp-sva-groupe4
5	tp-sva-groupe5
6	tp-sva-groupe6

Chaque binôme va ensuite mettre en place son environnement de travail: suivez le lien dans la dernière colonne du tableau pour trouver votre répertoire git. Copiez le lien donné sur le site (par exemple git@gitlab.enst.fr:se206/tp-sva-groupe6.git) et récupérez les sources pour commencer votre travail:

git clone git@gitlab.enst.fr:se206/tp-sva-groupeX.git

avec X le numéro de votre groupe.

1. Spécifications

Chaque groupe va traiter deux composants: un arbitre de type « round robin » et une queue d’écriture. Les binômes « A » vont d’abord formaliser l’arbitre et les binômes « B » la queue d’écriture. A la fin de la première partie de l’exercise, les binômes de chaque groupe vont s’échanger leurs résultats. Ceux qui ont formalisé la spécification de l’arbitre vont se trouver avec une spécification d’une queue d’écriture et vice versa. 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.

La propriété la plus difficile à formuler en SVA est la dernière. 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 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

Dans le répertoire qui correspond au module que vous traitez (arbiter ou wqueue) se trouve une dossier verif qui contient l’environnement de vérification. Entre autre, il y a un fichier check_*.sv à compléter avec les propriétés formalisés en SVA.

Pour le moment, il n’existe pas d’implémentation des modules sous vérification, mais des modules vides à remplir dans la deuxième TH de ce TP. Néanmoins, vous pouvez lancer le processus 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.

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.

---

3. Implémentation et Vérification

Après la première partie de ce TP, chaque binôme devrait avoir produit une spécification formelle sous forme de propriétés SVA et une documentation sous forme de traces témoins et contre-exemples. Pour l’implémentation, échangez vos productions avec l’autre binôme de votre groupe qui a fait le même travail pour l’autre module. Si vous avez bien respecté les consignes, vous devriez avoir travaillé sur le même répertoire que l’autre binôme. Alors, mettez à jour le répertoire, et récupérez les changements des autres (à éxécuter dans le dossier verif):

git add check_*.sv
git commit -m "put useful message here"
git push origin master
git pull origin master

Si l’autre binôme a été plus rapide, il est possible que vous devrez faire un merge avant de pouvoir publier vos changements.

Prenez le temps de regarder et comprendre la spécification avant de commencer le travail d’implémentation. Il est bel et bien possible que la spécification ne soit pas complètement correcte ou même contradictoire. Vous devrez alors corriger les propriétés à fur et à mésure.

Dans le sous-dossier src du composant à implémenter se trouve un fichier *.sv qui contient un module vide que vous devrez compléter pendant la suite du TP.

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

Si vous ne l’avez pas encore fait, déplacez-vous dans le dossier verif. Pour lancer l’interface graphique de l’outil de vérification, tapez

make check_gui

ce qui – après quelques temps – 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).