# An Executable Formal Model of the VHDL in Isabelle/HOL

arXiv: https://arxiv.org/abs/2202.04192 · HTML: https://mlsanity.com/paper/2202.04192/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 26 references that are in the map.
- First posted on arXiv 8 Feb 2022.

## Builds on (most cited first, 3 of 3)

- [Completeness for a First-order Abstract Separation Logic](https://mlsanity.com/paper/1608.06729/) (2016)
- [Modular Labelled Sequent Calculi for Abstract Separation Logics](https://mlsanity.com/paper/1710.10805/) (2017)
- [Formal Verification of Hardware Synthesis](https://mlsanity.com/paper/1301.4779/) (2013)

## Built on by (most cited first, 1 of 1)

- [Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification](https://mlsanity.com/paper/2503.22755/) (2025)

## Abstract (arXiv)

In the hardware design process, hardware components are usually described in a hardware description language. Most of the hardware description languages, such as Verilog and VHDL, do not have mathematical foundation and hence are not fit for formal reasoning about the design. To enable formal reasoning in one of the most commonly used description language VHDL, we define a formal model of the VHDL language in Isabelle/HOL. Our model targets the functional part of VHDL designs used in industry, specifically the design of the LEON3 processor's integer unit. We cover a wide range of features in the VHDL language that are usually not modelled in the literature and define a novel operational semantics for it. Furthermore, our model can be exported to OCaml code for execution, turning the formal model into a VHDL simulator. We have tested our simulator against simple designs used in the literature, as well as the div32 module in the LEON3 design. The Isabelle/HOL code is publicly available: https://zhehou.github.io/apps/VHDLModel.zip