Experience with Embedding Hardware Description Languages in HOL
The semantics of hardware description languages can be represented in higher order logic. This provides a formal deenition that is suitable for machine processing. Experiments are in progress at Cambridge to see whether this method can be the basis of practical tools based on the HOL theorem-proving assistant. Three languages are being investigated: ELLA, Silage and VHDL. The approaches taken for these languages are compared and current progress on building semantically-based theorem-proving tools is discussed.