VHDL semantics and validating transformations

Formal models are used to provide an unambiguous definition of the semantics of very high speed integrated circuit hardware description language (VHDL) and to prove equivalences of VHDL programs. This paper presents a formal model of the dynamic semantics of VHDL that characterizes several important features of VHDL such as delta delays, pulse rejection limits, disconnection delays, postponed processes, sequential statements, and resolution functions. The underlying logic is interval temporal logic, which assists in characterizing the timing information contained in a VHDL program. The semantic definition is not dependent on the VHDL simulation cycle since it only defines the net effect of evaluating a VHDL program. It is argued that this declarative style coupled with the inherent advantages of temporal logic makes it possible to validate transformations (or rewrite rules) on VHDL programs and to formally reason about the timing aspects of VHDL. In particular, we present proofs of soundness of rewrite rules such as process folding and signal collapsing, and use temporal logic to derive an algorithm for determining when a given VHDL program is free of transaction preemption