Formal Verification for DO-254 (and other Safety-Critical) Designs

Overview of DO-254

The focus of Document RTCA/DO-254 (all quotes from RTCA/DO-254 are used with permission from RTCA. www.rtca.org), also known as “ED-80” in Europe (and hereafter referred to as simply “DO-254”), is hardware reliability for flight safety. In other words, the FAA, EASA, and other aviation authorities want to ensure that the airborne electronic hardware (AEH) used in avionics works reliably as specified, avoiding faulty operation and potential air disasters. DO-254 defines a process that hardware vendors must follow to get their hardware certified for use in avionics. DO-254, which the FAA began enforcing in 2005 (through AC20-152), is modeled after DO-178B, the equivalent process for certifying software, which was published in its original version (DO-178) over 25 years ago. All in-flight hardware (i.e., PLD, FPGA or ASIC designs) must now comply with DO-254.

DO-254 and Functional Verification

Most DO-254 projects utilize functional verification to demonstrate that the system’s functional requirements have been properly met and verified. This is typically performed through a “directed test” approach using VHDL or Verilog and a simulation tool such as ModelSim or Questa from Siemens EDA, a part of Siemens Digital Industries Software. In a directed test approach, a verification engineer writes explicit tests that exercise the design’s requirements, and verifies the design operated as expected. This is used as evidence that the design correctly meets its requirements. Each directed test typically targets one or a few high-level requirements, and some requirements might need multiple directed tests.
However, project teams frequently find that, even after a focused verification effort involving hundreds or thousands of directed tests that achieve close to full statement coverage, the design still exhibits bugs in the lab. In some cases, bugs are found during full system verification, or even later in the project cycle. This problem worsens with increasing design size and complexity. In fact, on average, ~1% of the bugs are present in the final production design. This creates protracted project schedules, unexpected cost over-runs, and much higher costs, as well as potential safety issues.
Even after these bugs are found and resolved, the team is left with a haunting question:

• “Did we really find all the bugs?
• Are there any more bugs?
• Will the design always work as desired?”

For safety-critical applications, lives may depend on the answers to these questions.

To answer these questions, we need to understand why functional simulation missed these bugs in the first place.

* NOTE * This document does not provide general information on the DO-254 process, but rather focuses on the issue of advanced verification and tool assessment, specifically for the Siemens EDA Questa Formal Verification tool. If you need general information or training on the DO-254 process, we advise that you sign up for a DO_254 compliance class, such as the one offered through our Siemens EDA Partner, Patmos Engineering Services. You can get more information by clicking this link.