Experience with Embedding Hardware Description Languages in HOL

TLDR

The semantics of hardware description languages can be represented in higher order logic. Experiments are underway at Cambridge to determine whether this method can underpin practical tools based on the HOL theorem‑proving assistant. The authors investigate three languages—ELLA, Silage, and VHDL—comparing their approaches and reporting progress on building semantically‑based theorem‑proving tools. The formal definition is suitable for machine processing, and the authors compare approaches for ELLA, Silage, and VHDL while reporting progress on building semantically‑based theorem‑proving tools.

Abstract

The semantics of hardware description languages can be represented in higher order logic. This provides a formal definition 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.