Graf Research is excited to attend DASC 2025, where we will discuss the impact of Enverite PV-Bit on avionics safety. Be sure to visit our booth to learn more about how Enverite by Graf Research is helping shape the future of safety and security in FPGA-based avionics systems.
Accelerating Recertification of FPGA-Based Avionics Systems via Bitstream Equivalence Checking
Jonathan Graf, Evan Drinkert, Scott Harper, Margaret Winslow, Alan Cook, Ali Asgar Sohanghpurwala, Tim Dunham, and Wilfredo Tabada
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.