by Peter T Breuer, Universidad Politécnica de Madrid
A denotational semantics and a Hoare programming logic for a subset of the standard hardware description language VHDL is set out. Both semantics define the behaviour of synchronously clocked VHDL simulators in declarative and compositional style. The logic is proved complete with respect to the denotation.
The subset of the language treated is essentially elaborated VHDL excluding only delta-delayed signal assignments and zero waits.
However, for brevity, only one of the two forms of signal assignment is dealt with in the talk. Moreover, for simplicity, it is assumed that signal resolution functions and local state are encoded away by appropriate use of expressions and signals.