Reasoning about VHDL using operational and observational semantics
We define a Plotkin-style structural operational semantics for a subset of vhdl that includes delta time, zero-delay scheduling and waits, arbitrary wait statements, and (commutative) resolution functions. While most of these features have been dealt with in separation, their combination is intricate. We follow closely the “careful prose” definition of vhdl as given in .
We prove a (conditional) monogenicity result for the operational semantics showing that the parallelism present in vhdl is benign. A classification of program behaviours is also given.
While the semantics is of interest, of greater importance is the interpretation of the mature process algebra theory to our particular setting. An adaptation of bisimulation may be constructed but the concept of an observer, a process which inspects or acts as a test harness, turns out to be more useful. It leads naturally to a notion of observational equality that is a congruence with respect to parallel composition. This important result enables substitution of behaviourally equivalent subprograms without affecting the overall program behaviour. The capability to pass (incapability to fail) a test gives rise to a the may (must) preorder on processes. These preorders are shown to coincide.
KeywordsOperational Semantic Parallel Composition Sequential Program Process Algebra Denotational Semantic
- 1.Dominique Borrione, Laurence Pierre, and Ashraf Salem. PREVAIL: A proof environment for VHDL descriptions. In P Prinetto and P Camurati, editors, Advanced Research Workshop on Correct Hardware Design Methodologies, pages 163–186. ESPRIT CHARME, North Holland, June 1991.Google Scholar
- 2.P T Breuer, L Sanchez, and C Delgado Kloos. Clean formal semantics for VHDL. In European Design and Test Conference '94, 1994.Google Scholar
- 3.P T Breuer, L Sanchez, and C Delgado Kloos. A simple denotational semantics, proof theory and validation condition generator for unit-delay VHDL. Formal Methods in System Design, 7(1–2), July 1995.Google Scholar
- 4.R De Nicola and M C B Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1994.Google Scholar
- 5.Rocco De Nicola and Rosario Pugliese. Testing Linda: Observational semantics for an asynchronous language. Rapporto di Ricerca SI/RR-94/06, Dipartimento di Scienze dell'Informazione, Università di Roma, Italy, November 1994. To appear in Structures in Concurrency Theory (STRICT'95).Google Scholar
- 6.Carlos Delgado Kloos and Peter T Breuer, editors. Formal Semantics for VHDL, volume 307 of Kluwer International Series In Engineering And Computer Science. Kluwer Academic Publishers, March 1995.Google Scholar
- 7.Ivan V Fillippenko. VHDL verification in the state delta verification system (SDVS). In 1991 International Workshop on Formal Verification in VLSI Design, January 1991.Google Scholar
- 8.K G W Goossens. Reasoning about VHDL using operational and observational semantics. Rapporto di Ricerca SI/RR 95/06, Dipartimento di Scienze dell'Informazione, Università di Roma “La Sapienza”, April 1995.Google Scholar
- 9.The Institute of Electrical and Electronics Engineers, Inc., 345 East 47th Street, New York, NY10017 USA. IEEE Standard VHDL Language Reference Manual, IEEE std 1076–1987 edition, 1988.Google Scholar
- 10.The Institute of Electrical and Electronics Engineers, Inc., 345 East 47th Street, New York, NY10017 USA. IEEE Standard VHDL Language Reference Manual, IEEE std 1076–1993 edition, 1993.Google Scholar
- 11.Robin Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, 1989.Google Scholar
- 12.D M R Park. Concurrency and Automata on Infinite Sequences, volume 104 of Lecture Notes in Computer Science. Springer Verlag, 1980.Google Scholar
- 13.Gordon Plotkin. A structural approach to operational semantics. Technical Report FN-19, Computer Science Department, Aarhus University (DAIMI), 1981.Google Scholar
- 14.Simon Read. Formal Methods for VLSI Design. PhD thesis, Department of Computation, University of Manchester, 1994.Google Scholar
- 15.Ashraf Salem and Dominique Borrione. Formal semantics of VHDL timing constructs. In Euro-VHDL Stockholm, September 1991.Google Scholar
- 16.L Sanchez, C Delgado Kloos, and P T Breuer. Stream semantics for VHDL: An example. In Workshop on Design Methodologies for Microelectronics and Signal Processing, 1993.Google Scholar
- 17.Gabriele Umbreit. Providing a VHDL-interface for proof systems. In EURO-DAC, pages 698–703, 10662 Los Vaqueros Circle, PO Box 3014, Los Alamitos, CA 90720-1264, September 1992. IEEE Computer Society Press.Google Scholar
- 18.Philip A Wilsey. Developing a formal semantic definition of VHDL. In J Mermet, editor, VHDL for Simulation, Synthesis and Formal Proofs of Hardware, pages 243–256. Kluwer Academic Publishers, 1992.Google Scholar