Abstract
Design verification is a major concern in the development of Systems-on-a-Chip for which abstract models are required. Standard HDL languages are not well suited for this task. We developed a method for specifying behavioral models of systems as seen from the interfaces — Hierarchical Annotated Action Diagrams, and provided it with formal semantics based on a timed process algebra. HAAD models can be compiled into behavioral VHDL processes that for verification by simulation. The original HAAD formalism had a number of modeling limitations. We describe here a modification in the composition rules of HAAD that gives more flexibility for modeling of pipeline behaviors. The composition is done on a port-by-port basis, by “stitching” together the end of one port behavior with the beginning of the next one, without awaiting the end of the entire enclosing action diagram as in the original method. The semantics of HAAD were formally specified and we established a mapping between the VHDL process generated by our software and the semantic rules.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. M. Andreescu-Hilohi, Axiomatisation d’un langage de description des chronogrammes (ACTC P), Thèse de maîtrise, Université de Montréal, in progress, 1999.
A. Tarnauceanu, Logiciel pour la vérification par simulation de la spécification de haut niveau de systèmes matériels, M.Sc. Thesis, Université de Montréal, 1997.
A.-F. Nicolae, Modèles et Algorithmes Pour La Simulation Des Systèmes A Temps Réel, M.Sc. Thèse de maîtrise, Université de Montréal, 1999.
S. Gandrabur, ACTC: Une algèbre de processus temporisée pour la spécification et vérification d’interfaces matérielles, Ph.D. thesis, Université de Montréal, 2000.
E. Cerny, B. Berkane, P. Girodias, K. Kordoc, Hierarchical Annotated Action Diagrams: An Interface-Oriented Specification and Verification Method, Kluwer Academic Publishers, 1998.
F. Jin, E. Cerny, H. Hulgaard, Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints, Formal Methods in CAD (FMCAD’98), Palo Alto, November 1998.
C. Delgado Kloos et W. Damm (Editors), Practical Formal Methods for Hardware Design, Project 6128, FORMAT, Volume 1, Springer, 1997.
G. Borriello, A New Interface Specification Methodology and its Application to Transducer Synthesis, PhD Thesis, University of California, Berkeley, 1988.
A.J. Daga, P.R. Suaris, Interface Timing Verification Drives System Design, ACM/ IEEE Design Automation Conf. (DAC’97), Anaheim, CA, June 1997.
T. Bolognese, E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, 14: pages 25–59, 1987.
J.A. Rowson, A. Sangiovanni-Vincentelli, Interface-Based Design, ACM/IEEE Design Automation Conf. (DAC’97), Anaheim, CA, June 1997.
F. Jin, E. Cerny, Verification of Real-Time Controllers against Timing Diagram Specifications using Constraint Logic Programming, IFIP EuroMICRO, Vasteras, August 1998.
G. D. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media New York
About this chapter
Cite this chapter
Nicolae, AF., Cerny, E. (2001). Port-Stitching: An Interface-Oriented Hardware Specification and VHDL Model Generation. In: Mermet, J. (eds) Electronic Chips & Systems Design Languages. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-3326-6_22
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3326-6_22
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-4884-7
Online ISBN: 978-1-4757-3326-6
eBook Packages: Springer Book Archive