VHDL2TA: Outil de traduction en automates temporisés - SoC
Contents
1. 31 32 time_front time front time time front front up dn signal VADLID time NUMBER value 0 1 up up UP dn down DOWN dn DN I B 4 La grammaire des propri t s TCTL des sp cifications en UPPAAL extraite de LP Y 97 Prop E lt gt StateProp A StateProp StateProp AtomicProp StateProp not StateProp StateProp or StateProp StateProp and StateProp StateProp imply StateProp AtomicProp Id Id Id RelOP Nat Id RelOP Id Op Nat RelOp lt lt 1 gt 1 gt 1 Op 1 Id Alpha Id AlphaNum Nat Num Num Nat Alpha Al 1lZlal lz Num 01 19 AlphaNum Alpha Num 32 322. La commande vhdl2ta Isvl vhd e Isvl env t Isvl tmp 2 m ta o Isvl ta taf upl pa Isvl q t_ setup permet d effectuer l analyse instanci e sur les param tres en utilisant le model checker d UPPAAL afin de r duire les temps de setup des signaux d entr e du circuit d crit 1svl Les propri t s v rifier sont d crites dans le fichier lsvl1 q La description en UPPAAL g n r e Isvl ta int gre toutes les valeurs optimales des temps de setups r duits La commande vhdl2ta sp 3x2 vhd t sp 3x2 tmp 1 m temp o sp 3x2 check tmp tm configs_check permet de d tecter et d liminer les fausses configurations dans les fichiers de timing associ s aux portes de l architecture abstraite de la m moire SPSMALL Le fichier principal sp_3x2 check tmp contient les chemins vers les nouveaux fichiers de timing qui ne contiennent que les bonnes configurations La commande vhdl2ta sp 3x2 vhd t sp 3x2 tmp 1 m temp o sp 3x2 delays tmp tm delay files permet de g n rer le fichier d intervalles de d lais partir des fichiers de timing associ s aux portes du circuit et aussi partir de la description fonctionnelle sp_3x2 vhd La commande vhdl2ta sp _ 3x2 vhd t sp 3x2 timing tmp 2 m temp o sp_3x2 timing tmp tm timing file ts random permet de g n rer les fichiers de timing associ s aux portes de l architecture abstraite de la m moire SPSMALL partir de la description fonctionnelle du circuit en VHDL sp_3x2 vhd et partir d
3. sup u sup l Sdn Ou u sdn peuvent tre instanci es ou bien laiss es comme des param tres avec l sup lt u sup et l sdn lt u sdn selon le type de l analyse subs quente effectu e instanci e ou param tr e Chaque automate temporis est d terministe dans les transitions d actions mais pas dans les transitions de temps moins que sup u sup et I sdn u sdn Cependant il arrive parfois que m me dans le cas ou toutes les bornes des intervalles sont toutes gales le mod le global est quasi d terministe car des transitions concurrentes provenant des automates diff rents et franchissables au m me instant peuvent provoquer de l ind terminisme Cependant les sources d ind terminisme sont tr s r duites 8 32 ro l a E Ne risings WN OOOO y Eg Uy A b gt NG A Ta Fa N i Kr 9 A Nw a 7 N F l l k N E a pr hh A il ho P UN N stable s Y C YS FIR EQ A 4 i N o N A 4 a eh Poi a A an V A Pal i L Falling e Xx Ni s lt f gt k 9 T aa p A N C JA A E 1 i m b U N aE gt Mi nn V a k K Pa T N aa L N N K closefs pe Sd gt paad PS lt pa A NA fr y Ut 1 l lt g gt ga vg Mas a a ctive giW 7 Ca N ng lt 0 1 stable qi er an e a a _ N A zg fl g gt Figure 2 Les automates repr sentants les affectations des blocs s quentiels 3 Impl mentation VHDL2TA Dans cette partie on pr sente l architecture d
4. 4 32 fonctionnelle MYGALE LBG 98 et l outil d abstraction temporelle TIMEX en partant d une description au niveau transistors 2 3 L algorithme de traduction Les principes g n raux de l algorithme sont les suivants Dans ce mod le chaque bloc de la description VHDL est traduit en automate temporis qui mod lise la propagation des fronts montants et descendants des signaux d entr e sur la sortie de la porte en respectant les d lais de propagation induits par le bloc repr sent Avec ce mod le les fronts des signaux sont identifi s et propag s sur les sous parties du circuit Cependant la d tection de ces fronts n cessite l utilisation de variables afin de m moriser la valeur du signal avant et apr s l action d criture Ceci simplifie la t che d analyse ult rieure Dans ce mod le chaque automate temporis poss de une horloge locale qui permet de mesurer le d lai de propagation On distingue deux intervalles de d lais pour la propagation des fronts de sortie le d lai de propagation de chaque bloc est compris dans un intervalle d sup D sup ou d sdn D san selon le sens du front de sortie propag Ces intervalles sont d crits par des parametres Ce modele une extension du modele bi bounded inertial delay d crit dans MP 95 et BJM Y 02 Dans ce dernier mod le le temps de propagation d un front d une entr e d un bloc vers sa sortie est compris dans un unique intervalle d D En fait on ne distin
5. assign x s 0 L x0 s gt 1 x0 s guard e 2 0 sync e 2 down L x0 s gt 1 x0 s guard e 2 1 sync e 2 up L x0 s gt 1 x1 s guard e 2 1 0 and e 1 sync e 2 down assign x s 0 dy L x0 s gt 1 x1 s guard e 2 1 1 and e 1 sync e 2 up assign x s 0 L x0 s gt 1 f s guard x s gt delta0 1 s sync s down assign s 0 ERL g AL Se L guaro e L 0 Syne e L downme fy L x1 s gt 1 x1 s Guara e 1 Syne el up Jy es Ae ae Guard t bao and 6 2 sync e L down assign xs 07 Le rd OS t yuard e L gt let and e 2 s y Sync L p27 assigA 8 5S OF bj Tee als guard 6 2 0 syne 6 2 downs Jy LL Sr oe de querra e 2r she Syne e 2 4877 ly LS Je 0 Guard 2 PQ ama e L 7 Syne e 2 dowa assigo x S 1 07 LA gt L US guaro ea sil and L Heyne e 2 Alpe assign 22 81 OR Ss e AE S guard x s gt deltal 1 s sync s up assign s 1 27 32 LES A AS guard e 1 0 syne e 1 down Lafe Sass Less guard e 1 1 sync e 1 up LA gt de els guard e 1 1 0 and e 2 0 sync e 1 down assign x s 0 l L Eo ROS guard e 1 1 0 and Goca e Ff SYNC e downs asigna S Su d E ES L L guard e 1 1 1 and e 2 sync e 1 up assign xXx s O d E ly RO E guard e 1 1 1 and e 2 0 sync e 1 up assign x s Ue LE LES guard e 2 0 sync e 2 down e Ce H T guard e 2 1 syn
6. d lais tr s serr s avec lesquels on distingue les fronts montantes des fronts descendants de la sortie plut t que de les associer en un seul large intervalle l enveloppe convexe de l union des deux intervalles 5 32 2 3 1 Repr sentation des blocs combinatoires chaque bloc combinatoire qui affecte un signal s une nouvelle valeur est repr sent par un automate TA s compos de trois tats stable s rising s et falling s L tat stable s est un tat passive dans lequel la valeur du signal s est conforme la configuration d entr e m me si cette derni re change L tat rising s resp falling s est un tat de calcul sur lequel on passe chaque fois qu une nouvelle configuration d entr e qui induit un nouvel front montant resp descendant sur la sortie s apr s un d lais sup compris entre les deux bornes l sup et u sup resp sdn compris dans sdn u sdn On peut transiter entre les deux tats rising s et falling s dans le cas o deux fronts successifs sur les configurations d entr e qui induisent deux fronts oppos s sur la sortie surviennent avant que la sortie pour le premier front se stabilise Avec cette repr sentation seuls les fronts significatifs sont calcul s et pass s travers les blocs du circuit Ceci permet d avoir des calculs optimis s La figure pr sente l automate temporis associ l affectation concurrente s lt f e_1 e_m qui affecte le signal s Les trans
7. de la porte n_xor le comportement de la sortie de la porte qu on attend SS ron on Me da apy 16171 die 1234220 Ge est d crit par la propri t TCTL pr sent e ci dessous All CCOCES 0 and lt 6 or t 14 and t lt 16 or t gt 24 imply Ss 1 and t gt 7 and teks Or Atel and E lt 23 amply s 0 La BNF des propri t s de la logique TCTL employ es dans les sp cifications UPPAAL est pr sent e dans l annexe B 4 13 32 4 3 Les commandes d appel de VHDL2TA VHDL2TA peut tre employ en plusieurs modes diff rents e Mod le d automates temporis s on g n re la description de r seaux d automates temporis s partir de la description comportementale en VHDL de la description temporelle du circuit et du comportement des signaux d entr e e Programme VHDL temporis pr t simuler on g n re ce dernier programme partir des m mes descriptions d entr e que celles employ es dans le mode pr c dent e Mod le temporel il existe deux sous modes principaux Dans la premier mode mod le temporel complet on g n re les fichiers de timings associ s aux portes du circuit partir de leur fonctionnalit et les intervalles de d lais de propagation de ses fronts Dans le deuxi me mode mod le temporel bi bounded delay on g n re un fichier d intervalles de d lais des deux fronts pour chaque porte partir des fichiers de timing et de la description en VHDL du circuit e Optimisation VHDL ce
8. e Les transitions lt e gt lt e gt et lt f gt se produisent a chaque fois que la sortie est verrouill les gardes sont toutes a 0 et quand un changement sur l une des gardes gi de la valeur O 1 apparait l valuation de la fonction fi e est n cessaire Ici on distingue deux cas 1 si la valeur de la sortie s repr sent e par la variable vs est gale la valeur evalu e de la fonction fi e alors on passe directement via les transitions de l ensemble lt f gt vers l tat stable stable s 2 dans le cas contraire on passe via les transitions de l ensemble lt e gt resp lt e gt vers l tat de calcul rising s resp falling s si l valuation de la fonction fi e est gale 1 resp 0 afin d attribuer la valeur fi e 1 resp fi e 0 la variable vs et produire un front montant resp descendant sur la sortie s apr s l coulement d un d lai cup resp O Sdn Ce front produit sera propag comme un v nement d clencheur pour les automates ult rieurs Les autres transitions r f rent l occurrence des fronts sur les signaux apparus dans les affectations du processus et des changements sur les variables interm diaires associ es aux gardes gi qui n induisent pas de changements sur la valeur de la sortie s les transitions qu bouclent 2 3 3 Insertion des contraintes temporelles dans ce mod le pour chaque bloc dont la sortie est le signal s les bornes des deux intervalles de d lais
9. g pt cette option permet d indiquer le type des param tres temporels employer Il existe deux types 1 associer un seul param tre pour un v nement temporel ex deltaO d lai de propagation des fronts descendants sur la sortie de la porte n_xor 2 associer deux param tres pour un v nement temporel repr sentant les deux bornes extr mes de ce dernier ex delta0_ 1 delta0_u repr sente l intervalle de d lais de propagation des fronts descendants sur la sortie de la porte n_xor Par d faut l option prend cette derni re valeur Ce dernier type est bien adapt pour repr senter les intervalles de d lais de propagation des fronts sur la sortie des portes de circuits Bien que on peut sp cifier un intervalle de d lais avec un seul param tre dans les descriptions en HyTech et IMITATOR avec un seul param tre contrairement aux descriptions en UPPAAL ne traite pas le cas param tr 15 32 fig_opt abr g To cette option est employ e uniquement dans le mode d emploi ta du fait de son utilit Elle permet d indiquer l outil VHDL2TA d optimiser la figure repr sentant la description comportementale en VHDL avant de g n rer le mod le d automates temporis s Ceci permet d avoir des mod les plus optimis s que le mod le original A titre d exemple on n a r ussi passer un mod le d un circuit sur l outil d analyse HyTech qu apr s l utilisation de cette option Bien que le mod le de ce circuit passe
10. la garde de la transition vers l tat stable qui d clenche un front montant resp descendant sur la sortie s D autre part on distingue deux tats stables sur la sortie s l tat stable s qui correspond la stabilit de la sortie quand au moins l une des gardes gi est valu e vrai dans ce cas s est stable sur la valeur de fi e t q i est l indice minimum tandis que la location stable close s correspond au cas ou aucune garde gi n est satisfaite et la sortie s est verrouill le processus est ferm Le d clenchement des transitions est caus par le changement des variables interm diaires associ es aux gardes et aussi par le changement des signaux apparus dans les affectations de processus Donc les transitions sont sensibles implicitement aux changements des signaux de sensibilit du processus l ensemble e Les transitions des ensembles lt a gt lt a gt lt b gt lt b gt lt c gt lt c gt de la figure 2 sont similaires celles du mod le des portes combinatoires pr sent pr c demment d crit dans la figure 1 lorsque le processus correspond un registre ouvert Les transitions de l ensemble lt d gt lt d gt et lt f gt se produisent chaque fois qu un changement sur la valeur de la garde gi de la valeur O est apparue et toutes les autres gardes gk tel que k 1 sont 0 La sortie reste stable sur l ancienne valeur calcul e dans le cas des transitions de l ensemble lt f gt s fi
11. les choix de mod lisation 2 1 Le mod le de base d automates temporis s En r sum un automate temporis AD 94 est une machine tats finie enrichie avec des horloges qui voluent toutes avec la m me vitesse et qui peuvent tre mises z ro Un tat est un couple Lv o J est une location ou tat de contr le et v est une configuration de valeurs des horloges Chaque location est associ e une conjonction de contraintes lin aires sur les horloges appel e un invariant Un tat 1 v poss de deux types de transitions e une transition discr te tiquet e par un label d action not e e vers l tat v si v satisfait la contrainte associ e e appel e garde et v est obtenue partir de v en rempla ant certaines horloges par z ro les horloges apparues dans la liste des mises jour de la transition e e une transition d coulement du temps de d lai f l tat L v si v v t et pour tout t t q 0 lt t lt t v t satisfait l invariant associ J La composition parallele de deux automates temporis s est obtenue par la synchronisation de deux ou plusieurs transitions tiquet es sur la m me action Un r seau d automates temporis s est une composition parall le de deux ou plusieurs automates temporis s Ce dernier repr sente le modele global du syst me analys Les r seaux d automates temporis s sont bien analys s avec les techniques de model checking Divers outils d analyse on
12. 08 E Andr E Encrenaz L Fribourg Modeles d automates temporis s pour l analyse de circuits m moire D livrable D3 1 Projet VALMEM Janvier 2008 AEF 09 E Andr E Encrenaz L Fribourg Synthesizing Parametric Constraints on Various Case Studies Using IMITATOR Research Report LSV 09 13 Laboratoire Sp cification et V rification ENS Cachan France June 2009 18 pages AF 10 E Andr et L Fribourg Behavioral Cartography of Timed Automata In Antonin Kucera and Igor Potapov diteurs RP 10 LNCS 6227 Springer pages 76 90 septembre 2010 BBCELR 10 A Bara P Bazargan Sabet R Chevallier E Encrenaz D LeDu P Renault Formal Verification of Timed VHDL Programs International Forum on Specification and Design Languages 2010 BE 10a A Bara E Encrenaz Analyse de l architecture abstraite de la m moire SP SMALL 3x2 bits Reunion VALMEM Dec 2010 BE 10b A Bara E Encrenaz VHDL2TV outil de g n ration des programmes VHDL temporis s pr ts simuler rapport interne de l equipe Soc Lip6 2010 BE 11a A Bara E Encrenaz VHDL2TA http www Isv ens cachan fr encrenaz valmem vhdl2ta index html 2011 BE 11b A Bara E Encrenaz VHDL2TA outil de traduction des circuits d cris en VHDL en automates temporis s Jeu de Tests rapport interne de l equipe Soc Lip6 2011 25 32 BJMY 02 M Bozga H Jianmin O Maler and S Yovine Verification of asynchronous circuit
13. U 23 32 Nous avons aussi confirm que les valeurs de temps de thold est compris dans l intervalle 1633 718 en utilisant aussi la m thode inverse En fait nous avons re g n r le syst me de contraintes nouveau en rempla ant manuellement cette fois que les valeurs de temps de hold par des param tres dans la description en IMITATOR 2 g n r e Tous les autres param tres sont instanci s par les valeurs du point Pi0 Les contraintes obtenues sur le temps de hold sont donn es par 633 lt thold lt 718 6 Remarques finales L outil VHDL2TA permet de g n rer des mod les d automates temporis s en les d crivant dans le format d entr e des outils d analyse UPPAAL HyTech ou IMITATOR 1 et 2 Ces mod les repr sentent le comportement fonctionnel et temporel de circuits analyser L outil est test sur divers exemples de circuits asynchrones certains avec des m moires De plus les mod les g n r s repr sentant des circuits cent portes ont t analys s par le model checker d UPPAAL C est le cas de l architecture compl te abstraite de la m moire SPSMALL de 3 mots de 2 bits extraite au LIPO Une pr sentation d taill e de l analyse de cette derni re est donn e dans BE 10a L outil VHDL2TA a aussi t employ dans l approche d analyse de circuits propos e dans BBCELR 10 Cette approche permet d offrir une nouvelle opportunit aux concepteurs de circuits Ils pourraient analyser automatiquement la fo
14. VHDL2TA Outil de traduction en automates temporis s des circuits d crits en VHDL Manuel d utilisation Equipe Architecture et Logiciels des Syst mes sur Puce ALSOC Laboratoire d Informatique de PARIS 6 LIP6 Unit Mixte de Recherche UMR 7606 CNRS UPMC Abdelrezzak BARA Emmanuelle ENCRENAZ 12 Janvier 2011 R sum Ce document est un guide d utilisation de l outil VHDL2TA Translation of VHDL Programs to Timed Automata qui effectue la traduction en r seaux d automates temporis s de circuits num riques dont la partie fonctionnelle est d crite en VHDL et dont la partie temporelle des leurs portes est donn e par un ensemble de d lais Les r seaux d automates temporis s g n r s par l outil sont d crits dans le langage de description de l un des outils d analyse suivants UPPAAL HyTech IMITATOR ou IMITATOR 2 Cette traduction permet de faciliter la t che d analyse de circuits en utilisant les techniques d accessibilit et de model checking L outil VHDL2TA a t utilis dans l approche d analyse de circuits propos e dans BBCELR 10 Mots cl s Automates temporis s logique temporelle TCTL Model checking temporis s Accessibilit HyTech UppaaL IMITATOR Circuits asynchrones Circuits M moires Langage VHDL Abstraction fonctionnelle MYGALE Abstraction temporelle TIMEX 1 32 Architecture de la m moire SPSMALL Table des mati res 1 Introduction 2 Traduction automatique en automa
15. aleur fausse Evidement comme dans l tat stable stable s de l automate pr sent dans la section pr c dente tous les fronts sur les signaux de l ensemble e qui n induisent pas de changements sur la valeur de la garde gi sont mod lis s par des transitions qui bouclent de l tat stable stable g vers lui m me L affectation du signal s est repr sent par un autre automate pr sent dans la figure 2 pour la lisibilit tous les labels de synchronisation et les gardes de transitions ont t omis Toutes les affectations produisant un front montant sont regroup es dans un unique tat de calcul rising s tandis que les affectations produisant un front descendant dans un tat de calcul falling s Ce regroupement r duit la taille de l automate mais induit la r union de tous les intervalles de d lais associ s ces affectations l enveloppe convexe de la r union en fait les bornes sup rieures des intervalles de d lais O sup i resp O sdn i sont repr sent es comme des invariantes d tats de la 7 32 forme xs lt u Sup i resp xs lt u sdn 1 et le maximum de ces bornes sera repr sent comme l invariante de l tat rising s resp falling s de la forme xs lt max u supX 1 u Sup n resp xs lt max u sdn 1 u Sdn n de minimum des bornes inf rieures est repr sent comme une condition xs gt min I sup 1 Sup n resp xs min l san 1 I sdn n dans
16. bien sur les autres outils d analyse sans aucune optimisation de figure parametric_analysis abr g pa cette option est n employ e que dans le mode d emploi ta et quand l option ta_format est gale au format up descriptions en UPPAAL En utilisant cette option on peut effectuer l analyse instanci e sur les param tres temporels tels que les temps de setup et de hold des signaux d entr e des circuits analys s en utilisant le model checker d UPPAAL afin de r duire leurs valeurs Cette option prend en param tres 1 le fichier des propri t s TCTL obligatoire qui d crit ce qu on veut v rifier 2 le type de param tres r duire t_ setup s il s agit des temps de setup et t_hold s il s agit des temps de hold param tre optionnel par d faut c est t_setup On note que dans la plupart du temps ces propri t s d crivent le comportement des signaux de sorties des circuits analys s La description en UPPAAL g n r e int gre toutes les valeurs optimales des temps de setup ou des temps de hold r duits D autres options Loptions sont possibles passer en param tres pour la commande vhdl2ta Ces options sont employ es dans tous les modes d emploi de VHDL2TA On va les d couvrir plus loin dans la section 4 3 5 4 3 2 Programme VHDL temporis pr t simuler Dans ce mode ce programme est g n r partir des m mes descriptions d entr e que celles employ es dans le mode pr c dent La syntaxe de la co
17. c e 2 up LAS da ES guard e 2 1 0 and e 1 0 sync e 2 down assign x s Up LOE e gt ROS guard e 2 1 0 and e 1 1 sync e 2 down assign x s Us LI dle LS guard e 2 1 1 and e 1 1 sync e 2 up assign xX s O L fea s gt 29 guard e 2 1 1 and e 1 0 sync e 2 up assign x s 0 Instansiation des processus X env nd signals il env nd signals 1 Ass s il Ass s pa Definition du systeme 1 X system env nd signals il ASS Ss 11 28 32 B Les grammaires des descriptions d entr e de VHDL2TA B 1 La grammaire des descriptions fonctionnelles en VHDL vhdl_file entity architecture entity ENTITY VHDLID IS PORT ports END VHDLID ports port ports port port VHDLID mode BIT mode IN OUT E architecture ARCHITECTURE VHDLID OF VHDLID IS def_signals TBEGIN statements END VHDLID def_signals def_signal def_signals def_signal def_signal SIGNAL VHDLID BIT statements statements signal_assignment_statement statements process_statement signal_assignment_statement VHDLID AFFECT exprl exprl expr expr op2 expr expr BITVALUE VHDLID expr op2 expr NOT expr expr expr VADLID EQ BITVALUE process_statement process_label PROCESS signals_names_list TBEGIN process_statement_part END PROCESS process_label 3 process_
18. d aussi un deuxi me param tre optionnel quand le premier param tre pass est gal 1mi2 Ce param tre indique le mode dans lequel les descriptions en IMITATOR 2 sont g n r es On note que l outil IMITATOR 2 accepte trois modes d emploi 1 reachability qui permet de faire l analyse d accessibilit 2 inversemethod qui permet d appliquer d algorithme de la m thode inverse ACEF 09 pour la synth se des contraintes sur les param tres 3 bca qui permet d appliquer l algorithme BCA Behavioral Cartography Algorithm AF 10 afin de calculer la cartographie du syst me avec les deux variantes cover et randomX ta_version abr g tav indique le type du mod le d automates temporis s g n rer On distingue deux types de mod les 1 le mod le original dans lequel on associe des locations X0_1 X1_1 F_1 pour chaque affectation concurrente 1 d un processus branch par une garde 2 le mod le dans lequel on regroupe toutes les locations associ es aux affectations concurrentes 1 d un processus en locations XO X1 et F C est le mod le d automates pr sent dans la section 2 de ce manuel et qui a t employ dans les tests des circuits pr sent s dans BE 11a la page web de l outil VHDL2T A Ce dernier mod le est une abstraction du premier Par d faut cette option prend la valeur model_grp_locs repr sentant le deuxi me mod le le premier mod le est repr sent par la valeur model_ecl_locs param type abr
19. dique le format VHDL dans lequel les composants associ s aux portes du circuit sont repr sent s Les composants peuvent tre repr sent s soit par des processus process soit par des affectations concurrentes assign Il est tr s recommand d employer la premi re repr sentation pour diff rents raisons car elle est bien adapt e pour repr senter les blocs s quentiels et elle permet une meilleure lisibilit du code Cette option prend la premi re valeur par d faut 4 3 3 Mod le temporel Ce mode contient aussi deux sous modes principaux mod le temporel complet ce mode permet de g n rer les fichiers de timing associ s aux portes du circuit partir de la description fonctionnelle du circuit en VHDL et de la description temporelle donn e sous forme d un fichier d intervalles de d lais La syntaxe de la commande employ e 1c1 est donn e comme suit vhdl2ta lt vhld file gt temp lt temp file gt 2 mode temp out lt temp file gt options mod le temporel bi bounded delay Inversement en utilisant la syntaxe de la commande pr sent e ci dessous on peut g n rer un fichier d intervalles de d lais a partir des fichiers de timing associ s aux portes du circuit ainsi que sa description fonctionnelle vhdl2ta lt vhld_file gt temp lt temp file gt 1 mode temp out lt temp file gt options Il existe aussi un autre mode qui permet de d tecter et d liminer les fausses configurations dans les fichiers de
20. dl lt xorl and ck latch process andl d begin if andl 1 then a lt d end 1f end process END Nous avons effectu deux tests similaires 20 32 21 32 Premier test Nous avons pris un environnement de signaux d entr es et avons fix des d lais pour les portes du circuit avec lesquels la sp cification mentionn e ci dessous est satisfaite Puis nous avons montr que le comportement du signal de sortie O est conforme ce qui est d crit dans la sp cification Le temps de r ponse TCK gt Q doit tre inf rieur au cycle de l horloge Nous avons effectu l analyse en utilisant le model checker UPPAAL sur le mod le g n r par l outil VHDL2TA La description de ces d lais des portes et la description de cette environnement sont donn s comme suit Envi automaton environment clock Ck with chi L000 tLo 1000 inverse neyel s 2 7 1000 tip 2000 down L000 upp 2000 down d 1000 up 1634 down 2200 up 3000 down 3634 D laisi NOCE STATS Loe HO E D haat 3 HO SACS MATE and 2 SS oso Qui latch lt 240 240r 3 La description en UPPAAL g n r e par l outil est caract ris e par e 5 automates associ s aux signaux de sortie et aux signaux internes de circuit les automates d environnement e 5 horloges locales correspondant aux automates l horloge globale 2 5 variables discr tes associ es aux signaux du circuit e 4 x 5 param tres associ s aux d lais des f
21. e l outil ses modules ses descriptions d entr e sortie et ses caract ristiques 3 1 Architecture et impl mentation Principalement VHDL2TA int gre e un analyseur qui permet de donner une repr sentation structurelle aux descriptions d entr e de l outil qui sont syntaxiquement correctes la description fonctionnelle du circuit en VHDL la description temporelle des portes du circuit et la description d environnement des signaux d entr e e des modules de g n ration de descriptions d entr e des outils d analyse UPPAAL HyTech et IMITATOR 2 partir du format interm diaire produit par l analyseur l utilisateur peut choisir le type de la description de sortie qu on g n re 9 32 3 2 Les descriptions d entr e et sortie Comme le montre la figure 4 l outil prend en entr e les descriptions suivantes b up c 0 d a up b dn c 1 d 1 a dn D i Las a lt b or c xor dr Fichier temporel b 5 up 20 down process a b c 10 down 25 up begin d 15 up if a 1 then A Fichier environnement VHDL comporte N C L iA V UM vhdl TA b up de x a 10 t R seau d automates mn v temporis s Hytech Ne os Uppaal x asd PP Figure 4 Les descriptions d entr e sortie de l outil VHDL2TA la partie fonctionnelle du circuit programme VHDL est donn e par une description en VHDL Chaque bloc combinatoire resp s quentiel est d crit par une affectation concurrente resp proce
22. ectent une nouvelle valeur un seul signal donn Le format de ces affectations et de ces processus est d crit ci dessous Le fragment de la grammaire VHDL qui g n re ce sous ensemble du langage VHDL est donn dans l annexe B 1 S E delle de e E E E Process Name Process Me dy se ve e me begin uf guardi then e Ed A else Guard 2 Chen gt Eh else stt guard n then s lt fn end La description de la porte n_xor en VHDL est donn comme suit BNCE Declaration Architecture Declaration ENTITY mi xor IS ARCHITECTURE are OF n xor IS PORT 5 OUL BIT BEGIN el E Sen BIT s lt not e 1 xor e 2 eZ in BIT END arc END n xor 4 2 2 La partie temporelle du circuit d lais des portes d crit les d lais de propagation des fronts montants et descendants des signaux sur les portes du circuit G n ralement la description est donn e sous forme d un fichier dans lequel deux intervalles de d lais ou un d lai ponctuelle sont associ s respectivement aux fronts montants et descendants de chaque porte mod le temporel bi bounded delay Delai pour chaque front 62 kyle a LT 3s Une autre option consiste a associer un fichier de timing pour chaque porte modele STG complet Dans ces fichiers on associe un d lai ponctuel pour chaque configuration et pour chaque front d un signal d entr e d une porte qui induit un changement sur la sortie Un exemple d un modele temporel complet pour la porte n_
23. ement est d crit comme suit Envl automata environment clock ck with thi 1000 tlo 1000 inverse ncycles 1 0k 1 1000 up 2000 down down da 1000 up 1634 down Le comportement de la sortie O attendu est donn ci dessous Le temps de r ponse est bien conforme ce qui tait sp cifi Q 1467 up Nous avons fait encore des tests pour toutes les valeurs de Thold 634 717 Le temps de r ponse TCK gt Q est compris dans l intervalle 633 718 le comportement du signal de sortie O est toujours le m me Donc la sp cification est toujours satisfaite Nous avons repouss ensuite les tests cette fois en utilisant la description en IMITATOR 2 g n r e par l outil VHDL2TA Nous avons attribu des modifications sur cette description en rempla ant manuellement les valeurs de temps de setup et de hold du signal d par des param tres La description obtenue est employ e pour g n rer le syst me de contraintes synth tis es pour ce point en utilisant l outil IMITATOR 2 m thode inverse Ce syst me de contraintes synth tis es qu on note par K est exactement le m me que celui pr sent dans AEF 09 Il est donn comme suit lio gt U Tur gt THold Snatch THold Latcht gt not11 Onotat xor And Hold gt Notit Anat Lateh Onotit Not2t Oxort gt THold T Setu p 7 0 And OLatcht gt Not2t ONot 11 _ OX ort Not2t gt And OAndt gt U Notit gt Not1l Ono gt
24. euvent tre appliqu es Avec cette d marche on peut prouver formellement les propri t s temporelles complexes cit es ci dessus obtenir des informations sur la marge d erreur des caract ristiques temporelles ou bien extraire des contraintes lin aires temporelles param tr es Cette m thodologie d analyse temporelle de circuits en appliquant le formalisme d automates temporis s a t introduite par Maler et Pnueli dans MP 95 Pour faciliter une telle analyse 1l serait pratique d avoir un outil pour traduire automatiquement une description fonctionnelle VHDL combin e des d lais de propagation en formalisme d automates temporis s Ceci est l objet de l outil VHDL2TA Les mod les d automates temporis s g n r s par l outil sont sp cifi s dans les langages de description des outils d analyse tels que UPPAAL LPY 97 HyTech HHW 95 IMITATOR A 09 et IMITATOR 2 A 09 L outil VHDL2TA est bas sur la m thode de traduction dont les principes sont d crits dans BBCELR 10 Le mod le g n rique des portes de circuits propos MP 95 BJMY 02 a t tendu et sera pr sent e dans la section suivante de ce manuel L outil VHDL2TA a t d velopp au LIP6 Universit de Pierre et Marie Curie Paris 6 dans le cadre du projet ANR VALMEM Son code binaire ainsi que quelques exemples de tests de circuits sont t l chargeables partir de la page web r f renc e BE 1 la Organisation du manuel la deuxi me secti
25. gue pas le sens du front propag L algorithme propos est d crit formellement comme suit e Identification et cr ation des variables globales pour chaque bloc combinatoire ou s quentiel associ un signal s cr er une horloge locale xs une variable bool enne vs des labels de synchronisation sup et sdn des bornes de d lais l sup u sup l sdn u sdn e Pour chaque affectation concurrente associ e a un signal s cr er TA s voir la sous section 2 551 e Pour chaque processus associ a un signal s cr er NTA s voir la sous section 2 3 2 Instancier les param tres de d lais voir la sous section 2 3 3 e Cr er TA ou NTA pour l environnement des signaux d entr e La composition des automates cr s constitue le modele globale associ au circuit a analyser Les traces temporelles du mod le simulent bien les propagations des fronts des signaux sur les blocs combinatoires et s quentiels du circuit L ensemble des traces temporelles est complet chaque ex cution potentielle du circuit est repr sent e par une trace temporelle dans le modele L ensemble des traces temporelles est une sur approximation de l ensemble d ex cutions du circuit ceci est d aux approximations des d lais des blocs du circuit par des intervalles On peut donc avoir des traces temporelles qui ne correspondent a aucune trace d ex cution du circuit Cette sur approximation est r duite par l utilisation de deux intervalles de
26. ichiers de timing de configurations mod le temporel complet des portes d un circuit donn partir de sa description VHDL et du fichier de d lais de ses portes mod le temporel bi bounded delay Inversement il existe aussi un moyen de g n rer un fichier des intervalles de d lais des deux fronts pour chaque signal partir des fichiers de timing et de la description VHDL du circuit e D tection et limination des fausses configurations dans les fichiers de timing associ s aux portes d un circuit donn 4 Mode d emploi de VHDL2TA 4 1 Installation L outil est disponible en t l chargement sur le site web dont l URL est donn e ci dessous http www asim lip6 fr ema valmem vhdl2ta index html 4 2 Les descriptions d entr e de VHDL2TA Dans cette partie on d finit le format des descriptions d entr e de l outil employ es pour g n rer le mod le d automates temporis s repr sentant un circuit donn e On se sert de la porte n_xor 11 32 comme exemple dont la sortie est nomm e s et les deux entr es sont nomm es el et e2 respectivement 4 2 1 La description fonctionnelle du circuit est un programme VHDL o les blocs combinatoires du circuit sont d crits par des affectations concurrentes et les blocs s quentiels sont d crits par des processus Les programmes accept s par l analyseur de l outil ne contiennent que des affectations simples et des processus de type If elseif elseif else qui aff
27. ions qui bouclent Fa ON li LE J ee a A c N Te 0 f risimg s N E T D ss lt ul lt b gt a 7 Fa 7 a 7 E 1 P _ ol d Ela gt T a o y Hae e af a gt Y LC T E 1 n 9 i BI c A S A s able s l a _ A I 0 RES Li 7 A i E l d x A a AE lmer PJ l L ia _ Ma a Ta ul ES 0 N i a e R Figure 1 l automate repr sentant l affectation d un bloc combinatoire 6 32 2 3 2 Repr sentation des blocs s quentiels chaque bloc s quentiel est repr sent par un processus Le format g n ral des processus d crits en VHDL qu on mod lise est donn comme suit PROCESS Se de de ve EL begin le PE e peel Then Eo ty else uE 0 2 Chem G2 a BZ Oy LF elses 1t T then s lt fn end Comme on peut le constater ce processus prend en entr e un ensemble de signaux d entr e not e fe_l e_m et attribue une nouvelle valeur au signal de sortie s si l une de ses gardes est satisfaite par la configuration courante des signaux d entr e On peut voir ce processus comme une collection de n commandes avec des gardes exclusives dont les variables sont les signaux qui appartiennent a la liste de sensibilit du processus l ensemble e qui attribuent des nouvelles valeurs au signal de sortie s du processus Une commande avec une garde i tel que iin 1 n est mod lis e par not gl and and gi gt s lt fi e o s lt fi e est
28. itions de l ensemble lt b gt resp lt b gt r f rent l occurrence d un front sur l un des signaux de l ensemble e e_1 e_m induisant un front montant resp descendant sur la sortie s qui tait stable sur la valeur 0 resp 1 apr s un d lai amp sup resp O Sdn ici on transite vers l tat de calcul rising s resp falling s dans lequel on attend l coulement du d lai de propagation amp Sup resp O sdn repr sent comme un invariant d tat xs lt U Sup resp xs lt u sdn avant de passer vers l tat stable stable s avec un nouveau front montant resp descendant sur la sortie s La transition lt a gt resp lt a gt r f re la production d un front montant resp descendant sur la sortie s une fois que le d lai de propagation amp Sup resp O Sdn est coul repr sent comme une garde de transition xs gt l sup resp xs gt l sdn ici la sortie se stabilise sur la valeur 1 resp 0 Les transitions de l ensemble lt c gt resp lt c gt r f rent l occurrence d un front sur l un des signaux d entr e pendant que le mod le est dans l tat du calcul rising s resp falling s pour la production d un front montant resp descendant sur la sortie qui induit un changement sur cette valeur de calcul de la sortie s Les autres transitions r f rent l occurrence des fronts sur les signaux de l ensemble e qui n induisent pas du changement sur la sortie s les transit
29. its d crits en VHDL en r seaux d automates temporis s d crits dans le langage de description des outils d analyse tels que UPPAAL HyTech IMITATOR et IMITATOR 2 e L outil int gre un module nomm figure2tv qui permet de g n rer des programmes VHDL temporis pr ts simuler partir des descriptions d entr e qu on emploi pour g n rer les mod les d automates temporis s L outil VHDL2TV BE 10b est d di aussi pour cette t che e L outil int gre un module de r duction de figures repr sentation structurelle du programme VHDL produites lors de la phase de l analyse syntaxique de description fonctionnelles des circuits En cons quence les mod les d automates temporis s g n r s partir des figures r duites sont plus concis e Fn utilisant aussi le module de r duction des figures on peut g n rer une version optimis e de la description fonctionnelle et de la description temporelle d un circuit A titre d exemples on a r ussi r duire l architecture abstraite compl te de la m moire SPSMALL de 3 mots de 2 bits resp la m moire SPSMALL de 1 mots de 2 bits SPSMALL 3x2 resp SPSMALL 1x2 qu constitu de 92 blocs combinatoires et s quentiels resp 72 blocs en 62 blocs resp 50 blocs e L analyse instanci e sur les param tres simuler l analyse param tr e avec UPPAAL pour r duire les temps de setup des signaux d entr e du circuit en utilisant le model checker d UPPAAL e G n ration de f
30. l affectation du signal s avec la valeur de l valuation de la fonction bool enne fi e Cette affectation aura lieu si la condition gi est satisfaite et tous les autres conditions gk tel que k lt i sont fausses Cette repr sentation est mod lis e par un produit de n automates connect s avec des variables auxiliaires gi repr sentant les valeurs de v rit de leur garde correspondante Le syst me est compos de n automate TA gi qui value chaque garde gi et un automate TA s qui affecte le signal s L valuation de chaque grade gi est repr sent e par un automate TA gi pr sent sur la figure 2 Cet automate contient deux locations l tat stable stable gi dont la valeur de la garde est conforme aux valeurs des signaux de l ensemble e correspond la valeur instantan e de la garde soit vraie soit fausse l tat actif active gi de d lai nul vers lequel auquel on transite via les transitions de l ensemble lt g gt de l tat stable stable gi chaque fois qu il y a un front sur l un des signaux de l ensemble e qui induit un changement sur la valeur de la garde gi Le changement de la variable auxiliaire Ver vgi vgi repr sentant la garde gi dans le mod le est effectu dans l action des deux transitions uniques et urgentes les transitions de l ensemble lt g gt sortante de l tat actif active gi vers l tat stable stable gi l une est associ a la valeur vraie et l autre est associ e la v
31. mmande est presque le m me que celui du mode pr c dent vhdl2ta lt vhld file gt env env file temp lt temp file gt temp file mode sim out testbench file sim options options Comme on peut le voir la plupart des param tres pass s dans cette commande sont d crits pr c demment Il reste savoir que dans ce mode on passe en param tre de l option out le nom du fichier testbench qui constitue avec les autres fichiers VHDL d crivant la partie fonctionnelle et temporelle des portes du circuit le programme pr t simuler Tous les fichiers vhd g n r s sont dans le m me r pertoire courant que celui du fichier testbench Les autres options ta_sim sp cifiques pour ce mode sont sim version abr g simv il existe deux versions des programmes VHDL pr ts simuler qu on peut g n rer avec l outil VHDL2TA 1 la premi re version dans laquelle on associe un seul composant pour tout le circuit le programme n est constitu que deux fichiers 2 la deuxi me version dans laquelle un composant VHDL est associ pour chaque porte du circuit en d crivant sa fonctionnalit et ses annotations temporelles en cons quence le programme est constitu d un fichier testbench et de plusieurs fichiers VHDL Par d faut l option prend la valeur gate 16 32 repr sentant la deuxi me version A titre d indication la premi re version est repr sent e par la valeur circuit sim format abr g a simf in
32. mode permet de g n rer une description fonctionnelle et une description temporelle optimis es partir de la description en VHDL initiale et de la description temporelle initiale 4 3 1 Mod le d automates temporis s Ce mode permet de g n rer le mod le d automates temporis s en descriptions d entr e des outils tels que UPPAAL Hytech ou IMITATOR 2 partir de la description fonctionnelle en VHDL et ventuellement de la description temporelle du circuit et de l environnement des signaux d entr e du circuit La syntaxe de la commande qu on passe sur l outil est donn e comme suit vhdl2ta lt vhld_file gt env lt env_file gt temp lt temp file gt temp type mode tal out lt ta_file gt ta options options Les param tres pass s dans cette commande vhdl_ file le fichier VHDL qui d crit la fonctionnalit du circuit Ce param tre est toujours obligatoire temp abr g t c est l option qui permet de d crire la partie temporelle du circuit Elle prend en param tre le fichier temporel temp_ file et son type temp_ type 1 s il s agit d un mod le temporel complet 2 s il s agit d un mod le temporel bi bounded delay Par d faut les d lais des portes sont nuls si cette option n est pas sp cifi e On peut mettre t la place de temp dans la commande env abr g e cette option d crit l environnement du circuit Elle permet de fournir le fichier d environnement env_file Par d fa
33. nctionnalit et les propri t s temporelles de leurs circuits en comblant l cart entre les mod les de circuits con us et d crits en VHDL et l efficacit des outils de model checking temporis s Cette approche peut tre aussi employ e pour acc l rer la simulation temporelle des circuits complexes et la rendre plus pr cise en partant de la description au un niveau transistor et de la simulation lectrique pour passer un niveau de simulation RTL Le mod le au niveau transistor de chaque porte est n cessaire pour caract riser les d lais appropri s Une fois que le d lai de chaque porte est extrait la simulation de tout le syst me est effectu e au niveau logique 24 32 R f rences A 09 E Andr IMITATOR A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata In Martin Leucker and Carroll Morgan eds ICTAC 09 LNCS 5684 pages 336 342 Springer 2009 A 10 E Andr IMITATOR II A Tool for Solving the Good Parameters Problem in Timed Automata In Yu Fang Chen and Ahmed Rezine eds INFINITY 10 Electronic Proceedings in Theoretical Computer Science 39 pages 91 99 2010 AD 94 R Alur and D L Dill A Theory of Timed Automata TCS 126 2 183 235 1994 ACEF 09 E Andr T Chatain E Encrenaz L Fribourg An inverse method for parametric timed automata International Journal of foundations of Computer Sciences vol 20 no 5 pages 819 836 World Scientific Publishing Company AEF
34. on de ce manuel pr sente le mod le temporel adopt pour repr senter la fois la partie fonctionnelle et la partie temporelle des circuits ainsi que les principes de traduction que l outil VHDL2TA impl mente La section 3 d crit l architecture de l outil et ses caract ristiques Dans la section 4 on pr sente le mode d installation et d emploi de l outil La section 5 est consacr e la pr sentation de quelques exemples de tests de circuits en utilisant l outil VHDL2TA pour g n rer le mod le temporel les outils de model checking UPPAAL ou Hy Tech pour v rifier le mod le temporel et l outil de synth se de contraintes temporelles IMITATOR 2 pour synth tiser des contraintes sur les param tres de d lais qui assurent toujours le bon fonctionnement du syst me La section 6 conclue ce document Les annexes ajoutent des pr cisions techniques L annexe A d crit le code source des descriptions de sortie de quelques exemples de circuits vus dans la sections l annexe B les grammaires des descriptions d entr e de l outil VHDL2TA 3 32 2 Traduction automatique en automates temporis s des circuits d crits en VHDL avec des d lais Apr s une br ve pr sentation du formalisme d automates temporis s on d crira le fragment VHDL et le mod le de d lais consid r s pour repr senter respectivement la partie fonctionnelle et la partie temporelle du circuit analys On d crira ensuite l algorithme de traduction en commentant
35. ronts montants et descendants des signaux du circuit e 3x4 4x 1 locations des automates associ s aux portes du circuit les locations associ es aux automates d environnement La commande employ e pour g n rer cette description est mentionn e ci dessous VAS ESA abehevnG e VER Lacen eny aim larene EHET it ta O Vim Labo Ea star Up La propri t TCTL qui d crit le comportement du signal Q attendu suivant Q 1467 up 3467 down est donn e comme suit A t gt 0 and t lt 1467 or t gt 3467 imply a 0 and t gt 1467 and t lt 3467 imply aL Cette propri t TCTL est bien v rifi e par le mod le d automates temporis s d crit en Uppaaal Donc le temps de r ponse est bien conforme celui d crit dans la sp cification Nous notons que le temps de la v rification de cette propri t est inf rieur 0 1 sec et le temps de g n ration de la description en UPPAAL est inf rieur 0 1 sec 22 32 Comme on peut le constater dans ce test la valuation point Pi0 associ e aux valeurs des param tres de la sp cification est donn e comme suit Tur 1000 Tro 1000 THold 350 TSetup U Gwari T 219 not11 147 Nott 155 Snore 163 vac 147 xori 416 angit 80 Sandi 155 Lateht 240 Deuxi me test Nous avons refait un test identique au pr c dent mais cette fois avec un environnement plus simple qui satisfait les valeurs des param tres des signaux d entr e du point Pi0 L environn
36. s using timed automata In TPTS 02 ENTCS volume 65 2002 CEFX 06 R Chevallier E Encrenaz Tiphene L Fribourg W Xu Timing Analysis of an Embedded Memory SPSMALL WSEAS Transactions on Circuits and Systems vol 5 7 pp 973 978 2006 HHW 95 T A Henzinger P Ho and H Wong Toi A user guide to HyTech In TACAS pages 41 71 1995 LBG 98 Lester Anthony Bazargan Sabet Pirouz and Greiner Alain Yagle a second generation functional abstractor for cmos vlsi circuits In 10th International Conference on Microelectronics pages 265 268 Monastir Tunisia December 1998 LPY 97 K Larsen P Pettersson and W Yi UPPAAL in a Nutshell International Journal on Software Tools for Technology Transfer 1 134 152 1997 MP 95 O Maler and A Pnueli Timing analysis of asynchronous circuits using timed automata In Int conf on Correct Hardware Design and Verification Methods CHARME volume 987 pages 189 205 Springer 1995 Y 97 S Yovine Kronos A Verification Tool for Real Time Systems International Journal on Software Tools for Technology Transfer 1 123 134 1997 26 32 A Exemples de circuits A 1 Le mod le d automates temporis s d crit en UPPAAL du circuit n_xor YP et ee tes DESC ripe Lor du SyS TOE eae SS SoS eS x nm nn A SS SS nn nn a a Se See Definition des variables globales du systeme horloges discretes param tres ee a alg NN E E E E E E T ee ee ee ee ee clock Ey xX S in
37. signal time_front_up time_front_dn time_front_dn time dn time time up time_front_up time up time time dn signal VADLID time NUMBER up up UP dn down DOWN dn DN B 2 2 La grammaire du deuxi me modele Grammaire A fichier principal temp_file temp_signals temp_signals temp_signals temp_signal temp_signal temp_signal signal timing_file_signal 30 32 signal VADLID timing_file_signal FILE NAME Grammaire B fichier de timing de portes time_file sorties sorties sorties sortie sortie sortie param configurations param signals_in out_in TIME signals_in signal signals_in signal configurations configuration configurations configuration configuration n_io time nio n_iotiolio io 0 1 l ldnlup signal VADLID time NUMBER up u l U dn d l D B 3 La grammaire des descriptions d environnement env_file type_env behaviors_env type_env CYCLIC AUTOMATON ENVIRONMENT AUTOMATON CYCLIC ENVIRONMENT AUTOMATA ENVIRONMENT behaviors_env clock_def signals_behavior clock_def CLOCK signal WITH THI time TLO time INVERSE NCYCLES ENTIER signals_behavior signal_behavior signals_behavior signal_behavior signal_behavior signal time_fronts signal value 3 time_fronts time_front time_fronts time_front
38. ssus la partie temporelle du circuit d lais des portes d crit les d lais de propagation des fronts sur la sortie des portes du circuit Il existe deux types de descriptions 1 les descriptions donn es sous forme d un fichier dans lequel deux intervalles de d lais sont associ s chaque porte mod le temporel bi bounded delay 2 les descriptions dans lesquelles on associe un fichier de timing configuration front sortie temps pour chaque porte mod le STG complet On leur ajoute aussi un fichier principal dans lequel on associe chaque porte le nom chemin du fichier de timing correspondant On note que dans ce mod le les descriptions sont repr sent es par ces fichiers principaux L environnement du circuit Fichier d environnement d crit le comportement des signaux d entr e L outil VHDL2TA g n re ensuite le mod le d automates temporis s associ au circuit en description d entr e d un outil d analyse tel que UPPAAL HyTech ou IMITATOR 2 Dans certains cas on passe aussi des sp cifications en UPPAAL d crivant des propri t s temporelles du circuit analyser afin de les v rifier en employant le model check d UPPAAL Les sp cifications en UPPAAL sont d crites en logique temporelle TCTL Les propri t s qu on peut exprimer g n ralement dans les sp cifications UPPAAL sont les propri t s d accessibilit de suret et d quit 10 32 3 3 Fonctionnalit s de l outil e Traduction des circu
39. statement_part if_statement if_statement IF if_statement_ END IF if_statement_ condition THEN signal_assignment_statement ELSIF if_statement_ condition THEN signal_assignment_statement condition THEN signal_assignment_statement ELSE signal_assignment_statement 3 condition guard_exprl guard_exprl guard_expr guard_expr op2 guard_expr guard_expr VHDLID EQ BITVALUE T guard_expr op2 guard_expr NOT guard_expr 29 32 T guard_expr signals_names_list signal_name signals_names_list signal_name process_label VHDLID signal_name VHDLID op2 AND I ORI XOR B 2 La grammaire des descriptions temporelles Comme on a vu auparavant il existe deux types de descriptions temporelles que l outil VHDL2TA prend en entr e 1 les descriptions d intervalles des d lais associ s chaque porte du circuit mod liser donn sous forme d un fichier 2 Les descriptions dans lesquelles on associe un fichier de timing configuration front sortie temps pour chaque porte du circuit Ces fichiers sont accessibles via les informations mentionn es dans un fichier principal repr sentant de la description temporelle Ci dessous on pr sente les deux grammaires associ es ces deux mod les B 2 1 La grammaire du premier mod le temp file delay_signals delay_signals delay_signal delay_signals delay_ signal delay_signal signal time_front_dn time_front_up
40. t t d velopp s dans cette discipline tels que les outils UPPAAL et KRONOS Y 97 qui effectuent la v rification automatique des propri t s temporelles exprim es dans la logique TCTL l outil HyTech qui permet l analyse d accessibilit et l outil IMITATOR et IMITATOR 2 qui permet de synth tiser des contraintes lin aires sur des param tres temporelles qui assurent le bon fonctionnement du syst me analys 2 2 Le mod le fonctionnel d crit en VHDL et le mod le temporel Les programmes VHDL repr sentent la partie fonctionnelle du circuit analyser On prend en consid ration les descriptions Data Flow constitu s d affectations concurrentes d finissant les blocs combinatoires et des processus d finissant les blocs s quentiels latchs points m moires ou buffers Chaque instruction concurrente permet d affecter une nouvelle valeur au signal de sortie du bloc correspondant Les informations temporelles partie temporelle du circuit analyser sont dissoci es de la description VHDL on associe chaque bloc deux intervalles de d lais de propagation des fronts montants et descendants de son signal de sortie Ces intervalles de d lais sont parfois extraits des tables de timing associ es aux blocs du circuit analyser C est le cas de l architecture de la m moire SPSMALL CEFX 06 Cette derni re est une architecture compl te abstraite par le LIP6 dans le cadre du projet ANR VALMEM en utilisant l outil d abstraction
41. t e L RS e 2 0 Sr nL const ine delta 1 s iy delta us gt deltel 1s 3 deltal t S 24 broadcast chan e 1 down e 1 up e 2 down e 2 up s down S up les automates de l environnement qui d finissent les signaux d entr e process env nd signals L state env nd signals 0 t lt 5 envy nd sighals LAE lt 10 envy nda Signals Ze Le doy env nd signals gt lt 20 env nd sig els end ftirue init env nd signals 0 trans env nd Signals 0 gt env nd Signals Led ual Ts ST Syne e d ul assTon se Lil Jy env nd signals 1 gt env nd signals 2 4 guard t 10 sync e 2 up assign e 2 1 Ju envy ndesignele 2 envy md signals 3 Guard 1 o sync e l down assign e l 07 To eny nd signals 9 gt env nd signals end guard t 207 syne 2 down assigne 25 07 7 les automates qui d finissent tous les signaux auxiliaires et les signaux de sortie A A AAA A A A A SS SS les automates qui d finissent le signal s process Ass s state L x0 s x s lt delta0 u s 1 x1 s x s lt deltal u s 1 f s true init ors a trans l1 x0 s gt 1 x0 s guard e 1 0 sync e 1 down T L x0 s gt 1 x0 s guard e 1 1 sync e 1 up de L x0 s gt 1 x1 s guard e 1 1 0 and e 2 sync e 1 down assign x s 0 L x0 s gt 1 x1 s guard e 1 1 1 and e 2 sync e 1 up
42. ta n_xor vhd e n_xor env t n_xor tmp 2 m ta o n_xor ta taf upl g n re le mod le d automates temporis s associ la porte n_xor d crit en format UPPAAL dans le fichier n_xor ta Cette description en UPPAAL est d crite dans l annexe A 1 La commande vhdl2ta d flip flop vhd e d_ flip flop env t d flip flop tmp 2 m ta o d_ flip flop imi taf imi2 inversemethod g n re le mod le d automates temporis s d crit dans le fichier imi et une valuation de r f rence Pi0 d crite dans le fichier de r f rence pi0 Avec ces deux fichiers on peut appeler IMITATOR 2 en mode inversemethod la m thode inverse afin de g n rer le syst me de contraintes lin aires sur les param tres de d lais dont les valuations assurent le m me fonctionnement que celui de la valuation de r f rence Pi0 La commande vhdl2ta sp _3x2 vhd e sp 3x2 env t sp 3x2 tmp 2 m ta o sp 3x2 opt ta taf upl fo g n re une description en UPPAAL partir de la figure optimis e La description 18 32 g n r e contient 30 automates de moins que la description en UPPAL g n r e sans utiliser cette option Donc avec cette option on obtient des mod les optimis s La commande vhdl2ta sp _ 3x2 vhd t sp 3x2 tmp 2 m vhdl opt o sp 3x2 vhld_ opt vhd g n re une version optimis e d une description fonctionnelle et temporelle de l architecture abstraite de la m moire SPSMALL En utilisant ce mode cette derni re est r duite de 92 62 portes
43. tes temporis s des circuits d crits en VHDL avec des d lais 2 1 Le modele de base d automates temporis s 2 2 Le mod le fonctionnel d crit en VHDL et le mod le temporel 2 3 L algorithme de traduction 3 Impl mentation VHDL2TA 3 1 Architecture et impl mentation 3 2 Les descriptions d entr e et sortie 3 3 Fonctionnalit s de l outil 4 Mode d emploi de VHDL2T A 4 1 Installation 4 2 Les descriptions d entr e de VHDL2T A 4 3 Les commandes d appel de VHDL2TA 5 Exemples de tests Circuit Valmem latch 6 Remarques finales R f rences A Exemples de circuits B Les grammaires des descriptions d entr e de VHDL2TA 2 32 1 Introduction Ces travaux concernent la v rification de circuits num riques temporis s Ces circuits sont compos s de portes logiques auxquelles des d lais de propagation de fronts sont associ s L analyse de tels circuits permet de prouver des propri t s temporelles complexes telles que identifier les chemins critiques ajuster la p riode d horloge du circuit analys ou d terminer la p riode de stabilit des signaux d entr es sorties Ces circuits sont repr sent s la fois par un mod le fonctionnel d crit en VHDL et par un mod le temporel qui associe chaque bloc fonctionnel des d lais de propagation Afin de l analyser ce mod le est traduit dans le formalisme d automates temporis s dans lequel les techniques de simulation classique et de v rification par model checking p
44. timing associ s aux portes de circuits Dans ce mode il est indispensable d indiquer le mode configs_check qu on passe en param tre dans l option temp_mode La syntaxe de la commande qu on passe dans ce mode est donn e ci dessous On note que dans les deux modes pr c dents l option temp_mode prend en param tres les deux valeurs timing files et delay_file respectivement vhdl2ta lt vhld file gt temp lt temp file gt 2 mode temp out lt temp checked file gt temp mode configs check options Dans le premier mode on peut employer l option temp_select abr g ts avec laquelle on peut sp cifier les criteres de s lection des d lais des configurations sur un intervalle de d lais Les crit res de s lection que cette option peut prendre en param tre sont list s ci dessous e min s lectionner les bornes inf rieures des intervalles des d lais associ es aux portes e max s lectionner les bornes sup rieures e moy s lectionner les valeurs moyens leur partie enti re sup rieure des bornes des intervalles e random s lectionner des d lais al atoire dans les intervalles des d lais c est la valeur que temp_select prend par d faut On note que cette option peut tre employ e dans le mode d emploi de l outil VHDL2TA sim quand l option temp prend des fichiers temporelles de type 2 fichiers de d lais 17 32 D autre part pour avoir des fichiers de timing avec des d lais nuls pour toutes les config
45. u fichier de d lais sp_3x2_delays tmp Les d lais des configurations sur les intervalles de d lais sont s lectionn s d une mani re al atoire La commande vhdl2ta n xor vhd e n Xor env t n Xor timing tmp 1 m sim o n_xor_testbench vhd g n re le programme VHDL pr t simuler dont le fichier testbench est nomm n_xor_testbench vhd 19 32 5 Exemple de tests Dans cette section on pr sente un exemple de tests pour l outil VHDL2TA L int gralit des tests d roul s sur divers circuits est synth tis e dans BE 1 1b Circuit Valmem latch Dans cette partie nous effectuons quelques tests sur le circuit latch tudi dans le cadre du projet VALMEM AEF 09 AEF 08 Le circuit et la description des param tres de sa sp cification les temps de setup Tsetup et de hold Thold du signal d entr e D la dur e du front montant THI de l horloge CK la dur e du front descendant TLO de l horloge CK et le temps de r ponse TCK gt Q sont donn s sur la figure 5 extraite de AEF 08 a b Figure 5 a Le circuit valmem latch b la sp cification du circuit L impl mentation du circuit en VHDL est donn e comme suit ENTITY valmen tetch 15 PORT g Out BIT ck gt in BIT d gt 1n BIT l3 END valmem latch ARCHITECTURE RIL OF Valmem latch IS SIGNAL notl BIT SIGNAL not2 BIT SIGNAL xorl BIT SIGNAL andl BIT BEGIN notl lt not ck not2 lt not notl xOrl lt not2 xor ck an
46. urations 1l suffit d omettre l option temp On note que l option temp_mode abr g tm prend par d faut la valeur delay _ file si le type du fichier pass dans l option temp est gal 1 la valeur timing files si le type est gal 2 4 3 4 Optimisation VHDL Dans ce mode l outil VHDL2TA prend en entr e la description comportementale en VHDL du circuit optimiser et ventuellement sa description temporelle sous forme d un fichier d intervalle de d lais ensuite il g n re la version optimis e de ses descriptions La syntaxe de la commande employ e dans ce mode est donn e comme suit vhdl2ta lt vhld file gt temp temp file temp type mode vhdl opt Fout lt vhdl file gt lt temp file gt options Comme on peut le constater cette commande peut prendre en param tres les noms des deux descriptions fonctionnelles et temporelles simultan ment 4 3 5 Options g n rales On distingue deux classes d options des options sp cifiques un mode donn qu on vient de voir ci dessus et des options g n rales qui peuvent tre employ es dans tous les modes Ces derni res sont donn es comme suit mode par d faut ta comme c est d j indiqu auparavant c est le mode d emploi de VHDL2TA debug abr g d cette option permet de donner des informations de debogage warning abr g w cette option permet d afficher les warnings 4 3 6 Exemples d Appels La commande vhdl2
47. ut le comportement des signaux d entr e du circuit est stable la valeur 0 si cette option n est pas pass e en param tres de la commande vhdl2ta mode abr g m mode d emploi de VHDL2TA Dans ce mode d emploi il prend la valeur ta On note que cette option prend par d faut cette derni re valeur Donc il n est pas obligatoire de la sp cifier dans ce mode Voici les valeurs que l option mode prend dans tous les modes d emploi de VHDL 14 32 e ta mod le d automates temporis s voir section 4 3 1 e sim programme VHDL temporis pr t simuler voir section 4 3 2 e temp mod le temporelle voir section 4 3 3 e vhdl_ opt optimisation VHDL voir section 4 3 4 out abr g 0 cette option permet de passer en param tre le nom de la description de sortie Par d faut le nom de la description prend le m me nom que celle de la description en VHDL en changeant l extension vhd par l extension de la description de sortie ex Hytech hy UPPAAL ta e ele Les autres options ta_options sp cifiques pour ce mode sont ta_format abr g taf indique le format de la description g n rer Les param tres que l option peut prendre sont e hy s l s agit d une description en format HyTech e upl s il s agit d une description en format UPPAAL e imi s il s agit d une description en format IMITATOR e imi2 s il s agit d une description en format IMITATOR 2 L option ta_ format pren
48. xor est donn ci dessous On peut remarquer que le premier modele modele temporel bi bounded delay est une abstraction de ce dernier modele 12 32 Delar pour chaque configuration MZ EMS a ZAS 3ns 2ns 3ns Ins 4ns Ins 4ns SOQOPPOECGSSOO D eec O C0 C0 Q C cac 10 5 0 C Dans ce mod le une phase d abstraction de d lais introduite dans l outil est n cessaire pour extraire pour chaque porte du circuit deux intervalles de d lais abstractions de d lais associ s aux fronts montants et descendants propag s sur la sortie de la porte partir de son fichier de timing 4 2 3 La description d environnement est donn e sous forme d un fichier qui contient une liste de comportements associ s aux signaux d entr e du circuit mod liser Un comportement d un signal est une suite altern e de fronts montants et descendants des instants croissants ou intervalle d instants La syntaxe des descriptions d environnement est d crite par une grammaire g n ratrice donn e dans l annexe B 3 Voici un exemple de description d environnement des signaux d entr e de la porte n_xor et HAN el To Up do GOWN 6 2 10 up 20 down 4 2 4 Fichier des propri t s TCTL contient les comportements des signaux de sortie qui sont exprim s en propri t s de la logique TCTL afin d effectuer le model checking avec UPPAAL Le but est de v rifier si le mod le d automates g n r satisfait ces propri t s Dans l exemple
Download Pdf Manuals
Related Search