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 qui sont décrits dans le langage de description de l'outil UPPAAL ou de l'outil HyTech.
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. Cet outil est disponible en téléchargement sur le lien ci-dessous [à venir].
Pour l'utilisation de VHDL2TA, veuillez vous référer au guide d'utilisation [à venir].
Pour toute information, n'hésitez pas à contacter Abdelrezzak Bara.
Ces études de circuits sont synthétisées dans [à venir]. Pour chaque exemple du circuit, nous donnons dans le tableau ci-dessous :
la référence de l'article dans lequel le circuit est présenté.
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 UPPAAL générée.
fichier des propriétés à vérifier par l'outil UPPAAL.
les détails des tests effectués.
|
|
Références |
Fichiers |
Expériences |
|---|---|---|---|
|
and-or |
|||
|
chu150 |
|||
|
converta |
|||
|
desynch |
|||
|
D flip-flop |
|||
|
half |
|||
|
mp-for-pkt |
|||
|
porte Muller |
|
||
|
qr42 |
|||
|
rcv-setup |
|||
|
rpdft |
|||
|
sbuf-read-ctl |
|||
|
sbuf-send-ctl |
|||
|
trigger |
|||
|
spsmall-blueb-lsv1 |
|||
|
spsmall-blueb-lsv2 |
03 novembre 2009 : Transformation automatique de description VHDL en automates temporisés (Reunion VALMEM).
|
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. |
|
|
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). |
|
|
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. Clariso 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. Clariso 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. |
|
|
R. Clariso. Abstract Interpretation Techniques for the Verification of Timed Systems. PhD Thesis, Department of Software (LSI), Technical University of Catalonia (UPC). September 2005. |
|
|
C. 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. Pena. 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 24 fevrier 2009.