Application Research of Formal Verification in Aerospace FPGA

In the current aerospace system, FPGA is mainly used to implement important functions such as navigation control, image recognition, and signal processing. Its safety directly affects system functionality, performability and other key technical metrics. With the increasing scale and complexity of FPGA-based aerospace software, traditional verification methods such as simulation verification and physical testing have struggled to cover all boundary scenarios, thus the test sufficiency has gradually declined. To ensure high safety and high reliability of aerospace FPGA, formal verification technology has gradually become one of the important verification methods. In this paper, the present situation of the research on the design of formal verification of aerospace FPGA is studied, and the advantages and disadvantages of formal verification are introduced. Finally, combining with characteristics of aerospace FPGA, we summarizes the problems faced in the application of formal verification in the past decade, and summarizes our solutions, some of which have been partially or wholly applied in our verification.