An Executable Formal Model of the VHDL in Isabelle/HOL

TL;DR

This paper presents a formal, executable model of VHDL in Isabelle/HOL, enabling formal reasoning and simulation of hardware designs, including complex features and real-world processor components.

Contribution

It introduces a comprehensive operational semantics for VHDL in Isabelle/HOL, covering features often omitted in previous models, and provides a VHDL simulator exported to OCaml.

Findings

Successfully modeled VHDL features used in industry

Validated the model with LEON3 processor's integer unit

Generated an executable VHDL simulator from the formal model

Abstract

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