PostScript This paper presents a formal model of several fundamental concepts in VHDL including the semantics of individual concurrent statements, and groups of those statements, resolution functions, delta delays, and hierarchical component structuring. Based on this model, several extensions to VHDL are proposed, including nondeterministic assignments and unbounded asynchrony. Nondeterminism allows the specification of environments and of classes of devices. This model naturally captures the meaning of composition of VHDL programs. This thesis develops a sound, mechanically verified proof system suitable for the mechanical verification of both the safety and liveness properties of concurrent programs.
Mechanical verification increases the trustworthiness of a proof.
The proof system provides a mechanized framework for reasoning about concurrent programs under a variety of fairness assumptions. It is demonstrated by the mechanically verified proofs of four concurrent programs. This thesis presents several significant results, including the first extensive mechanized use of proof rules which are theorems of an operational semantics. This thesis both contributes to the science of mechanized program verification and lays the groundwork for future research. International Workshop on Formal Methods in VLSI Design, Miami, January, 1991.