Changes between Initial Version and Version 1 of MOCCA-TP2-2022


Ignore:
Timestamp:
Oct 13, 2021, 6:21:09 PM (3 years ago)
Author:
franck
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • MOCCA-TP2-2022

    v1 v1  
     1{{{
     2#!html
     3<h1> TP2 : Synthèse d'automate avec Alliance </h1>
     4}}}
     5
     6[[PageOutline]]
     7
     8= 1 Introduction =
     9
     10Le but de ce TP est de présenter quelques outils de la chaîne '''Alliance''' dont :
     11  * Les outils de synthèse logique '''syf''', '''boom''', '''boog''', '''loon''' ;
     12  * L'éditeur graphique de netlist '''xsch''' ;
     13  * Les outils pour la preuve formelle '''flatbeh''', '''proof''' ;
     14  * Le simulateur '''asimut''' ;
     15Chaque 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.
     16
     17[[Image(synthese_alliance.jpg, nolink, 600px)]]
     18
     19Ce TP portera donc sur les méthodes de génération et de validation d’une netlist de cellules précaractérisées.
     20En effet, même s’il est acquis que les outils de génération d’'''Alliance''' fonctionnent correctement, la validation de chaque vue générée est indispensable.
     21Elle permet de limiter le coût et le temps de la conception.
     22
     23Les dépendances de données dans le flux sont matérialisées dans la réalité par une dépendance de fichier.
     24Le fichier '''Makefile''' exécuté à l’aide de la commande '''make''' permet de gérer ces dépendances.
     25
     26'''L’usage de Makefile est obligatoire.'''
     27
     28Pour exécuter les outils d'Alliance vous devez ajouter dans le fichier .bashrc
     29{{{
     30source /soc/alliance/etc/profile.d/alc_env.sh
     31}}}
     32
     33== 1.1 Synthèse d'automates d'états finis ==
     34
     35Un circuit combinatoire pur ne dispose pas de registres internes.
     36De ce fait, ses sorties ne dépendent que de ses entrées primaires.
     37A l'inverse, un circuit séquentiel synchrone disposant de registres internes voit ses sorties changer en fonction de ses entrées mais aussi des valeurs mémorisées dans ses registres.
     38En conséquence, l'état du circuit à l'instant t+1 dépend aussi de son état à l'instant t. Ce type de circuit peut être modélisé par un '''automate d'états finis'''.
     39
     40[[Image(ex_digicode.jpg,nolink)]]
     41
     42=== 1.1.1 Automates de MOORE et de MEALY ===
     43
     44L'automate de MOORE voit l'état de ses sorties changer uniquement sur front d'horloge.
     45Les entrées peuvent donc bouger entre deux fronts sans modifier les sorties.
     46Par contre dans le cas d'un automate de MEALY, la variation des entrées peut modifier à tout moment la valeur des sorties.
     47Dans notre '''fsm''' (''finite-state machine''), on s’imposera de séparer la fonction de génération de la fonction de transition (automate de Moore).
     48Pour cela, deux process distincts matérialiseront le calcul du prochain état et sa mise à jour.
     49
     50[[Image(automate.jpg, nolink)]]
     51
     52=== 1.1.2 VHDL et SYF ===
     53
     54Afin de décrire de tels automates, on utilise un style particulier de description VHDL qui définit l'architecture fsm.
     55Le fichier correspondant possède également l'extension ''.fsm''.
     56A partir de ce fichier, l'outil '''syf''' effectue la synthèse d'automate et transforme cet automate abstrait en un réseau booléen.
     57'''syf ''' génère donc un fichier VHDL au format ''.vbe''.
     58
     59Comme la plupart des outils utilisés au laboratoire, il faut positionner certaines variables d'environnement avant d'utiliser '''syf'''.
     60Pour les connaître, reportez-vous au man de '''syf'''.
     61
     62=== 1.1.3 Exemple ===
     63
     64Afin de se familiariser avec la syntaxe de description d'un fichier ''.fsm'', un exemple
     65de compteur de trois "1" successifs est présenté. Sa vocation est de détecter par exemple sur une liaison série une séquence de trois "1" successifs. Le graphe d'états que l'on cherche à décrire est représenté sur la figure .
     66
     67Le format fsm est également décrit dans une page man. Pensez à la consulter.
     68
     69[[Image(graphe1.jpg, nolink)]]
     70
     71{{{
     72entity circuit is
     73  port ( ck, i, reset, vdd, vss : in bit;
     74         o : out bit
     75       );
     76end circuit;
     77
     78architecture MOORE of circuit is
     79
     80  type ETAT_TYPE is (E0, E1, E2, E3);
     81  signal EF, EP : ETAT_TYPE;
     82
     83  -- pragma CURRENT_STATE EP
     84  -- pragma NEXT_STATE EF
     85  -- pragma CLOCK CK
     86
     87begin
     88
     89  process ( EP, i, reset )
     90  begin
     91
     92    if ( reset = ’1’ ) then
     93      EF <= E0;
     94    else
     95      case EP is
     96        when E0 =>
     97          if ( i = ’1’ ) then
     98            EF <= E1;
     99          else
     100            EF <= E0;
     101          end if;
     102
     103        when E1 =>
     104          if ( i = ’1’ ) then
     105            EF <= E2;
     106          else
     107            EF <= E0;
     108          end if;
     109        when E2 =>
     110          if ( i = ’1’ ) then
     111            EF <= E3;
     112          else
     113            EF <= E0;
     114          end if;
     115        when E3 =>
     116          if ( i = ’1’ ) then
     117            EF <= E3;
     118          else
     119            EF <= E0;
     120          end if;
     121
     122        when others => assert (’1’)
     123          report "etat illegal";
     124      end case;
     125    end if;
     126
     127    case EP is
     128      when E0 =>
     129        o <= ’0’;
     130      when E1 =>
     131        o <= ’0’;
     132      when E2 =>
     133        o <= ’0’;
     134      when E3 =>
     135        o <= ’1’;
     136
     137      when others => assert (’1’)
     138        report "etat illegal";
     139    end case;
     140
     141  end process;
     142
     143  process( ck )
     144  begin
     145    if (ck=’1’ and not ck’stable) then
     146      EP <= EF;
     147    end if;
     148  end process;
     149
     150end MOORE;
     151}}}
     152
     153== 1.2 Synthèse logique et optimisation structurelle ==
     154
     155=== 1.2.1 Synthèse logique ===
     156
     157La synthèse logique permet d'obtenir une netlist de portes à partir d'un réseau booléen (format ''.vbe'').
     158Plusieurs outils sont disponibles.
     159
     160L'outil '''boom''' permet l'optimisation de réseau booléen avant synthèse.
     161
     162L'outil '''boog''' réalise la projection structurelle du comportement sur la bibliothèque de cellules précaractérisées '''sxlib''' afin d'obtenir la '''netlist'''.
     163La netlist pouvant être soit au format ''.vst'' soit au format ''.al'', pensez à vérifier la variable d'environnement '''MBK_OUT_LO'''.
     164
     165=== 1.2.2 Résolution des problèmes de fanout (sortance) ===
     166
     167Les netlists générées contiennent parfois des signaux internes attaquant un nombre important de portes (grand fanout).
     168Ceci se traduit par une détérioration des fronts (rise time et fall time).
     169Il y a alors une perte en performance temporelle.
     170Afin de résoudre ces problèmes, l'outil '''loon''' remplace les cellules ayant un fanout (i.e sortance) trop grand par des cellules plus puissantes ou bien insère des buffers.
     171
     172=== 1.2.3 Visualisation de la chaîne longue ===
     173
     174A tout moment, les netlists peuvent être visualisées graphiquement. L'outil '''xsch''' permet de visualiser le chemin le plus long grâce aux fichiers ''.xsc'' et ''.vst'' générés à la fois par '''boog''' et par '''loon'''.
     175
     176||[[Image(T_RC.jpg,nolink)]]||La résistance équivalente '''R'''  est calculée sur la totalité des transistors du AND appartenant au chemin actif. De même, la capacité '''C''' est calculée sur les transistors passants du NOR correspondant au chemin entre i0 et la sortie de la cellule.||
     177
     178=== 1.2.4 Vérification de la netlist ===
     179
     180La netlist doit être certifiée.
     181Pour cela, on dispose du simulateur '''asimut''', mais aussi de l’outil '''proof''' qui procède à une comparaison formelle de deux descriptions comportementales (''.vbe'').
     182L’outil '''flatbeh''' permet d’obtenir le nouveau fichier comportemental à partir de la netlist.
     183
     184= 2. Travail à effectuer =
     185
     186Les différentes parties seront automatisées à l'aide d'un fichier '''Makefile'''.
     187
     188== 2.1 Réalisation d'un compteur ==
     189     
     190   * En s'inspirant du compteur de trois "un" présenté, écrire au format ''.fsm'' la description d'un compteur de cinq "un" successifs sous la forme d'un automate de Moore.
     191   * Synthétiser l'automate avec '''syf''' avec les options de codage '''-a''', '''-j''', '''-m''', '''-o''', '''-r''' et en utilisant les options '''-CEV'''.
     192     Penser à bien positionner les variables d'environnement.
     193{{{
     194> syf -CEV -a <fsm_source>
     195}}}
     196  * Visualiser les fichiers ''.enc''.
     197  * Ecrire le fichier ''.pat'' de vecteurs de test.
     198  * Simuler avec '''asimut''' toutes les vues comportementales obtenues.
     199
     200'''Que se passe-t-il si le reset n'est pas positionné en début de pattern ? Pourquoi ? '''
     201
     202== 2.2 Réalisation d'un digicode ==
     203
     204On veut réaliser une puce pour digicode.
     205Les spécifications sont les suivantes :
     206
     207  * Les chiffres de 0 à 9 sont codés en binaire naturel sur 4 bits.
     208  * A et B sont codés comme suit : A = 1010, B = 1011.
     209  * Le digicode fonctionne en deux modes :
     210    * Mode Jour : La porte s'ouvre en appuyant sur "O"
     211    * Mode Nuit : La porte ne s'ouvre que si le code est correct
     212  * Pour distinguer les deux modes un **timer externe** calcule le signal jour.
     213    Ce signal vaut ’1’ entre 8h00 et 20h00 et ’0’ sinon.
     214  * Le digicode commande une alarme dès qu'un des chiffres entrés n'est pas le bon
     215  * L'automate revient dans son état d'attente automatiquement dans deux cas, grâce à
     216    un **timer externe** active le signal reset :
     217    1. si rien n'est entré au clavier au bout de 5 secondes,
     218    2. si l'alarme a sonné pendant 2mn.
     219  * La puce fonctionne à une fréquence de 10MHz
     220  * Toute pression d'une touche du clavier est accompagnée du signal press_kbd.
     221    Celui-ci signale à la puce que les données en sortie du clavier sont valides.
     222    Ce signal est à 1 durant un cycle d’horloge.
     223
     224Le code est 53A17.
     225
     226**Remarques :**
     227 * On ne vous demande pas de programmer les timers, mais vous pouvez dans votre compte rendu faire un schéma représentant le clavier, les timers et l'automate.
     228 * Le code de l'automate est câblé, toutefois si vous vous le souhaitez vous pouvez rendre votre digicode programmable. Dans ce cas il vous appartient de proposer une spécification, puis de l'implémenter.
     229
     230L'interface de l'automate est le suivant :
     231{{{
     232  in ck
     233  in reset
     234  in jour
     235  in i[3:0]
     236  in O
     237  in press_kbd
     238  out porte
     239  out alarm
     240}}}
     241
     242Vous devez :
     243  * Dessiner le graphe d'états de l'automate.
     244  * Ecrire au format ''.fsm'' l'automate.
     245  * Synthétiser l'automate avec '''syf''' en utilisant les options de codage '''-a''', '''-j''', '''-m''', '''-o''', '''-r''' et en utilisant les options '''-CEV'''.
     246{{{
     247> syf -CEV -a <fsm_source>
     248}}}
     249  * Ecrire le fichier ''.pat'' de vecteurs de test.
     250  * Simuler avec '''asimut''' toutes les vues comportementales obtenues.
     251
     252'''Question''' :
     253Quelles sont vos remarques concernant la complexité des expressions (i.e. temps) et le nombre de registres (i.e surface) des descriptions comportementales suivant les encodages ?'''
     254'''Comparez aussi leurs nombres de littéraux.'''
     255
     256  * Lancer l'optimisation du réseau booléen avec l'outil '''boom''' en demandant une optimisation en '''surface''' puis en '''délai'''.
     257{{{
     258> boom -V <vbe_source> <vbe_destination>
     259}}}
     260  * Essayer '''boom''' avec différents algorithmes '''-s''', '''-j''', '''-b''', '''-g''', '''-p'''... Le mode et le niveau d'optimisation sont aussi à changer.
     261  * Comparer le nombre de littéraux après factorisation.
     262
     263Pour chacun des réseaux booléens obtenus précédemment, effectuer le mapping sur cellules précaractérisées :
     264  * Synthétiser la vue structurelle (en faisant attention à bien positionner les variables d'environnement) en lançant l'outil '''boog'''.
     265{{{
     266> boog <vbe_source> <vst_destination>
     267}}}
     268  * Observer l'influence des options de '''syf''' et de '''boom''' avec les différences netlists obtenues.
     269  * Valider le travail de '''boog''' en resimulant avec '''asimut''' les netlists obtenues avec les vecteurs de test qui ont servi à valider le réseau booléen initial.
     270  * Utiliser '''xsch''' pour visualiser la netlist.
     271{{{
     272> xsch -I vst -l <vst_source>
     273}}}
     274Cet outil vous permet de visualiser le chemin critique, représenté en rouge.
     275
     276Si vous utilisez l'option '-slide' qui permet d'afficher un ensemble de netlists, n'oubliez pas d'appuyer sur les touches '+' ou '-' pour éditer vos fichiers !
     277
     278Pour toutes les vues structurelles obtenues précédemment :
     279  * Optimiser la netlist en lancant l'outil '''loon'''.
     280{{{
     281> loon <vst_source> <vst_destination> <lax_param>
     282}}}
     283  * 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.
     284
     285'''Quelle est, selon vous, la meilleure des netlists ? Pourquoi ?'''
     286
     287À effectuer sur cette netlist :
     288  * 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.
     289
     290  * Deux précautions valent mieux qu’une ! Faire une vérification formelle de la netlist en la comparant au fichier comportemental d’origine issu de '''syf'''.
     291{{{
     292> flatbeh <vst_source> <vbe_dest>
     293
     294> proof -d <vbe_origine> <vbe_dest>
     295}}}
     296
     297  * Comparer si les deux fichiers sont bien identiques.
     298
     299= 3 Compte rendu =
     300
     301Vous rédigerez un compte-rendu pour ce TP dans lequel vous ferez attention à bien répondre aux questions posées ici (en gras).
     302Vous inclurez les différents résultats obtenus surface/temps/optimisation.
     303
     304Vous déposerez le compte rendu sur le formulaire reçu par mail
     305Le dessin du graphe du digicode peut être fait avec  [http://www.graphviz.org graphviz]
     306([https://graphviz.gitlab.io/_pages/Gallery/directed/fsm.html exemple]). Si vous n'avez pas le temps, faite un scan du graphe sur papier.
     307
     308Vous ferez attention à joindre les différents Makefile créés de façon à ce que la commande '''make''' effectue les différentes étapes de ce TP.
     309Ces fichiers doivent également fournir une règle '''clean''' qui permet d'effacer tous les fichiers générés.
     310
     311Ces règles seront à suivre durant tous les TPs de Tools.
     312
     313= Makefile =
     314
     315Le Makefile permet d'exprimer le processus de construction d'un circuit.
     316
     317[[Image(makefile.png, nolink, 400px)]]