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

发布时间：2018-01-26 07:08

本文关键词： FPGA组合逻辑程序 Petri网状态可达图形式化验证同步时序逻辑电路　出处：《华侨大学》2015年硕士论文　论文类型：学位论文

【摘要】：随着计算机、电子通信等技术的高速发展,国家对电子自动化应用的要求也在不断提高。现场可编程门阵列(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网理论在数字系统中的进一步应用提供了可能。
[Abstract]:With the rapid development of computer, electronic communication and other technologies. National requirements for electronic automation applications are also increasing. Field Programmable Gate Array Field Programmable Gate Array. FPGA, as a very important digital technology, has been widely used in some secure systems (such as transportation, automotive electronics and military industry). This puts forward strict requirements for the security and reliability of FPGA programs. However, with the increasing scale of FPGA digital system, the workload becomes more and more heavy only by the debugging of designers. It is difficult to ensure the reliability of the program, and the traditional simulation tools can only identify semantic and syntax problems, but can not detect the hidden logic errors in the program. Verification of design correctness is an important research topic in academia and industry, and has achieved fruitful results. The formal verification method is the most widely used. This paper presents the modeling method of FPGA combinational logic program based on the formal language, Petri net. And the verification method of system mutex specification which can be combined with Datuk and Computation Tree Logic (CTL). Finally, the modeling and analysis method of a class of synchronous sequential logic circuits is given. The Petri net is selected as the VHDL of FPGA combinational logic system. Very-High-Speed Integrated Circuit Hardware Description language). Modeling tools for programs. An algorithm for automatically converting VHDL programs into ordinary Petri nets is proposed. 2.According to the working principle of FPGA, the state of FPGA combinational logic system can be obtained by Petri net model. 3. CTL formula is used to describe the properties and specifications of the system and to enumerate and verify each state, in order to detect and locate the statements that violate the mutex specification in the VHDL program. 4. According to the working principle of synchronous sequential logic circuit, the modeling method of restraining arc Petri net for this kind of circuit is proposed. The method presented in this paper can automatically analyze and locate the logic errors in the FPGA combinational logic program and improve the reliability of the FPGA system. The formal verification of VHDL program has great application value. This paper also proposes a formal modeling and analysis method for a class of synchronous sequential logic circuits. It provides the possibility for the further application of Petri net theory in digital system.
【学位授予单位】：华侨大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TN791

【参考文献】