Research On Formal Methods For Modeling And Analyzing FPGA Programs

With the rapid development of computer and E-communication technology, the national requirements for the application of electronic automation are being strengthened. As a very important digital technology, Field-Programmable Gate Arrays(FPGAs) have been widely used in safe-critical systems, such as traffic systems, automotive electronics and defense industry, etc. Thus the reliability and safety of FPGA programs are required to satisfy strict performances. However, with the rapid increase of FPGA digital systems, its workload is also becoming heavier and the reliability of programs is difficult to be guaranteed only by artificial debugging. Moreover, the traditional simulation tools can be used to identity semanteme and grammar errors, but not logic mistakes in FPGA programs. Hence, to verify the correctness of design problem is an important research topic in the academic circles and the industrial circles, and important theoretic results have been published. Among them, the formal verification method is the most hopeful.A method is presented to model FPGA combinational logic programs as formal language—Petri nets, and to verify the system mutual exclusion specifications via stage reachable graph and Computation Tree Logic(CTL) Finally, this work introduces a method to model and analyze a class of synchronous sequential logic circuits.1. An algorithm is proposed to translate Very-High-Speed Integrated Circuit Hardware Description Language(VHDL) programs of FPGA combinational logic system to ordinary Petri nets;2. According to the working principle of FPGA, the state reachable graph of FPGA combinational logic system is computed based on its Petri-net model;3. CTL formula is used to describe system specifications and verify each state for detection and location instructions which violate mutual exclusion specifications in VHDL programs;4. According to the working principle of synchronous sequential logic circuit, a method is obtained to translate such circuits to inhibitor arc Petri nets, and to analyze Logic its function based on the state reachable graph of its Petri-net model.Using these methods, logic mistakes can be identified automatically in FPGA combinational logic programs. Hence, the reliability of FPGA system can be improved. The proposed methed has great value for application in formal verification of VHDL programs. Furthermore, this work presents the formal modeling and analysis method for a class of synchronous sequential logic circuit, and provides the possibility for further application of Petri net theory in digital system.