Lowering the adoption barriers for Formal Verification of ASIC and FPGA designs in the Space sector

The verification gap has reached the Space sector. Simulation is still good although limited, but as FPGA (Field Programable Gate Array) and ASIC (Application-Specific Integrated Circuit) capacities increase, this verification gap grows bigger. As the verification gap grows bigger, functional simulation will stop being enough to guarantee assurance of digital designs.

Thus, it is time to introduce Formal Verification, as a complement to simulation, into the space electronic engineer toolkit. Formal verification could be defined as "mathematically proving properties of digital designs". Currently, there aren't any standardized methodologies for formal verification, which leaves engineers to be left to their own to devise how to best apply the techniques to their designs. While the adoption barriers are high, the space community needs to prepare for the verification gap of the future.

This activity will develop a way to lower adoption barriers for Formal Verification in the Space Sector by implementing a multiple-headed approach, which comprises:

1. The definition of a formal methodology for sub-modules and IP cores,
2. The creation of a build and test manager,
3. The creation of a set of examples of increasing complexity, and
4. The application of the methodology to the formal verification of two different IP cores.