Abstract
The FORMAT-project aims at a verification environment for VHDL-based hardware design, employing two major state-of-the-art verification methods: (1) (compositional) symbolic model checking (SMC), and (2) interactive theorem proving, supported by automatic verification tools for finite-state subtasks.
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
W. Damm, B. Josko, and R. Schlör (1993): A net-based semantics for VHDL. In EURO-DAC’93/EURO-VHDL’93. IEEE CS Press, pages 514–519.
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–410.
M. Francis, S. Finn, E. Mayger, and R.B. Hughes (1993): Reference manual for the LAMBDA system, Version 4.2. Technical report, Abstract Hardware Limited.
Nick Chapman (1994): Translating VHDL into L2. Technical report, Abstract Hardware Limited.
G. Döhmen and R. Herrmann (1995): A deterministic finite-state model for VHDL. In Formal Semantics for VHDL. Kluwer Academic Publisher.
G. Döhmen, R. Herrmann, and H. Pargmann (1995): Translating VHDL into functional symbolic finite-state models. Formal Methods in System Design, 7:125–148.
W. Damm, B. Josko, and R. Schlör (1993): A net-based semantics for VHDL. In EVRO-DAC’93/EVRG-VEDL’93. IEEE CS Press, pages 514–519.
G. Döhmen (1994): Petri nets as intermediate representation beween VHDL and symbolic transition systems. In EURO-VHDL’94, Grenoble, France, September.
R. Herrmann and H. Pargmann (1994): Compiling VHDL data types into BDDs. Technical Report, OFFIS, Germany.
H. Pargmann and R. Herrmann (1995): Reduced Symbolic Transition Systems for VHDL. In Proceedings GI/ITG Workshop, Passau.
G. Kutty, Y.S. Ramakrishna, L.E. Moser, L.K. Dillon, and P.M. Melliar-Smith (1993): A graphical interval logic toolset for verifying concurrent systems. In 5th International Conference on Computer Aided Verification, pages 123–137, June 1993.
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., Döhmen, G., Herrmann, R., Kelb, P., Pargmann, H., Schlör, R. (1997). Verification Flow. 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_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-60641-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62007-5
Online ISBN: 978-3-642-60641-0
eBook Packages: Springer Book Archive