Structural operational semantics for a portable subset of behavioral VHDL-93

Goossens defined structural operational semantics for a subset of VHDL-87 and proved that the parallelism present in VHDL is benign. We extend this work to include VHDL-93 features such as shared variables and postponed processes that change the underlying semantic model. In the presence of shared v...

Full description

Saved in:
Bibliographic Details
Published in:Formal methods in system design 2001-01, Vol.18 (1), p.69-88
Main Authors: Thirunarayan, Krishnaprasad, Ewing, Robert L
Format: Article
Language:English
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Goossens defined structural operational semantics for a subset of VHDL-87 and proved that the parallelism present in VHDL is benign. We extend this work to include VHDL-93 features such as shared variables and postponed processes that change the underlying semantic model. In the presence of shared variables, nondeterministic execution of VHDL-93 processes destroys the unique meaning property. We identify and characterize a class of portable VHDL-93 descriptions for which unique meaning property can be salvaged. We analyze the computability of the portability condition and show that portability checks are neither local nor static. Our formal specification can serve as a correctness criteria for a VHDL-93 simulator or can be used as a basis for coding a simulator.
ISSN:0925-9856
DOI:10.1023/A:1008786720393