GOMACTech 2025 Preview: FPGA Safety and Security Policy Compliance via HDL-to-Bitstream Equivalence Checking (Session 43.5)

Security and safety policies across domains such as embedded security, defense safety, and automotive safety have been updated to require the ability to prove that an FPGA design’s functionality is unchanged from RTL through synthesis, P&R, and bitstream generation. 

Fortunately, emerging tools for bitstream equivalence checking can be paired with proven, FPGA-optimized equivalence checking to create a verification chain that satisfies these new policy demands. Indeed, at the upcoming GOMACTech conference in Pasadena, CA this March 17-20, Siemens will be describing an industry-first solution for RTL to bitstream equivalence checking for safety and security compliance.

Below is a sneak peek …

First, recall that the motivation for this new flow is that key portions of policies for defense security (DoD Microelectronics: FPGA Level of Assurance Best Practices), weapon system safety (AFMAN 91-119), and automotive safety (ISO 26262) all either directly call for – or are most comprehensively satisfied by – the use of a chain of verification tools that demonstrates equivalence between the user’s FPGA hardware description language (HDL) source code and the resulting programming bitstream.

Major requirements of these policies are met by the following EDA tool chain illustrated blow:

Starting at the top of this flow chart:

• Electrical engineers convert design specifications into HDL code – VHDL, Verilog, or SystemVerilog – that captures the functionality the FPGA needs to execute. After some functional verification, this HDL is then synthesized into lower-level logic gates, which is placed and routed in the FPGA
• This is when the integrated solutions on the LHS of the diagram provided by Siemens Questa Equivalent FPGA and GRC’s Enverite PV-Bit come into play:
  • Questa Equivalent FPGA by Siemens is the only equivalence checking tool optimized for FPGA architectures through direct integrations with FPGA vendor implementation flows. This solution verifies the equivalence between the user’s HDL, the synthesized gate-level netlist, and the final P&R gate-level netlist produced by the FPGA build tools
  • Enverite PV-Bit by Graf Research verifies both the logical and physical equivalence between the final, P&R gate-level netlist and the proprietary FPGA bitstream itself.

In short, this flow ensures that the functionality original HDL design is exactly the same functionality executed on-board the FPGA for all inputs and all time. Tying this back to the DoD assurance requirements cited above, the presentation will go on to connect these capabilities to FPGA safety and security policies that establish practices necessary to provide assurance that deployed FPGAs operate only as intended.

Furthermore, while safety policies are primarily concerned with assurance against human or build software errors, security policies have the additional concern of malicious actors actively seeking to create unwanted functionality. As such, the presentation will provide an exploration of how equivalence checking supports requirements for three policy documents: DoD FPGA Level of Assurance (LoA) security best practices, AFMAN 91-119 safety/security policy, and ISO 26262 automotive functional safety.

All of the above will be illustrated with real world customer case studies that will enumerate how each tool’s outputs directly link to policy requirements. For example:

• The RTL to synthesis netlist and synthesis to P&R netlist design representations were proven equivalent by Questa Equivalent FPGA, which produced a comparison result file. This includes detailed information on the comparison performed, including counterexamples upon detected failures.  Recording such evidence is required under all security and safety policy regimes, and it is emphasized in the DoD Evidence Based Assurance (EBA) paradigm.
• Enverite PV-Bit was run using the P&R’d design and the FPGA bitstream as inputs and produced both a design report and an attestation report, each of which were automatically digitally signed to prove their authenticity. The design report provides evidence related to the operation of PV-Bit on the specific user design, and the attestation report enumerates the set of features that the specific version of PV-Bit evaluated when producing the conclusions listed in the design report.

Here is the listing for the paper:

FPGA Safety and Security Policy Compliance via HDL-to-Bitstream Equivalence Checking
Session 43.5, Multidisciplinary Approaches to Security
Thursday, March 20 / 8:20 a.m. – 10 a.m. / Ballroom D&E

(And here is the list of all Siemens’ activities at GOMACTech)

If you don’t get to meet my colleague and presenter Kevin Urish in this session, please come by the Siemens booth (505) to deep-dive on this topic with him!

Joe Hupcey III
for Kevin Urish and the Siemens’ Questa OneSpin team