Les tests : retour aux origines

A partir du fichier "addaccu.ap", il est possible de réobtenir une description comportementale VHDL du composant et de la comparer avec un prouveur formel au fichier VHDL d'origine pour "prouver" que les deux sont identiques au sens du comportement.
Les variables d'environnement doivent être:

MBK_IN_PH=ap
MBK_IN_LO=al
MBK_OUT_LO=al

On commence par extracter la netliste au niveau des transistors avec lynx:

lynx -v -t addaccu addaccue

Ceci nous donne le fichier addaccue.al qu'il faut donner à yagle pour qu'il nous fournisse une description comportementale VHDL de cette netliste. Mais avant, il faut savoir que les signaux qui ont été déclarés comme registres vont gêner le prouveur formel qui a besoin des vrais noms des registres et pas les noms qui se trouvaient dans la netliste physique. Il faut donc dire à yagle de transformer ces noms. Creez le fichier "diviseure.inf" avec, a l'intérieur, les déclarations suivant:

rename
core.reg_0.dff_s : reg(0) ;
core.reg_1.dff_s : reg(1) ;
core.reg_2.dff_s : reg(2) ;
core.reg_3.dff_s : reg(3) ;
end

Pour trouver ce qu'il faut mettre dans un fichier .inf, vérifiez quels sont vos signaux registres, lancez: yagle -v     sur votre netliste logique extractée(ici addaccue.al) et éditez le fichier addaccue.vbe pour trouver comment les signaux registres ont été nommés (attention, dans addaccue.vbe, il faut prendre en compte le nom qui se trouve dans les commentaires en face de chaque définition SIGNAL). Le fichier .inf pourrait être plus court en en utilisant les jokers:

rename
core.reg_*.dff_s : reg(*);
end

Voilà. Maintenant on peut lancer yagle avec la commande suivante:

yagle -v -i addaccue

L'option -i sert à utiliser les informations de addaccue.inf. Les signaux ont étés renommés. On a notre description VHDL. Avant de lancer le prouveur formel, on vérifie qu'on a bien décommenté les déclaration de vdd,vss,vdde,vsse dans "addaccu.vbe", puis on lance:

proof -d -p addaccue addaccu

J'explique: -d sert à afficher les équations logiques quand il y a une erreur, et -p sert à prendre en compte une inversion de polarité qui est survenu pendant le mapping avec "scmap" et réinverse ces polarités dans le premier fichier qu'on lui donne. C'est pour ça qu'il est important de mettre le fichier addaccue en premier. Si tout se passe bien, on termine avec:

FORMAL PROOF : OK!

une dernière formalité est de lancer un vérificateur de design, druc sur la netliste physique addaccu.ap. Cette phase ne nous a jamais posé de problème:

druc addaccu

Et on est sûr que les règles de design sont respectées.
Les limites de cette réalisation:

- le fichier de patterns qui a servi pour la simulation comportementale est beaucoup trop court et ne rend pas compte de la validité de la description. Il y a deux solutions: soit on édite un fichier de patterns beaucoup plus long, mais ça peut devenir long et répétitif, soit on se penche sur un moyen de générer ces fichiers, et dans ce cas on a de la chance, car le programme "genpat", autorise la génération d'un fichier de patterns à partir d'un programme c (voir page man de genpat).
- il faudrait lancer une simulation avec asimut sur chaque netliste logique obtenue pour être encore plus sûr de ce qui se passe.