FPGA程序的形式化建模与分析方法研究

摘要

随着计算机、电子通信等技术的高速发展，国家对电子自动化应用的要求也在不断提高。现场可编程门阵列（Field Programmable Gate Array，FPGA）作为目前一项非常重要的数字化技术，被广泛应用于一些安全苛求的系统（例如交通、汽车电子和军工产业等），这就对FPGA程序的安全可靠性提出了严格的要求。然而，随着FPGA数字系统的规模不断增大，仅仅依靠设计人员的调试使得工作量变得繁重，难以保证程序的可靠性，而且传统仿真工具仅能识别语义和语法问题，却无法检测出隐藏在程序中的逻辑错误。因此，设计正确性的验证问题是目前学术界和工业界的重要研究课题，并取得了丰硕的成果，其中形式化验证方法的应用最为广泛。
　　本研究主要内容包括：⑴选用Petri网作为FPGA组合逻辑系统的VHDL（Very-High-Speed Integrated Circuit Hardware Description Language）程序的建模工具，提出将 VHDL程序自动转换为普通Petri网的算法；⑵根据FPGA工作原理，通过Petri网模型来计算获得FPGA组合逻辑系统的状态可达图；⑶采用CTL公式描述系统的性质规范并枚举验证每个状态，目的是检测和定位VHDL程序中违反互斥规范的语句；⑷根据同步时序逻辑电路的工作原理，提出了这类电路的抑制弧Petri网建模方法，并通过Petri网可达图分析电路的逻辑功能。

目录

封面

声明

中文摘要

英文摘要

目录

第1章 绪论

1.1 课题研究背景与意义

1.2 国内外研究现状

1.3 本文研究内容和结构安排

第2章 基础知识

2.1 引言

2.2 Petri网的基础知识

2.3 VHDL语言介绍

2.4 小结

第3章 FPGA组合逻辑程序的Petri网建模方法

3.1 引言

3.2 模型框架和建模思路

3.3 将组合逻辑VHDL程序转换为普通Petri网的算法

3.4 Petri网模型的简化与电路实现

3.5 小结

第4章 基于Petri网的FPGA组合逻辑系统状态可达图计算方法

4.1 引言

4.2 FPGA组合逻辑系统状态可达图生成算法

4.3 具体示例分析

4.4 小结

第5章 基于Petri网的系统互斥规范形式化验证

5.1 引言

5.2 形式化验证的思路

5.3 计算树逻辑CTL

5.4 系统性质规范的描述和验证算法

5.5 具体示例分析

5.6 小结

第6章 抑制弧Petri网在同步时序逻辑电路中的应用

6.1 引言

6.2 抑制弧Petri网及常用触发器的建模方法

6.3 同步时序逻辑电路状态可达图生成算法

6.4 具体示例分析

6.5 小结

第7章 总结与展望

7.1 研究总结

7.1 展望未来

参考文献

致谢

个人简历、在学期间发表的学术论文与研究成果