Isabelle/HOL 中 VHDL 的可执行形式化模型
计算与语言
2022-02-10 v1 形式语言与自动机理论
计算机科学中的逻辑
摘要
在硬件设计过程中，硬件组件通常用硬件描述语言描述。大多数硬件描述语言（如 Verilog 和 VHDL）没有数学基础，因此不适合对设计进行形式化推理。为了在最常用的描述语言之一 VHDL 中启用形式化推理，我们在 Isabelle/HOL 中定义了 VHDL 语言的形式化模型。我们的模型面向工业中使用的 VHDL 设计的功能部分，特别是 LEON3 处理器整数单元的设计。我们涵盖了文献中通常未被建模的 VHDL 语言中的广泛特性，并为其定义了一种新颖的操作语义。此外，我们的模型可导出为 OCaml 代码以供执行，从而将形式化模型转变为 VHDL 模拟器。我们已针对文献中使用的简单设计以及 LEON3 设计中的 div32 模块测试了我们的模拟器。Isabelle/HOL 代码公开可用：https://zhehou.github.io/apps/VHDLModel.zip
引用
@article{arxiv.2202.04192,
title = {An Executable Formal Model of the VHDL in Isabelle/HOL},
author = {Wilayat Khan and Zhe Hou and David Sanan and Jamel Nebhen and Yang Liu and Alwen Tiu},
journal= {arXiv preprint arXiv:2202.04192},
year = {2022}
}