Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

A flowgraph semantics of VHDL: Toward a VHDL verification workbench in HOL

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

VHDL-based verification methods require a formalized semantics of this hardware description language. As it has been shown recently that flowgraphs are an excellent means for defining the semantics of VHDL, we also use them to formalize full VHDL. However, our approach differs in important aspects from previous works. We use flowgraphs as an intermediate level for facilitating the deep embedding of VHDL in higher order logics, i.e. each VHDL program directly is a well-formed formula of the logic itself. This leads to a transparent semantic definition, since all constructs are defined explicitly as conservative extensions of the logic, and allows the direct reasoning about VHDL constructs. The relevant constructs of VHDL have been formalized, including delta delay. As we provide a general verification framework, different verification techniques such as model-checking, first-order theorem proving or invariant-based approaches may be used, depending on the verification task.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. B. Levy, I. Filippenko, L. Marcus, and T. Menas. Using the state delta verification system (SDVS) for hardware verification. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 337–360, Nijmegen, June 1992. IFIP TC10/WG 10.2, North-Holland.

  2. B.C. Brock, W.A. Hunt, and W.D. Young. Introduction to a formally defined hardware description language. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 3–35, Nijmegen, June 1992. IFIP TC10/WG 10.2, North-Holland.

  3. R. Camposano. Behavior-preserving transformations for high-level synthesis. In M. Leeser and G. Brown, editors,Proc. of Mathematical Sciences Institute Workshop: Specification, Verification and Synthesis: Mathematical Aspects, pages 106–128, July 1989.

  4. D. Borrione, L.V.Pierre, and A.M. Salem. Formal verification of VHDL descriptions in the Prevail environment.IEEE Design & Test of Computers, pages 42–55, June 1992.

  5. D. Boussebha, N. Giambiasi, and H. Magnier. Temporal verification of behavioral descriptions in VHDL. InEuropean Design Automation Conference, pages 692–697, Hamburg, Germany, 1992. IEEE.

  6. D. Eisenbiegler, K. Schneider, and r. Kumar. A functional approach for formalizing regular hardware structures. In J. J. Joyce and C-J. H. Seger, editors,Proc. of the International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, Canada, August, 11–13 1993. University of British Columbia, Springer, Lecture Notes in Computer Science No. 780.

  7. G. de Jong. verification of data flow graphs using temporal logic. InInternational Workshop on Applied Formal Methods for Correct VLSI Design, pages 169–178. IFIP WG 10.2/WG 10.5, North-Holland, 1990, 1989.

  8. D.E. Knuth and P.B. Bendix. Simple word problems in universal algebra.Computational algebra, 1:263–297, 1970.

    Google Scholar 

  9. D.J. Kinniment and A.M. Koelmans. Modelling and verification of timing conditions with the Boyer Moore prover. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 111–127, Nijmegen, June 1992. IFIP TC10/WG 10.2, North-Holland.

  10. G. Döhmen. Petri nets as intermediate representation beween VHDL and symbolic transition systems. InEURO-VHDL'94, Grenoble, France, September 1994.

  11. H. Eveking. Experience in designing formally verifiable HDL's. In D. Borrione and R. Waxman, editors,Computer Hardware Description Languages and their Applications, pages 321–334, Marseille, April 1991. IFIP WG 10.2, North-Holland.

  12. F. Feldbusch and R. Kumar. Verification of synthesized circuits at register transfer level. InProc. of 2nd European Design Automation Conference, pages 22–26, Amsterdam, Februar 1991.

  13. K.G.W. Goossens. Embedding a CHDDL in a proof system. LFCS Report Series ECS-LFC-91-155, University of Edinburgh, May 1991.

  14. A. Gupta. Formal hardware verification methods: A survey.Journal of Formal Methods in System Design, 1:151–238, 1992.

    Google Scholar 

  15. J. Helbig, R. Schlör, W. Damm, G. Döhmen, and P. Kelb. VHDL/S — integrating statecharts, timing diagrams, and VHDL.Microprocessing and Microprogramming, 38:571–580, 1993.

    Google Scholar 

  16. J. Van Tassel and D. Hemmendinger. Toward formal verification of VHDL specifications. InInternational Workshop on Applied Formal Methods for Correct VLSI Design, pages 409–418. IFIP WG 10.2/WG 10.5, North-Holland, 1990, 1989.

  17. J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors.Stepwise Refinement of Distributed Systems, volume 430 ofLecture Notes in Computer Science. Springer, REX Workshop, Mook, May/June 1989.

  18. K. Schneider, R. Kumar, and Th. Kropf. Alternative proof procedures for finite-state machines in a higherorder environment. In J. J. Joyce and C-J. H. Seger, editors,International Workshop on Higher-Order Logic Theorem Proving and its Applications, Vancouver, Canada, August, 11–13, 1993 1994.

  19. L. Lamport and M. Abadi. Composing specifications. Technical report, Digital Equipment Cooperation, 1990.

  20. L.M. Augustin, B.A. Gennart, Y.Huh, D.C. Luckham, and A.G. Stanculescu. Verification of VHDL designs using VAL. InProc. of the 25th Design Automation Conference, pages 48–53. ACM/IEEE, 1988.

  21. M. Fröhlich and M. Werner. da Vinci V1.3 user manual. Technical report. University of Bremen, Bremen, Germany, March 1994.

    Google Scholar 

  22. T. Margaria. Hierachical mixed-mode verification of complex FSMs described at the RT level. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129–156, Nijmegen, June 1992. IFIP TC10/WG 10.2, North-Holland.

  23. M.C. McFarland, A.C. Parker, and R. Camposano. Tutorial on high-level synthesis. In25th Design Automation Conference, pages 330–336, 1988.

  24. T.F. Melham. Abstraction mechanisms for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, editors,VLSI Specification, Verification, and Synthesis, pages 129–157. Kluwer Academic Publishers, 1988.

  25. L. Pierre. From a HDL description to formal proof systems: Principles and mechanization. In D. Borrione and R. Waxman, editors,Computer Hardware Description Languages and their Applications, pages 21–41. North-Holland, Marseille, April 1991.

  26. P.T. Breuer, L. Sánchez, and C.D. Kloos. Proof theory and a validation condition generator for VHDL. InProc. of the EURO-VHDL, Grenoble, France, September 1994. IEEE Press.

  27. R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel. Experience with embedding hardware description languages in HOL. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129–156, Nijmegen, June 1992. IFIP TC10/WG 10.2, North-Holland.

  28. R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel. The HOL verification of ELLA designs. InProc. of the International Workshop on Formal Methods in VLSI Design, Miami, 1991.

  29. R. Lipsett, C. Schaefer, and C. Ussery.VHDL: Hardware Description and Design. Kluwer Academic Publishers, 1989.

  30. R. Reetz and Th. Kropf. Hardwarebeschreibungssprachen und formale Verifikation. Technischer Bericht 358-C2-4/93, Sonderforschungsbereich 358, September 1993.

  31. R. Reetz and Th. Kropf. Simplifying deep embedding: A formalised code generator. InProc. of the International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 378–390, Malta, September 1994. Lecture Notes in Computer Science No. 859, Springer.

  32. D.M. Russinoff. Specifcation and verification of gate-level VHDL models of synchronous and asynchronous circuits. In E. Börger, editor,Speicification and Validation Methods, Oxford University Press. Oxford, 1994.

    Google Scholar 

  33. S. Olcoz and J.M. Colom. Toward a formal semantics of IEEE std. VHDL-1076. InEuro VHDL'93, pages 526–531, Hamburg, Germany, 1993.

  34. S. Rajgopal, K. Hedlund, and D. Reeves. Integrating hardware verification with CHDLs. In D. Borrione and R. Waxman, editors,Computer Hardware Description Languages and their Applications, pages 153–163. North-Holland, Marseille, April 1991.

  35. J.P. Van Tassel. A formalisation of the VHDL simulation cycle. InProc. of the International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 213–228. IFIP WG 10.2, September 1992.

  36. V. Stavridou, J.A. Goguen, A. Stevens, S.M. Eker, S.N. Aloneftis, and K.M. Hobley. FUNNEL and 2OBJ: Towards an integrated hardware design environment. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 197–223, Nijmegen, June 1992. IFIP TC10/WG 10.2, North-Holland.

  37. IEEE standard VHDL language reference manual. Std 1076, IEEE, 1987.

  38. W. Damm, G. Döhmen, V. Gerstner, and B. Josko. Modular verification of petri nets. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems, volume 430 ofLecture Notes in Computer Science, pages 180–207, REX Workshop, Mook, May/June 1989. Springer.

  39. X. Wang and E.P. Stabler. Formalization of VHDL synthesis procedure in higher-order logic. InProc. of the International Workshop on the HOL Theorem Proving System And Its Applications, pages 106–120, August 1991.

Download references

Author information

Authors and Affiliations

  1. Institut für Rechnerentwurf und Fehlertoleranz, Universität Karlsruhe, Postfach 6980, 76128, Karlsruhe, Germany

    Ralf Reetz & Thomas Kropf

Authors
  1. Ralf Reetz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Kropf
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This work was financed by the german research society (DFG) under contract SFB 358.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Reetz, R., Kropf, T. A flowgraph semantics of VHDL: Toward a VHDL verification workbench in HOL. Form Method Syst Des 7, 73–99 (1995). https://doi.org/10.1007/BF01383874

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01383874

Keywords

Search

Navigation