VHDL is the standard language for the description of hardware at different levels of abstraction. Verification of VHDL programs requires a formal semantics for VHDL in a calculus enabling formal correctness proofs. Some of the hardware specific constructs of VHDL, disable classical approaches to semantics of usual programming languages.
The talk gave a formal semantics, based on higher order logic and flow graphs, that allows a simple formalisation of a large subset of VHDL. It avoids many disadvantages of conventional compiler based approaches and is well-suited to hardware verification. The talk presented the problems in developing a formal semantics for VHDL, the particular tasks connected with formal verification of VHDL and the central ideas of the Karlsruhe solution.