硬件综合的形式化验证
编程语言
2013-11-08 v1
摘要
我们报道了一种名为 Fe-Si（FEatherweight SynthesIs）的高级硬件描述语言（HDL）认证编译器的实现。Fe-Si 是 Bluespec 的简化版本，Bluespec 是一种基于受保护原子动作概念的 HDL。Fe-Si 在 Coq 中被定义为依值类型的深度嵌入。编译器的目标语言对应于 Verilog 或 VHDL 的可综合子集。我们方法的一个关键方面是，编译器的输入程序可以在 Coq 内部定义并证明其正确性。然后，我们使用抽取和一个 Verilog 后端（用 OCaml 编写）来获得硬件设计的认证版本。
引用
@article{arxiv.1301.4779,
title = {Formal Verification of Hardware Synthesis},
author = {Thomas Braibant and Adam Chlipala},
journal= {arXiv preprint arXiv:1301.4779},
year = {2013}
}