Formal Verification Takes Safety-Critical Applications For A Drive

The high reliability of safety-critical chips for automotive applications is a well-known imperative for today’s higher-end cars and as driverless cars move closer to reality. Uber, in fact, is testing autonomous cars in Boston of all places, where aggressive driving reigns supreme and honking the horn is considered an art form.

As automotive manufacturers realize that their differentiation might rest on the latest electronic functionality, pressure for technology advancement is intense. In aeronautical electronics, competitive pressures are lower. After all, Airbus and Boeing don’t compete on fancy features for the pilots. Reliability is the indispensable design requirement to avoid catastrophic aircraft failure.

A range of standards pertaining to specific applications governs safety-critical devices. These standards specify certification, key compliance metrics, requirements management and other safety-related aspects. The International Electrotechnical Commission (IEC) oversees the automotive ISO 26262 standard, under the umbrella IEC61508. The Radio Technical Commission for Aeronautics (RTCA) publishes the DO-254 aeronautical standard and guides the compliance of complex electronic hardware in airborne systems.

For either automotive or aeronautical applications, safety-critical designs need to be free of systematic errors, ensure development design flaws are handled with rigorous design verification, certified design methodologies and intricate requirements tracking. The other major ISO 26262 requirement is the safe handling of random faults during device operation caused by effects such as radiation or electro-magnetic disruption that temporarily change a signal value in the device. This requirement drives the incorporation of fault-handling circuitry to enable recovery from failure without detriment to device operation. The verification of fault-handling systems requires fault injection to be applied with a diagnostic coverage level to 98% or more for devices meeting the Automotive Safety Integrity Level (ASIL) D ISO 26262 specification.

DO-254 focuses on design practices and systematic issues that require advanced verification techniques throughout the aeronautical development flow. The handling of random faults using on-chip safety handling solutions is essential to safety-critical automotive chips. Random faults in aeronautical devices where space and power are less of a concern make use of redundant systems. An aircraft normally contains three identical, redundant components operating concurrently for each critical electronic system. This Triple Modular Redundancy (TMR) technique ensures that if the operation of one component fluctuates from the other two, it is disregarded and shut down, providing a failsafe solution to random faults in avionics.

Formal verification is an ideal tool for complex, safety-critical verification in automotive or aeronautical applications, although its use differs between the two segments.

Many semiconductor companies use formal throughout automotive development. For systematic verification, it is an indispensable tool given its exhaustive nature. Because specified properties described using assertions can be related to verification requirements more exactly, verifying them is easier to catalog. For random faults, the latest formal tools now include fault-injection technology for diagnostic analysis to grade safe versus unsafe faults in the device, providing key information for regulatory organizations.

Aeronautical development tends to exhibit a significant degree of inertia due to the lack of competitive pressure and the need for careful, proven advancement. Formal is leveraged in the form of Equivalency Checking on FPGAs used in these systems to double check the synthesis and P&R process, and now super-linting code-checking tools.

New automotive engineering converts in need of safety-critical tools are flocking to formal verification, a result of its thorough and exhaustive analysis, and helping move the automotive industry one step closer to self-driving cars. The aeronautical industry undoubtedly will follow suit, but in its own conservative timeframe.