Changes between Version 24 and Version 25 of ToolsCourseTp5

Timestamp:

Sep 20, 2007, 1:54:29 PM (17 years ago)

Author:

anne

Comment:

--

ToolsCourseTp5

@@ -104 +104 @@
 l'outil ''' YAGLE ''' est capable d'extraire la description VHDL comportementale d'uncircuit au format '''.vhd''' à partir d'une ''netlist '' au format '''.al''' ''si celle-ci est au niveau transistor.''
 L'outil '''VASY''' permet de convertir une description VHDL comportementale du format '''.vhd''' au format '''.vbe'''. La commande à utiliser est :
- 
+{{{
+> export MBK_IN_LO=al
+
+> export YAGLE_BEH_FORMAT=vbe
+> yagle -s file1 file2
+> vasy -a -I vhd file1 file2
+}}}
+ Avant tout vous devez utiliser la commande :
+{{{
+>source avt_env.sh
+}}}
+
+Cette commande permet de mettre en place l'environnement nécessaire à l'utilisation de '''YAGLE''' ( le fichier avt_env.sh étant fourni )
+Les documentations pour cet outil se trouvent en :'''/users/soft/AvtTools2003/doc '''.
+
+=== 1.5 PROOF ===
+Lorsqu'on veut prouver l'équivalence de deux descriptions comportementales de type ''dataflow'' d'un même circuit à n entrées, on peut simuler par '''asimut''' 2n vecteurs pour les deux descriptions et les comparer.
+Cette solution devient vite coûteuseen temps CPU et il vaut mieux faire appel à un outil de preuve formelle qui effectue la comparaison ''mathématique'' des deux réseaux booléens.
+'''PROOF''' réalise cette opération entre les description file1.vbe et file2.vbe par la commande
+{{{
+>proof file1 file2
+}}}
 == 2 Schéma d'un inverseur ==
 Le schéma théorique d'un inverseur est présenté