127 | | * Décrire le comportement de la cellule inverseuse dans un fichier '''.vbe'''. |
128 | | * Dessiner le "stick-diagram" de l'inverseur inv_x1 dont le schéma en transistors est représenté. |
129 | | * Saisir sous '''GRAAL''' le dessin de la cellule en respectant le gabarit spécifié. |
130 | | * Valider les règles de dessin symbolique en lançant '''DRUC''' sous '''GRAAL'''. |
131 | | * Extraire la netlist de l'inverseur au format '''.al''' avec '''COUGAR'''. |
132 | | * Extraire le VHDL comportemental avec '''YAGLE'''. |
133 | | * Effectuer la preuve formelle entre le fichier '''.vbe''' extrait par '''YAGLE''' et le fichier '''.vbe''' de la spécification initiale. |
134 | | * Automatisez la vérification en écrivant un Makefile. |
| 124 | Pour chacune des deux cellules à réaliser, réaliser les étapes suivantes : |
136 | | == 5.2 Réalisation d'un Nand2 == |
| 126 | * Décrire le comportement de la cellule dans un fichier au format .vbe. |
| 127 | * Dessiner sur papier un stick-diagram. |
| 128 | * Saisir sous graal le dessin de la cellule en respectant le gabarit SXLIB . |
| 129 | * Valider les règles de dessin symbolique en lançant la commande DRUC sous graal. |
| 130 | * Utilisez la commande EQUI pour vérifier la connectivité des équipotentielles. |
| 131 | * Extraire la netlist de l'inverseur au format .spi avec cougar. |
| 132 | * Utiliser les outils yagle et proof pour vérifier le comportement. |
| 133 | * Créer un Makefile pour automatiser les différentes étapes. |
138 | | * Décrire le comportement de la cellule Nand à 2 entrées dans un fichier '''.vbe'''. |
139 | | * Dessiner le "stick-diagram" du Nand2 dont le schéma en transistors est représenté. |
140 | | * Saisir sous '''GRAAL''' le dessin de la cellule en respectant le gabarit spécifié. |
141 | | * Valider les règles de dessin symbolique en lançant '''DRUC''' sous '''GRAAL'''. |
142 | | * Extraire la netlist de la porte nand2 au format '''.al''' avec '''COUGAR'''. |
143 | | * Extraire le VHDL comportemental avec '''YAGLE'''. |
144 | | * Effectuer la preuve formelle entre le fichier '''.vbe''' extrait par '''YAGLE''' et le fichier '''.vbe''' de la spécification initiale. |
145 | | * Automatisez la vérification en écrivant un Makefile. |
| 135 | N'oubliez pas que les mans existent ... |
149 | | * Décrire le comportement de la cellule And à 2 entrées dans un fichier '''.vbe'''. |
150 | | * Dessiner le "stick-diagram" du And2. |
151 | | * Définir la hiérarchie à utiliser pour créer cette cellule. |
152 | | * Saisir sous '''GRAAL''' le dessin de la cellule en respectant le gabarit spécifié. |
153 | | * Valider les règles de dessin symbolique en lançant '''DRUC''' sous '''GRAAL'''. |
154 | | * Extraire la netlist de la porte nand2 au format '''.al''' avec '''COUGAR'''. |
155 | | * Extraire le VHDL comportemental avec '''YAGLE'''. |
156 | | * Effectuer la preuve formelle entre le fichier '''.vbe''' extrait par '''YAGLE''' et le fichier '''.vbe''' de la spécification initiale. |
157 | | * Automatisez la vérification en écrivant un Makefile. |
| 139 | Pour cette cellule, réaliser les étapes suivantes : |
159 | | = 6 Rapport = |
| 141 | * Décrire le comportement de la cellule dans un fichier au format .vbe. |
| 142 | * Dessiner sur papier un stick-diagram. '''Que constatez vous ?''' |
| 143 | * Saisir sous graal le dessin de la cellule en utilisant les 2 cellules précédemment crées. |
| 144 | * Valider les règles de dessin symbolique en lançant la commande DRUC sous graal. |
| 145 | * Utilisez la commande EQUI pour vérifier la connectivité des équipotentielles. |
| 146 | * Extraire la netlist de l'inverseur au format .spi avec cougar. |
| 147 | * Utiliser les outils yagle et proof pour vérifier le comportement. |
| 148 | * Créer un Makefile pour automatiser les différentes étapes. |
| 149 | |
| 150 | = 6 Compte rendu = |