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