Skip to main content
Article
Structural Operational Semantics for a Portable Subset of Behavioral VHDL-93
Formal Methods in System Design
  • Krishnaprasad Thirunarayan, Wright State University - Main Campus
  • Robert Ewing
Document Type
Article
Publication Date
1-1-2001
Abstract

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, non-deterministic 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.

DOI
10.1023/A:1008786720393
Citation Information
Krishnaprasad Thirunarayan and Robert Ewing. "Structural Operational Semantics for a Portable Subset of Behavioral VHDL-93" Formal Methods in System Design Vol. 18 Iss. 1 (2001) p. 69 - 88 ISSN: 0925-9856
Available at: http://works.bepress.com/tk_prasad/38/