Formal-Based Verification for Safety-Critical Aeronautical Devices

Although the aeronautical electronics sector lacks the competitive pressure of its fast-paced cousin, the rapidly growing automotive semiconductor market, the aero sector is evolving and incorporating new techniques.

Formal verification has become a go-to technology in the safety-critical sphere due to the exhaustive nature of its analysis. By tackling both systematic design bugs as well as random failure verification, it enables crucial reliability metrics to be met. In today’s aeronautical development processes, formal is used to check design code and flow consistency, although its potential is far greater.

Safety-Critical Device Primer

Competition is driving modern automobile electronic sophistication, resulting in increasing integrated circuit (IC) complexity. Safety-critical development is, of course, more widespread than the automotive industry. For example in the aeronautical, power generation and medical devices sectors, extreme reliability is the essential requirement.

Regardless of the industry sector, safety-critical designs consist of two overarching requirements: the elimination of systematic errors and the safe handling of random faults. Systematic errors are design flaws that occur during development and are addressed using a combination of rigorous design verification, certified design methodologies and intricate requirements planning. Random faults occur during device operation, due to radiation or electro-magnetic effects temporarily changing a stored value. Random fault protection requires incorporating fault-handling circuitry to allow recovery from failure without detriment to device operation.

Aeronautical Electronics Trends and Safety Standards

Safety-critical development is governed by regulatory standards that pertain to the specific application (See Figure 1). The International Electrotechnical Commission (IEC) governs many of these standards, including the automotive ISO26262, under the umbrella IEC61508. The DO-254 aeronautical standard is published by the Radio Technical Commission for Aeronautics (RTCA) and directs the compliance of complex electronic hardware in airborne systems. The standard specifies development flow certification, key compliance metrics, and requirement management.

Figure 1: Safety critical standards are created for specific applications.

Figure 1: Safety critical standards are created for specific applications.

Modern aircraft contain a plethora of electronic devices, which could cause catastrophic aircraft failure. Unlike the automotive sector, competitive pressures for new features are low and the complication of their development, extreme. As such, the industry exhibits a significant degree of reluctance toward changes in development practices.

The use of application specific ICs (ASICs), field programmable gate arrays (FPGAs) and programmable logic devices (PLDs) in aeronautical devices drove the necessity for the DO-254 standard. DO-254 focuses on design practices and systematic issues rather than random faults, simply because an aircraft is usually large enough to contain three identical, redundant components for each critical electronic system. Components operate concurrently and if the operation of one component varies from the other two, it is disregarded and shut down. This Triple Modular Redundancy (TMR) technique provides a failsafe solution to random faults.

Systematic faults are rigorously covered by DO-254, requiring advanced verification techniques throughout the development flow. It is here that formal verification is poised to evolve as an indispensable tool.

Formal Verification, Not Simulation

For the majority of complex device verification, simulation is the technology of choice due to its maturity, reliability and widespread use. Simulation has drawbacks, the most significant of which is the requirement for stimulus, often as complex as the design. If the stimulus is not written correctly, operational design aspects will remain untested, masking potential bugs.

Formal verification takes a different approach. It eliminates the stimuli requirement by calculating every state the design code can adopt. Engineers specify properties of the design, essentially asking operational questions, such as “Can sequence X ever happen?” or “Is the output value Y possible?” and similar. Any question will be exhaustively answered with no reliance on stimulus to hit on the right state. Furthermore, because assertions (that is, the specified properties) more directly relate to verification requirements, their successful verification is easier to catalog.

Formal Equivalency Checking in Aeronautical Electronic Development

FPGAs have become widely used in aircraft, offering significant benefits over processor-based solutions. Synthesis is used in FPGA flows to convert Register Transfer Level (RTL) code to gate netlists. In ASIC synthesis, the RTL register configuration is maintained, with optimizations applied to combinational logic. By contrast, FPGAs operate using fixed Look Up Tables (LUTs), which require a balance between registers and combinational logic. To achieve this balance, register configurations also are optimized, creating a verification issue.

The verification of synthesis optimizations is performed using Formal Equivalence Checking (EC) tools, which compare golden RTL representations with resulting netlists. Most EC technologies assume the same register configuration across compared code bases and focus on the relatively straightforward combination logic. In FPGA register optimization flows, the formal tool must analyze design functionality over multiple clock cycles—a far more complex proposition. This requires “sequential” equivalence checking (See Figure 2).

Figure 2: An FPGA combinatorial/sequential verification flow mixes equivalence checking with property checking to test for sequentially optimized code.

Figure 2: An FPGA combinatorial/sequential verification flow mixes equivalence checking with property checking to test for sequentially optimized code.

Specialized EC tools exist, including OneSpin’s EC-FPGA, which mix equivalence checking with advanced property checking to exhaustively test for sequentially optimized code. Essentially, the tool derives properties from the cycle-optimized RTL code, which is then sequentially proven on the netlist.

Formal Static Checking on Aeronautical System Design Code

Functional RTL code usually is verified using simulation, but static syntax-checking tools are also leveraged to weed out early bugs. These linting tools identify a broad range of issues efficiently, but are based on code syntax only with no account of code operation. As such, a large number of warnings are generated for correct code. These warnings often overwhelm the real errors, generating log files hundreds of pages long and hiding real issues.

Formal “Inspection” performs similar static checks, but also considers code operation by automatically generating assertions based on functionality. This formal application (app) will analyze code syntax issues, generating properties that describe intended operation to expose real errors. A good example is an array index out-of-bounds exception (See Figure 3). A syntax check reveals an array index larger than the number of elements, generating a lint warning. By checking code operation, formal inspection shows that no such access is made.

Figure 3: Formal can analyze code syntax and perform an array out of bounds operational static check.

Figure 3: Formal can analyze code syntax and perform an array out of bounds operational static check.

Summary and Looking Forward

Formal verification will continue to play a significant role for safety-critical verification. Although the inertial aeronautical industry leverages the technology for relatively straightforward tasks, formal use in automotive semiconductors is widespread, given its exhaustive nature. The aeronautical industry is likely to adopt these techniques as their device complexity grows.

Dave-KelfDave Kelf heads OneSpin’s marketing efforts and services as vice president of marketing. Previously, he was president and CEO of Sigmatix, Inc. He worked in sales and marketing at Cadence Design Systems, and was responsible for the Verilog and VHDL verification product line. As vice president of marketing at Co-Design Automation and then Synopsys, Kelf oversaw the successful introduction and growth of the SystemVerilog language, before running marketing for Novas Software, which became Springsoft (now Synopsys). He holds a Master of Science degree in Microelectronics and an MBA from Boston University.

Share and Enjoy:
  • Digg
  • Sphinn
  • Facebook
  • Mixx
  • Google
  • TwitThis