The Application of Formal Verification on the FPGA of Instrument and Control Systems in Nuclear Power Plants

Autor: Hai Zeng, Sen Li, Jiaxu Zuo
Rok vydání: 2017
Předmět:
Zdroj: Proceedings of The 20th Pacific Basin Nuclear Conference ISBN: 9789811023101
DOI: 10.1007/978-981-10-2311-8_63
Popis: With the development of the nuclear technology, the instrumentation and control (I&C) systems have evolved from the analog systems to the current state-of-the-art digital systems. It has been reported that China has recently developed the digital systems based on Field Programmable Gate Array (FPGA) in CAP1400 nuclear power plant. And the lack of methods in the verification and validation work of the FPGA systems has become an important issue. This thesis describes the basic principles of FPGA, and the development process of FPGA. And then, the thesis proposes an effective improved method—formal verification, describing three methods of formal verification in detail, namely theorem proof, model checking, and equivalence proof. Describing the FPGA verification methodology and pointing out the shortcomings of traditional simulation, comparing the formal verification and traditional simulation verification in terms of complexity, timing, and applications. We also discussed the importance of formal verification method in FPGA. We selected the temperature and power control chip based on FPGA as an example, using System Verilog Assertions (SVA) method of model checking, and verifying the SRAM controller module and the internal calculation module. Through the analysis of the results, this paper proved the feasibility of formal verification methods in the instrumentation and control system of nuclear power plants, and provided some references of verification work for other system chips in instrumentation and control of nuclear power plant in the future work. The thesis showed that verification engineers can use the formal verification method based on SVA to verify the robustness of the system quickly and accurately. This method improves the controllability and observability which are the main drawbacks of the traditional simulation verification. It also avoids several issues in the debug process of traditional simulation verification, improving the accuracy and completeness of the chip verification.
Databáze: OpenAIRE