Learn how to apply formal verification to safety-critical aviation designs
Formal verification techniques are being increasingly used to supplement established simulation strategies to trace and eliminate bugs and meet the hardware reliability requirements of aviation’s DO-254 (EU: ED-80) standard. However, their application is still at a comparatively early stage and there remain questions around functional verification’s use.
A new technical publication from Siemens Digital Industries Software addresses functional verification within this context. It takes a detailed look at why some bugs escape formal simulation, even though the technique has greatly matured in the last four decades, and why the increasing size and complexity of aviation designs targeting FPGAs present new challenges. On average, about 1 per cent of the bugs in a design today escape through to production silicon, still worryingly high for safety critical use-cases.
“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,” write authors David Landoll and Mark Eslinger of Siemens EDA.
“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.”
The books main sections look at developing supplementary formal verification methodologies for safety critical projects, and at the tool assessment, qualification and selection process set by the DO-254 standard.
The formal verification section is organized under four key topics.
- Formal verification demystified through examples
- Examples of applying formal verification to safety critical designs
- Deploying formal to add safety to the verification process
- The limitations of formal verification
Coding in SystemVerilog and flows are described in detail and with specific refence to the Questa Formal Verification tool from Siemens EDA. ‘Formal Verification for DO-254 (and other Safety-Critical) Designs’ is available for immediate download at this link.
