TY - GEN

T1 - Reasoning about VHDL using operational and observational semantics

AU - Goossens, K.G.W.

PY - 1995

Y1 - 1995

N2 - 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 [9].
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.
This work is supported by the euroform network sponsored by the Human Capital and Mobility programme of the European Community.

AB - 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 [9].
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.
This work is supported by the euroform network sponsored by the Human Capital and Mobility programme of the European Community.

U2 - 10.1007/3-540-60385-9_19

DO - 10.1007/3-540-60385-9_19

M3 - Conference contribution

SN - 3-540-60385-9

T3 - Lecture Notes in Computer Science

SP - 311

EP - 327

BT - Correct hardware design and verification methods : Proceedings of the IFIP WG 10.5 Advanced Research Working Conference ; October 2 - 4, 1995, Frankfurt/Main, Germany

A2 - Camurati, Paolo E.

A2 - Eveking, Hans

PB - Springer

CY - Berlin

T2 - conference; Advanced Research Working Conference on Correct Hardware Design Methologies (CHARME) ; 8 (Frankfurt/Main) : 1995.10.02-04; 1995-10-02; 1995-10-04

Y2 - 2 October 1995 through 4 October 1995

ER -