本文關(guān)鍵詞： FPGA組合邏輯程序 Petri網(wǎng) 狀態(tài)可達(dá)圖 形式化驗(yàn)證 同步時(shí)序邏輯電路　出處：《華僑大學(xué)》2015年碩士論文　論文類型：學(xué)位論文

【摘要】：隨著計(jì)算機(jī)、電子通信等技術(shù)的高速發(fā)展,國家對電子自動化應(yīng)用的要求也在不斷提高。現(xiàn)場可編程門陣列(Field Programmable Gate Array,FPGA)作為目前一項(xiàng)非常重要的數(shù)字化技術(shù),被廣泛應(yīng)用于一些安全苛求的系統(tǒng)(例如交通、汽車電子和軍工產(chǎn)業(yè)等),這就對FPGA程序的安全可靠性提出了嚴(yán)格的要求。然而,隨著FPGA數(shù)字系統(tǒng)的規(guī)模不斷增大,僅僅依靠設(shè)計(jì)人員的調(diào)試使得工作量變得繁重,難以保證程序的可靠性,而且傳統(tǒng)仿真工具僅能識別語義和語法問題,卻無法檢測出隱藏在程序中的邏輯錯(cuò)誤。因此,設(shè)計(jì)正確性的驗(yàn)證問題是目前學(xué)術(shù)界和工業(yè)界的重要研究課題,并取得了豐碩的成果,其中形式化驗(yàn)證方法的應(yīng)用最為廣泛。本文基于形式化語言——Petri網(wǎng)給出了FPGA組合邏輯程序的建模方法,以及系統(tǒng)狀態(tài)可達(dá)圖和計(jì)算樹邏輯(Computation Tree Logic,CTL)相結(jié)合的系統(tǒng)互斥規(guī)范驗(yàn)證方法,最后還給出了一類同步時(shí)序邏輯電路的建模和分析方法:1.選用Petri網(wǎng)作為FPGA組合邏輯系統(tǒng)的VHDL(Very-High-Speed Integrated Circuit Hardware Description Language)程序的建模工具,提出將VHDL程序自動轉(zhuǎn)換為普通Petri網(wǎng)的算法;2.根據(jù)FPGA工作原理,通過Petri網(wǎng)模型來計(jì)算獲得FPGA組合邏輯系統(tǒng)的狀態(tài)可達(dá)圖;3.采用CTL公式描述系統(tǒng)的性質(zhì)規(guī)范并枚舉驗(yàn)證每個(gè)狀態(tài),目的是檢測和定位VHDL程序中違反互斥規(guī)范的語句;4.根據(jù)同步時(shí)序邏輯電路的工作原理,提出了這類電路的抑制弧Petri網(wǎng)建模方法,并通過Petri網(wǎng)可達(dá)圖分析電路的邏輯功能。本文所提出的方法可以自動分析和定位FPGA組合邏輯程序中的邏輯錯(cuò)誤,提高FPGA系統(tǒng)的可靠性,對VHDL程序的形式化驗(yàn)證有較大的應(yīng)用價(jià)值。本文還對一類同步時(shí)序邏輯電路提出了形式化建模和分析方法,為Petri網(wǎng)理論在數(shù)字系統(tǒng)中的進(jìn)一步應(yīng)用提供了可能。
[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.
【學(xué)位授予單位】：華僑大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TN791

【參考文獻(xiàn)】

相關(guān)期刊論文 前3條

1 楊海鋼;孫嘉斌;王慰;;FPGA器件設(shè)計(jì)技術(shù)發(fā)展綜述[J];電子與信息學(xué)報(bào);2010年03期

2 刁嵐松,孟晗,劉明業(yè),楊凱;高級綜合中VHDL描述向Petri網(wǎng)轉(zhuǎn)換方法的研究[J];計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào);2003年09期

3 逄濤;段振華;劉曉芳;;Verilog程序的命題投影時(shí)序邏輯符號模型檢測[J];西安電子科技大學(xué)學(xué)報(bào);2014年02期

，

本文編號：1465018