VHDL semantics and validating transformations

Formal models are used to provide an unambiguous definition of the semantic s of very high speed integrated circuit hardware description language (VHDL ) and to prove equi,equivalences of VHDL programs. This paper presents a fo rmal model of the dynamic semantics of VHDL that characterizes several impo rtant features of VHDL such as delta delays, pulse rejection limits, discon nection delays, postponed processes, sequential statements, and resolution functions. The underlying logic is interval temporal logic, which assists i n characterizing the timing information contained in a VHDL program. The se mantic definition is not dependent on the VHDL simulation cycle since it on ly defines the net effect of evaluating a VHDL program. It is argued that t his declarative style coupled with the inherent advantages of temporal logi c makes it possible to validate transformations (or rewrite rules) on VHDL programs and to formally reason about the timing aspects of :PVHDL. In part icular, we present proofs of soundness of rewrite rules such as process fol ding and signal collapsing, and use temporal logic to derive an algorithm f or determining when a given VHDL program is free of transaction preemption.