Automatic property generation for formal verification applied to HDL-based design of an on-board computer for space applications

The flexibility of Commercial-Off-The-Shelf (COTS) SRAM based FPGAs is an attractive option for the design of artificial satellites, however, the functional verification of HDL-based designs is required and is of fundamental importance. Formal verification using model checking represents a system as formal model that are automatically generated by synthesis tools. On the other hand, the properties are represented by temporal logic expressions and are traditionally manually elaborated, which is susceptible to human errors increasing the costs and time of the verification. This work presents a new method for automatic property generation for formal verification of Hardware Description Language (HDL) based systems. The industrial case study is a communication subsystem of an artificial satellite, which was developed in cooperation with the Brazilian Institute of Space Research (INPE).