A FORMALIZATION OF THE VHDL SIMULATION CYCLE

The VHSIC Hardware Description Language (VHDL) has been gaining wide acceptance as a unifying HDL. It is, however, still a language in which the only way of validating a design is by careful simulation. With the aim of better understanding VHDL's particular simulation process and eventually reasoning about it, a formalisation of VHDL's simulation cycle has been developed for a subset of the language. It has also been possible to embed the semantics in the Cambridge Higher-Order Logic (HOL) system and derive interesting properties about specific VHDL programs.