Accelerating Recertification of FPGA-Based Avionics Systems via Bitstream Equivalence Checking

Field programmable gate arrays (FPGAs) are ubiquitous in avionics. While FPGAs are easily reprogrammable, update cycles can be long even for minor changes due to recertification testing requirements. Formal verification software can provide proofs about some portions of the FPGA re-design process, but standard formal verification software cannot validate the final FPGA bitstream design. A new software technique, Bitstream Equivalence Checking (BEC), can prove the logical and physical equivalence of an FPGA bitstream to a physical netlist representation. Used in concert with Logic Equivalence Checking (LEC) as well as timing and physical design analysis tools, BEC enables a new delta verification flow that defines the relationship between an original, certified FPGA bitstream and the bitstream that results after minor updates to the source code. This paper explains the process and illustrates its application to an example AMD Xilinx FPGA design when modified with a variety of source changes. The consequences of applying the process to avionics systems recertification are explored.