Formal verification for DO-254 and other safety-critical designs
DO-254 defines a process that hardware vendors must follow to get their hardware certified for use in avionics.
Formal Verification – A better methodology for safety critical designs
In a perfect world, all scenarios that can occur should be identified up-front during the requirements capture process and verified during the directed test simulation process. For smaller simpler designs, this task is challenging, but possible.
However, today’s FPGA designs can easily reach hundreds-of-thousands of gates, and frequently exceed 1M gates. As designs grow in size and complexity, the number of corner case situations in the design grows exponentially, making thorough verification virtually impossible.
Indeed, DO-254 itself recognizes this limitation by declaring that, if you can comprehensively verify a device, you can declare it “simple” and avoid much of the DO-254 process. Therefore, by definition, any device meeting DO-254 Level A/B that isn’t identified as “simple” has been verified with incomplete functional verification.
That isn’t to say that all these designs are necessarily buggy or somehow unsafe. However, it does say that there is some risk that a functional bug has slipped through the verification process. This is an inherent by-product of producing larger and more complex designs.
Most late-stage bugs escape early detection because they are not easy to stimulate and detect. Most of these bugs require interactions between several different pieces of logic, and will only exhibit themselves under the precise alignment of several unusual or possibly unexpected events. This paper will explore this phenomenon, why functional simulation and even lab verification misses these corner case scenarios, and how formal verification can play a role in better verifying safety critical designs.