Formal Methods for Aircraft Standards Compliance

When promoting adoption of formal methods in functional verification, there are two hurdles to overcome: one technical, the other people. The first is a comfortable and familiar challenge for us engineers. Take the course, pass the test, get the certificate. Very mechanical and deterministic. People on the other hand are non-deterministic and less amenable to logical arguments. They already have a solution (simulation or lab testing for FPGAs) with which they are very comfortable. Imperfect sure, but they understand how to work with those limitations.

Formal methods can provide a definite proof that an expected behavior will never fail but require new investment in training and experience. What ultimately tilts the scale is regulatory and competitive pressure, now emerging around DO-254 compliance for airborne electronic hardware. Where probabilistic simulation-based proofs sometimes aren’t good enough. Siemens have just released a white paper to help ease designers into working with the formal methods appendix of DO-254.

First, understand your audience

Formal proponents often don’t pay much attention to the people-hurdle. The authors of this paper (Harry Foster, Mark Eslinger and David Landoll) put persuading their audience front and center. They are aiming directly at people who design components for aircraft, not smartphones, cars or datacenters. Their platforms of choice are PLDs, FPGAs, perhaps less commonly ASICs and their design language of choice is VHDL. They’re familiar with assertion-based verification and may already use PSL or SVA for assertions. Finally, DO-254 compliance is their touchstone; how will formal methods help them here? The authors get all of this and are careful to provide a gentle path into formal methods which doesn’t presume much of what we might take for granted in the ASIC design world.

Decrypting the DO-254 appendix on formal

The standard was released over 20 years ago, when formal tools were research applications, primarily directed to theorem proving for software. Objectives and language used in the appendix reflect this very early use of such techniques, which must look very discouraging to any hands-on hardware designer with an objective and a deadline to meet. A large part of the Siemens white paper is devoted to providing a translation to modern day formal methods and applications. To a terminology far less intimidating and more actionable in a production verification environment.

I co-authored a book along these lines directed at ASIC designers (Finding Your Way Through Formal Verification). It was interesting for me to compare similarities and differences, especially in how the authors take a more from-scratch start in understanding the value of formal methods. One point that will resonate especially with designers of aircraft components is traceability. An assertion, formally checked, can connect directly to a requirement. If the assertion is proved, the requirement is met, whereas with simulation you still need to prove you have met adequate coverage.

Building trust

All of this makes sense, but who is really using formal methods in production? Big SoC designers must live on the bleeding edge, but mil-aero designers have different priorities. The paper goes on to elaborate with supporting information to show that these more cautious designers aren’t going to be guinea pigs. Use of formal methods is already well established among many leading semiconductor and systems companies and use models are now very well defined. There are now commercial tools available from multiple suppliers and this market is growing at a healthy clip.

They also spend time on a topic that I think is very important in building trust. They talk about limitations. Formal methods have well-known size/complexity limits. These are less acute for hardware than for software given the nature of modern RTL-based design but they’re real, nonetheless. The moral being that you should choose target problems in the testplan to accommodate these limitations. Certain classes of problem are challenging – datapaths and deep-sequential problems for example. Proof attempts can return an inconclusive result in which case you may need to break the problem down further or satisfy yourself that the proof depth is adequate to meet the requirement. Most important of all, formal methods do not replace dynamic verification (simulation). These techniques are complementary and always will be, except perhaps for very small functions.

This paper is a good example of how to promote a technology to an audience unfamiliar not only with the technique but also the need. Good job!

Also Read:

Verifications Horizons 2021, Now More Siemens

Optimize AI Chips with Embedded Analytics

AMS IC Designers need Full Tool Flows