Isabelle/HOL中VHDL的可执行形式化模型
An Executable Formal Model of the VHDL in Isabelle/HOL
摘要：
在硬件设计过程中，硬件组件通常用硬件描述语言来描述。大多数硬件描述语言，如Verilog和VHDL，没有数学基础，因此不适合对设计进行形式化推理。为了使最常用的描述语言之一的VHDL的形式化推理，我们定义了一个正式的模型，在Isabelle/HOL的VHDL语言。我们的模型针对工业上使用的VHDL设计的功能部分，特别是LEON 3处理器的整数单元的设计。我们涵盖了广泛的功能，在VHDL语言中，通常没有建模的文献，并定义了一个新的操作语义为它。此外，我们的模型可以导出到OCaml代码执行，把正式的模型变成一个VHDL模拟器。我们已经测试了我们的模拟器对文献中使用的简单设计，以及在LEON 3设计的div 32模块。Isabelle/HOL代码可在https://zhehou.github.io/apps/VHDLModel.zip上公开获取
英文摘要：
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
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
