Changes between Version 32 and Version 33 of ToolsCourseTp1

Timestamp:

Sep 18, 2008, 4:31:09 PM (18 years ago)

Author:

cobell

Comment:

--

ToolsCourseTp1

@@ -9 +9 @@
   * Les outils de synthèse logique '''SYF''', '''BOOM''', '''BOOG''', '''LOON''' ;
   * L'éditeur graphique de netlist '''XSCH''' ;
+  * Les outils pour la preuve formelle '''FLATBEH''', '''PROOF''' ;
   * Le simulateur '''ASIMUT''' ;
 Chaque outil possède ses propres options donnant des résultats plus ou moins adaptés suivant l'utilisation que l'on veut faire du circuit.
@@ -174 +175 @@
 
 La netlist doit être certifiée.
-Pour cela, on dispose du simulateur '''ASIMUT'''.
+Pour cela, on dispose du simulateur '''ASIMUT''', mais aussi de l’outil '''PROOF''' qui procède à une comparaison formelle de deux descriptions comportementales (.vbe).
+L’outil '''FLATBEH''' permet d’obtenir le nouveau fichier comportemental à partir de la netlist.
 
 = 2. Travail à effectuer =
@@ -186 +188 @@
      Penser à bien positionner les variables d'environnement.
 {{{
->syf -CEV -a <fsm_source> -
+> syf -CEV -a <fsm_source>
 }}}
   * Visualiser les fichiers '''.enc'''.
@@ -234 +236 @@
   * Le synthétiser avec '''SYF''' en utilisant les options de codage '''-a''', '''-j''', '''-m''', '''-o''', '''-r''' et en utilisant les options '''-CEV'''.
 {{{
->syf -CEV -a <fsm_source> -
+> syf -CEV -a <fsm_source>
 }}}
   * Ecrire le fichier '''.pat''' de vecteurs de test.
@@ -248 +250 @@
   * Lancer l'optimisation booléenne avec l'outil '''BOOM''' en demandant une optimisation en '''surface''' puis en '''délai'''.
 {{{
->boom -V <vbe_source> <vbe_destination> -
+> boom -V <vbe_source> <vbe_destination>
 }}}
   * Essayer '''BOOM''' avec les différents algorithmes '''-s''', '''-j''', '''-b''', '''-g''', '''-p'''... Le mode et le niveau d'optimisation sont aussi à changer.
@@ -258 +260 @@
   * Synthétiser la vue structurelle (en faisant attention à bien positionner les variables d'environnement) :
 {{{
->boog <vbe_source> -
+> boog <vbe_source>
 }}}
   * Observer l'influence des options de '''SYF''' et de '''BOOM''' avec les différences netlists obtenues ;
@@ -278 +280 @@
   * Lancer '''LOON'''.
 {{{
->loon <vst_source> <vst_destination> <lax_param> -
+> loon <vst_source> <vst_destination> <lax_param>
 }}}
   * Effectuer une optimisation de fanout en modifiant le facteur de fanout dans le fichier d'option '''.lax'''. Imposer des valeurs de capacités sur les sorties.
@@ -289 +291 @@
   * Valider le travail de '''LOON''' en resimulant sous '''ASIMUT''' les netlists obtenues avec les vecteurs de test qui ont servi à valider la vue comportementale initiale.
 
+Deux précautions valent mieux qu’une ! Faîtes une vérification formelle de votre netlist en la comparant au fichier comportemental d’origine issu de '''SYF''' :
+
+{{{
+> flatbeh <vst_source> <vbe_dest>
+
+> proof -d <vbe_origine> <vbe_dest>
+}}}
+
+  * Comparer si les deux fichiers sont bien identiques.
+
 = 3. Compte rendu =
 
-Vous rédigerez un compte-rendu d'une page maximum pour ce TP, et vous joindrez les fichiers écrits (et uniquement les fichiers écrits, pas ceux générés par les différents outils).
-Vous ferez attention à bien répondre au question posées ici dans le compte rendu, vous y inclurez les différents résultats obtenus surface/temps/optimisation).
+Vous rédigerez un compte-rendu d'une page maximum pour ce TP dans lequel vous ferez attention à bien répondre aux questions posées ici (en gras).
+Vous inclurez les différents résultats obtenus surface/temps/optimisation
+
+De plus, vous joindrez les fichiers écrits (et uniquement les fichiers écrits, pas ceux générés par les différents outils !).
 Vous ferez également attention à joindre les différents Makefile créés de façon à ce que la commande '''make''' effectue les différentes étapes de ce TP de A à Z.
+Ces fichiers doivent également fournir une règle '''clean''' qui permet d'effacer tous les fichiers générés.
+
+Ces règles seront à suivre durant les prochains TPs.
 
 = 4. Annexe : Makefile =