An Executable Formal Model of the VHDL in Isabelle/HOL
This work addresses the problem of enabling formal verification for hardware designers using VHDL, though it is incremental as it builds on existing formal methods for specific components.
The authors tackled the lack of mathematical foundation in VHDL for formal reasoning by defining an executable formal model in Isabelle/HOL, which was tested against simple designs and the LEON3 processor's div32 module.
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