Deploying Formal in a DO-254 Program
The primary focus of DO-254, referred to as ED-80 in Europe, is hardware reliability of airborne electronic hardware. DO-254 is considered state of the art and compliance is compulsory for any company putting an IC on an aircraft. One component of the standard is the verification of functional behavior. This activity is commonly accomplished using a directed test approach, where engineers identify the stimulus and test scenarios of interest and then ensure the design behavior matches the requirements. In recent years, constrained-random stimulus and coverage driven testing have become more widely adopted, and while certainly more effective than a directed testing approach, there remains the question as to whether the state space has been conclusively tested. Complimenting this approach if Formal Verification.
What is Formal Verification?
It is important to first note that Formal Verification takes a different approach in the verification of design behavior against its requirements. In formal verification, mathematical algorithms are leveraged to validate correctness. The beauty of a formal approach is it’s exhaustive analysis of the state space, meaning if there is undesirable behavior, the formal tool will point out the root cause(s) of the issue, saving a substantial amount of debug time. Additionally, the exhaustive nature of formal analysis is clearly appealing to safety and mission critical workflows because it effectively proves the total absence of unspecified behavior as well as identifying any bugs in the expected functionality. Often times, formal apps are built on top of the underlying mathematical analysis “engines” to provide push button behavior for a particular type of analysis. As an example, Questa Formal Autocheck hunts for combinatorial loops, FSM deadlocks, arithmetic overflow scenarios, and more.
Leveraging Formal in DO-254
Formal methods have their place in a DO-254 workflow. In fact, Appendix B calls out formal directly as an advanced verification technique. Unfortunately, the text written in the standard is difficult to understand. To help make sense of this, two white papers are now available which dive deep into the usage of Formal Verification in a DO-254 lifecycle.
- Understanding formal methods for use in DO-254 programs
- Formal Verification for DO-254 (and other Safety-Critical) Designs
In these papers, you will learn about the advantages (and limitations) of Formal Verification, using formal in the context of DO-254 guidance, and the deployment and qualification of Formal design automation technologies.
