Tests de l'architecture abstraite spsmall-blueb-lsv2

1. Architecture complète abstraite SPSMALL-BLUEB-LSV2

On reprend l'architecture présentée dans [Xu06] qui est une extension de l'architecture SPSMALL-BLUEB-LSV avec deux points mémoires. Son graphe AFTG associé à l'implémentation SP1 ce dette architecture est donné sur la figure 1. Le graphe AFTG de l'imlémentation SP2 est identique à celui de SP1 en terme de fonctionnalité. En revanche, les délais de propagation de leurs composants peuvent être différents.

Nous allons présenté ci-dessous les résultats de tests obtenus en utilisant les modèles d'automates temporisés (représentant le modèle AFTG) décrits en format d'UPPAAL générés par l'outil VHDL2TA ; et de les comparer par rapport à ceux qui sont décrits dans [CEFX06].

2. Analyse instanciée

2.1. Descriptions d'entrée sortie

• Dans le tableau présenté ci-dessous, nous présentons l'ensemble des descriptions d'entrée sortie de l'outil VHDL2TA employées dans les tests effectués sur l'architecture spsmall-blueb-lsv2. Les détails des tests sont donnés dans exp-spsmall-blueb-lsv2.
  
  

  Tests	VHDL	Délais	Env	HyTech	IMITATOR-2	UPPAAL	Propriétés TCTL
  test 1	spsmall-blueb-lsv2.vhd	SP1.temp	spsmall-blueb-lsv2.env	spsmall-blueb-lsv2.hy	spsmall-blueb-lsv2.imi	spsmall-blueb-lsv2.ta	spsmall-blueb-lsv2.q
  test 2	"	SP2.temp	spsmall-blueb-lsv2.env	spsmall-blueb-lsv2.hy	spsmall-blueb-lsv2.imi	spsmall-blueb-lsv2.ta	spsmall-blueb-lsv2.q

  
  

• A titre d'exemple, les descriptions en UPPAAL, en HyTech et en IMITATOR-2 du premier test sont générées en utilisant, respectivement, les commandes présentées ci-dessous :

  • vhdl2ta lsv2.vhd -e env1.env -t delay.temp 2 -m ta -o lsv2.ta -taf upl

  • vhdl2ta lsv2.vhd -e env1.env -t delay.temp 2 -m ta -o lsv2.hy -taf hy

  • vhdl2ta lsv2.vhd -e env1.env -t delay.temp 2 -m ta -o lsv2.imi -taf imi2

2.2. Résultats d'analyse

• Le tableau mentionné ci-dessous récapitule pour chaque test :

  • les résultats de model-checking des propriétés TCTL sur le modèle généré décrit en UPPAAL, en utilisant le model-checker d'UPPAAL.

  • l'analyse d'accessibilité en utilisant l'outil d'analyse HyTech sur le modèle décrit dans le langage de description de cet outil.

  • l'analyse d'accessibilité en utilisant l'outil de synthèse paramétrée IMITATOR-2 sur le modèle décrit dans le langage de description de cet outil, ainsi le format graphique du graphe d'atteignabilité (graphe de régions) produit par IMITATOR-2.

  
  

  Tests	Model-checking TCTL	analyse avec HyTech	analyse avec IMITATOR-2	graphe d'accessibilité
  test 1	MC-TCTL-1	RA-HY-1	RA-IMI2-1	Graphe-Region-1
  test 1	MC-TCTL-2	RA-HY-2	RA-IMI2-2	Graphe-Region-2

  
  

• Les analyses avec UPPAAL, HyTech et IMITATOR-2 dans ces tests ont été effectués en utilisant, respectivement, les commandes présentées ci-dessous :

  • verifyta lsv2.ta query.q

  • hytech lsv2.hy

  • IMITATOR lsv2.imi -mode reachability

3. Réduction des temps de setup

3.1. Descriptions d'entrée des outils d'analyse

• Dans le tableau présenté ci-dessous, on récapitule les descriptions en UPPAAL employées pour faire l'analyse paramétrée sur les temps de setup des signaux d'entrée de l'architecture abstraite. Nous avons attribué des modifications manuelles sur ces descriptions en remplaçant les valeurs des temps de setup associés aux signaux d'entrée par des constantes en UPPAAL.
  
  

  Tests	UPPAAL file	Propriétés TCTL
  test 1	lsv2-param.ta	lsv2-param.q
  test 2	lsv2-param.ta	lsv2-param.q

3.2. Résultats d'analyse

• Les propriétés TCTL dans ces tests sont bien vérifiées pour toutes les valeurs des temps :

  • t_setup^d ∈ {96, . . . , 108}, t_setup^wen ∈ {29, . . . , 48} et t_setup^a ∈ {34, . . . , 58} pour l'implémentation SP1. Le temps de réponse d'écriture de la valeur 1 (resp valeur 0) sur la sortie Q, T_CK→Q(W1) = 56 ≤ t_max^write = 56 (resp T_CK→Q(W0) = 55 < t_max^write); et le temps de réponse de la lecture de la valeur 1 (resp valeur 0) sur la sortie Q, T_CK→Q(R1) = 75 < t_max^read = 77 (resp T_CK→Q(R0) = 74 < t_max^read).

  • t_setup^d ∈ {229, . . . , 241}, t_setup^wen ∈ {55, . . . , 109} et t_setup^a ∈ {73, . . . , 110} pour l'implémentation SP2. Le temps de réponse d'écriture de la valeur 1 (resp valeur 0) sur la sortie Q, T_CK→Q(W1) = 136 < t_max^write = 142 (resp T_CK→Q(W0) = 141 < t_max^write); et le temps de réponse de la lecture de la valeur 1 (resp valeur 0) sur la sortie Q, T_CK→Q(R1) = 164 < t_max^read = 169 (resp T_CK→Q(R0) = 169 ≤ t_max^read).

• Le tableau présenté ci-dessous récapitule ces résultats de tests.
  
  

  Tests	Model-checking TCTL	Temps de setup
  test 1	MC-TCTL-PARAM-1	RD-T-SETUP-1
  test 2	MC-TCTL-PARAM-2	RD-T-SETUP-2

Remarque :

• Nous avons aussi obtenu les mêmes résultats de réduction des temps de setup des signaux d'entrée D, WEN et A que ceux obtenus avec les tests décrits précédemment. La réduction de ces temps de setup a été effectuée directement à partir des descriptions d'entrée (VHDL, temp, env) employées pour générer les descriptions en UPPAAL lors de la phase d'analyse instanciée (partie 2). En fait, nous avons passé en paramètre l'option -pa dans la commande vhdl2ta. Cette option permet d'effectuer l'analyse instanciée sur les paramètres des temps de setup des signaux d'entrée de l'architecture. La commande que nous avons passé sur l'outil VHDL2TA pour réduire les temps de setup dans le dernier test (test6) est donnée comme suit :

  • vhdl2ta lsv2.vhd -t delay.temp 2 -e env_ovc.env -m ta -o lsv2.ta -taf upl -pa query.q

• Le tableau présenté ci-dessous récapitule, pour chaque test, les descriptions en UPPAAL générées qui intègrent toutes les valeurs optimales des temps de setup réduits, les propriétés TCTL vérifiées, l'historique de la vérification (en utilisant l'outil VHDL2TA) avec le model-checker d'UPPAAL de ces propriétés et les valeurs des temps de setup des signaux d'entrée avec lesquelles ces dernières propriétés sont bien vérifiées.
  
  

  Tests	UPPAAL avec temps de setup réduits	Model-checking TCTL automatique	Temps de setup	Propriétés TCTL
  test 1	lsv2-param-auto.ta	MC-TCTL-PARAM-AUTO-1	RD-T-SETUP-AUTO-1	lsv2-param-auto.q
  test 2	lsv2-param-auto.ta	MC-TCTL-PARAM-AUTO-2	RD-T-SETUP-AUTO-2	lsv2-param-auto.q

4. Comparaison avec les résultats obtenus dans [CEFX06] & [Xu06]

Les résultats obtenus et leur comparaison avec ceux qui sont cités dans [CEFX06] et [Xu06], sont récapitulés dans les tables mentionnées ci-dessous. On note que l'unité de temps est de 10 ps.

4.1. Pour l'implémentation SP1

4.2. Pour l'implémentation SP2

Références