VHDL2TA ( translation of VHDL Programs to Timed Automata ) est un outil de traduction des circuits numériques 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 ou IMITATOR-2.
L’outil VHDL2TA est développé par Abdelrezzak Bara en collaboration avec Emmanuelle Encrenaz et Pirouz Bazargan-Sabet.
VHDL2TA est développé en langage C, il emploie l'outil d'analyse syntaxique BISON. Le code bin de l'outil est disponible en téléchargement sur le lien ci-dessous [vhdl2ta].
Pour l’utilisation de VHDL2TA, veuillez vous référer au guide d'utilisation [user-manual].
Pour toute information, n’hésitez pas à contacter Abdelrezzak Bara.
Ces études de circuits sont synthétisées dans [circuits-studies]. Pour chaque exemple du circuit, nous donnons dans le tableau ci-dessous :
la référence de l'article dans lequel le circuit est tiré.
les détails des tests effectués.
l'ensemble des fichiers employés dans chaque test. Cet ensemble est constitué de :
fichier contenant la description du circuit en VHDL.
fichier des délais des portes du circuit.
fichier qui décrit le comportement des signaux d'entrée du circuit.
fichier de la description en HyTech générée.
fichier de la description en IMITATOR-2 générée.
fichier de la description en UPPAAL générée.
fichier des propriétés à vérifier par l'outil UPPAAL.
l'ensemble des fichiers contenant les résultats de tests obtenus, en employant les outils d'analyse sur les descriptions générées.
un document décrivant ces tests effectués.
Nom du circuit |
Références |
Tests effectués |
Document |
|---|---|---|---|
and-or |
|||
chu150 |
|||
converta |
|||
desynch |
|||
D-flip-flop |
|||
half |
|||
mp-for-pkt |
|||
porte Muller |
|||
qr42 |
|||
rcv-setup |
|||
rpdft |
|||
sbuf-read-ctl |
|||
sbuf-send-ctl |
|||
SR-latch1 |
|||
SR-latch2 |
|||
trigger |
|||
valmem_latch |
|||
spsmall-blueb-lsv1 |
|||
spsmall-blueb-lsv2 |
|||
spsmall-3x2 |
|
E, André, A. Bara, P. Bazargan-Sabet, R. Chevallier, E. Encrenaz, L. Fribourg, D. Le-Dû et P. Renault, Experiments of Prototype Tools on Case Studies, Comparison of obtained results and Conclusion, Délivrables D4.2 & D4.3 - Projet ANR VALMEM, Décembre 2010.. |
|
|
E.André, T. Chatain, E. Encrenaz, L. Fribourg, An Inverse Method for Parametric Timed Automata, 2nd International Workshop on Reachability Problems (RP'08), sept. 2008, U.K., Electronic Notes in Theoretical Computer Science (ENTCS) , 223, pages 29-46, Elsevier Sciences Publishers 2008. |
|
|
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. |
|
|
E. André, E. Encrenaz, L. Fribourg, Modèles d'automates temporisés pour l'analyse de circuits mémoire, Délivrable D3.1 - Projet ANR VALMEM, Janvier 2008.. |
|
|
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. |
|
|
P.A. Beerel, C.-T. Hsieh, S. Wadekar. Estimation of Energy Consumption in Speed-Independent Control Circuits, IEEE transactions on CAD, pp. 672-680. June, 1996. |
|
|
M.Bozga, H. Jianmin, O.Maler and S. Yovine, Verification of Asynchronous Circuits Using Timed Automata, In TPTS'02 Workshop, joint with ETAPS'02 Conference, Elsevier (2002). |
|
|
R.Clarisó. Abstract Interpretation Techniques for the Verification of Timed Systems. PhD Thesis, Department of Software (LSI), Technical University of Catalonia (UPC). September 2005. |
|
|
S.T.Chakradhar, S. Banerjee, R.K. Roy, Dhiraj Pradhan. Synthesis of initializable asynchronous circuits, IEEE transactions on Very Large Scale Integration (VLSI) Systems, 4 (2). ISSN 1063-8210 , pp. ISSN 1063-8210, pp. 254–263. 254-263. June 1996. |
|
|
R.Clarisó and J. Cortadella. Verification of timed circuits with symbolic delays. In Proc. Asia and South Pacific Design Automation Conference, pages 628-633. January 2004. |
|
|
R.Clarisó and J. Cortadella. Verification of concurrent systems with parametric delays using octahedra. In ACSD ’05. IEEE Computer Society, 2005. |
|
|
R.Chevallier, E. Encrenaz, L. Fribourg, W. Xu, Timing Analysis of an Embedded Memory: SPSMALL, WSEAS 10th international conference on circuits, july 2006, Greece. |
|
|
Nelson, C. Myers, and T. Yoneda, Efficient verification of hazard-freedom in gate-level timed asynchronous circuits, in IEEE transactions on CAD, 26(3): 592-605, March, 2007. |
|
|
D.L. Oliveira, M. Strum, and S. S. Sato, Burst-Mode Asynchronous Controllers on FPGA, International Journal of Reconfigurable Computing, vol. 2008, Article ID 926851, 10 pages, 2008. doi:10.1155/2008/926851. |
|
|
Simon L Peyton Jones. A practical technique for designing asynchronous nite-state machines. Technical report, Glasgow university, 1998. |
|
|
M.A. Peña. Relative timing based verification of concurrent systems. Department of Computer Architecture, Technical University of Catalonia, Barcelona, Spain, April 2003. |
|
|
N.Starodoubtsev, M. Goncharov, I. Klotchkov and A. Smirnov. Synthesis of asynchronous interface circuits by STG refinement. In: A. Yakovlev and R. Nouta (Eds.) Proceedings of Int. Workshop on Asynchronous Interfaces: Tools, techniques, and Implementations (AINT'2000), TU Delft, The Netherlands, July 2000, ISBN 90-5326-037-4, pp. 65-74. |
|
|
Hiroshi Saito, Alex Kondratyev, Jordi Cortadella, Luciano Lavagno, Alex Yakovlev, and Takashi Nanya, Design of Asynchronous Controllers with Delay Insensitive Interface, IEICE transaction, vol.E85-A, no.12, pp.2577-2585, December 2002. |
|
|
W.Xu, Timing Analysis of SPSMALL, internal report, june 06 . |
|
|
Peter Vanbekbergen, Albert Wang, Kurt Keutzer. A Design and Validation System for Asynchronous Circuits. 32nd ACM/IEEE Design Automation Conference DAC 1995: 725-730. |
Page maintenue par Abdelrezzak Bara.
Dernière modification en 25 féverier 2011.