Semantics of a verification-oriented subset of VHDL

  • David Déharbe
  • Dominique Borrione
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)


This paper gives operational semantics for a subset of VHDL in terms of abstract machines. Restrictions to the VHDL source code are the finiteness of data types, and the absence of quantitative timing informations. The abstract machine of a design unit is built by composition of the abstract machines for its embedded processes and blocks. The kernel process in our model is distributed among the composed machines. One transition of the final abstract machine models a VHDL delta cycle. This model can be used for symbolic model checking and equivalence verification.


Statement Part Finite State Machine Assignment Statement Parallel Composition Abstract Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    C. Bayol, B. Soulas, F. Corno, P. Prinetto, and D. Borrione. A process algebra interpretation of a verification oriented overlanguage of VHDL. In Euro-DAC with Euro-VHDL '94, pages 506–511, Grenoble, France, Sep. 1994. ACM/IEEE, IEEE Computer Society Press.Google Scholar
  2. 2.
    W. Damm, B. Josko, and R. Schlör. Specification and Validation methods for Programming Languages and Systems, chapter Specification and Verification of VHDL-based System-Level Hardware Designs, pages 331–410. Oxford University Press, 1995. E. Börger, editor.Google Scholar
  3. 3.
    K. Davis. A Denotational Definition of the VHDL Simulation Kernel. In 11th International Symposium on Computer Hardware Description Languages and their Applications, pages 509–521, Ottawa, Canada, 1993.Google Scholar
  4. 4.
    A. Debreil and D. Jaillet. Synchronous description in VHDL for formal proof and resulting guidelines proposed by BULL. Advanced report, BULL Produits Systèmes Département Développement Assisté, rue Jean Jaures-B.P. 68-Les Clayes-sous-Bois-France, July 1992. BULL/92.0001 rev.A.Google Scholar
  5. 5.
    C. Delgado Kloos and P. Breuer, editors. Formal Semantics for VHDL, volume 307 of Series in Engineering and Computer Science. Kluwer Academic Publishers, Boston, March 1995.Google Scholar
  6. 6.
    R. Herrmann and H. Pargmann. Computing binary decision diagrams for VHDL data types. In Euro-DAC with Euro-VHDL '94, Grenoble, France, Sep. 1994.Google Scholar
  7. 7.
    IEEE. IEEE Standard VHDL Language Reference Manual, 1993. Std 1076–1993.Google Scholar
  8. 8.
    B. Levy, I. Filippenko, L. Markus, and T. Menas. Using the State Delta Verification System for Hardware Description. In V. Stravidou, T. Melham, and R. Boute, editors, Theorem Provers in Circuit Design, pages 337–360, Nijmegen, Netherlands, June 1992. IFIP A-10, North Holland.Google Scholar
  9. 9.
    S. Olcoz and J. Colon. A Petri net approach for the analysis of VHDL descriptions. In G. Milne and L. Pierre, editors, Correct Hardware Design and Verification Methods, volume 683 of Lecture Notes in Computer Science, pages 15–26, Arles, France, May 1993. ESPRIT WG 6018 and IFIP WG 10.2, Springer Verlag.Google Scholar
  10. 10.
    A. Salem and D. Borrione. VHDL for simulation, synthesis, and formal proofs of hardware, chapter Formal semantics for VHDL timing constructs. Kluwer international series in engineering and computer science. Kluwer Academic Publishers. 1992. J. Mermet editor.Google Scholar
  11. 11.
    J. Van Tassel. A formalisation of the VHDL simulation cycle. Technical Report 249, University of Cambridge, Cambridge, March 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • David Déharbe
    • 1
  • Dominique Borrione
    • 1
  1. 1.ARTEMIS-IMAGGrenoble Cedex 9France

Personalised recommendations