|Title||Structural Operational Semantics for a Portable Subset of Behavioral VHDL-93|
|Publication Type||Journal Article|
|Year of Publication||2001|
|Authors||Robert L. Ewing, Krishnaprasad Thirunarayan|
Goossens defined structural operational semantics for a subset of VHDL-87 and proved that the parallelism present in VHDL is benign. We extend thiswork 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.
|Full Text|| |
K. Thirunarayan and R. L. Ewing, Structural Operational Semantics for a Portable Subset of Behavioral VHDL-93, In : Formal Methods in System Design,, Jan 2001.