Abstract
VHDL/S blends four different and self-contained linguistic paradigms: VHDL, state based specifications, timing diagrams, and temporal logic (figure 1.1) This is achieved by a stream based semantics that uniformly underlies all parts of the language. As a result, the designer who uses VHDL/S can switch back and forth between the paradigms without changing his pragmatic conceptual understanding of reactive behaviour in time. This approach is explained in detail in (J. Helbig et al. 1993).
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
J. Helbig, R. Schlör, W. Damm, G. Döhmen, and P. Kelb. (1993): VHDL/S-integrating Statecharts, timing diagrams, and VHDL. Microprocessing and Microprogramming 38, pages 571–580.
D. Harel (1987): StateCharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8.
E.M. Clarke, E.A. Emerson, and A.P. Sistla (1986): Automatic verification of finite-state concurrent systems using temporal logic. ACM Trans. on Programming Languages and Systems, 8:244–263.
B. Josko (1993): Modular specification and verification of reactive systems. Habilitationsschrift, University of Oldenburg.
Z. Manna and A. Pnueli (1982): Verification of concurrent programs: The temporal framework. In R. S. Boyer and J. S. Moore, editors, Correctness Problems in Computer Science, chapter 5, pages 215–273. Academic Press.
J.R. Burch, E.M. Clarke. K.L. McMillan, D.L. Dill, and J. Hwang (1990): Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logics in Computer Science, pages 428–439, June.
J. R. Armstrong (1988): Chip-level Modeling with VHDL. Prentice-Hall, New York.
W. Damm, B. Josko, and R. Schlör (1995): Specification and verification of VHDL-based system-level hardware designs. In E. Börger, editor, Specification and validation methods. Oxford University Press, pages 331–341.
M. Fujita and H. Fujisawa (1990): Specification, verification and synthesis of control circuits with propositional temporal logic. In J.A. Darringer and F.J. Rammig, editors, Computer Hardware Description Languages and their Applications, pages 265–279. Elsevier Science Publishers B.V..
G. Boriello (1992): Formalized timing diagrams. In Proceedings, The European Conference on Design Automation, pages 372–377, Brussels, Belgium, March.
Ph. Moeschier, H.P. Amann, and F. Pellandini (1993): High-level modelling using extended timing diagrams. In proceedings of EURO-DAC’93, pages 494–499, September.
K. Khordoc, M. Dufresne, E. Cerny, P. Babkine, and A. Silburt (1993): Integrating behavior and timing in executable specifications. In Conference on Hardware Description Languages and their Applications, pages 385–402. OCRI Publications, April.
G. v. Bochmann (1993): Specification languages for communication protocols. In Conference on Hardware Description Languages and their Applications, pages 365–382. OCRI Publications, April.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 ECSC-EC-EAEC, Brussels-Luxembourg
About this chapter
Cite this chapter
Damm, W. et al. (1997). Specification Languages. In: Kloos, C.D., Damm, W. (eds) Practical Formal Methods for Hardware Design. Research Reports Esprit. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-60641-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-60641-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62007-5
Online ISBN: 978-3-642-60641-0
eBook Packages: Springer Book Archive