论文标题
ISABELLE/HOL中VHDL的可执行正式模型
An Executable Formal Model of the VHDL in Isabelle/HOL
论文作者
论文摘要
在硬件设计过程中，硬件组件通常在硬件说明语言中描述。大多数硬件说明语言，例如Verilog和VHDL，都不具有数学基础，因此不适合对设计的正式推理。为了在最常用的描述语言之一中启用正式推理，我们在isabelle/hol中定义了VHDL语言的形式模型。我们的模型针对行业中使用的VHDL设计的功能部分，特别是Leon3处理器整数单元的设计。我们涵盖了VHDL语言的广泛特征，这些功能通常在文献中建模并为其定义了新颖的操作语义。此外，我们的模型可以导出到OCAML代码进行执行，将正式模型转换为VHDL模拟器。我们已经测试了模拟器针对文献中使用的简单设计以及Leon3设计中的Div32模块。 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
