Bridging the Gap Between Modern, Rigorous FPGA Development Flow and DO-254/ED-80
Focusing on functional verification, this article introduces state-of-the-art formal equivalence checking solutions for field programmable gate arrays (FPGAs) and makes a case for their applicability to AEH development.
DO-254 is the standard for design assurance guidance for airborne electronic hardware (AEH). The Radio Technical Commission for Aeronautics (RTCA, Inc.) originally published the standard in 2000. In 2005, the Federal Aviation Administration (FAA) officially adopted DO-254 as an acceptable means of compliance for the design of complex AEH. The European counterpart of DO‑254 is the European Organization for Civil Aviation Equipment (EUROCAE) ED-80. The European Aviation Safety Agency (EASA) permits applicants to use ED-80 to comply with its AEH certification specifications. The two documents are technically equivalent.
DO-254 imposes a strict, rigorous development process (Figure 1) based on defining clear requirements and accurately tracking their implementation and verification. Considered an objective prescriptive standard, DO-254 focuses—at least in principle—on prescribing what shall be achieved, rather than how to achieve it. This is only partly correct in theory, and even less so in practice: the reality is that mature technologies routinely applied for the development of hardware for both consumer and safety-critical applications, such as those used to develop automotive advanced driver assistance systems (ADAS), are not yet mainstream in avionics. This is partly because achieving DO-254 compliance poses a feared and crucial challenge to AEH development projects. Adhering to technical solutions more readily accepted by auditors reduces the risk of delays.
Industry and authorities are aware of this dangerous, widening gap between technology and certification practices. SHARDELD, a study commissioned by EASA and published in 2012, presents a comprehensive analysis of state-of-the-art tools for hardware development. The study details what technologies are routinely used in DO-254 projects and evaluates tools that have widespread adoption in the semiconductor industry and might be considered for AEH development. In North America, and also in Europe with the Re-Engineering and Streamlining Standards for Avionics Certification (RESSAC) research project, there are efforts underway to streamline the certification process. The aim is to define domain-independent objectives (overarching properties) that all certifications must satisfy, along with criteria for how the evidence against these objectives shall be assessed. This approach would replace numerous avionics standards and enable a flexible certification platform more suited to accommodate modern technical solutions.
The Gap between Certification and Verification
As hardware continues to increase in complexity, engineers need state-of-the-art tools and methods to deliver high quality, safe hardware within budget and time constraints. Constrained random coverage driven simulation, for example, is the modern bread and butter verification methodology to unveil unexpected functional scenarios and measure verification progress. Compared to directed testing, however, this methodology makes it harder to map verification artifacts to requirements. It is, therefore, rarely applied in DO-254 programs.
Engineering teams work around certification obstacles. Certain solutions deemed necessary from the technical perspective might be excluded from the certification flow to avoid disrupting the certification process due to tool qualification issues, for instance. Advanced design implementation optimizations might be switched off. FPGA synthesis tools, for example, can perform sequential logic optimizations like retiming. These optimizations carry a higher risk of introducing errors in the design and require adequate verification. This defensive attitude may support arguments towards certification, but it also reveals an overall lack of confidence in the verification flow.
As design progresses, robust verification steps target bugs that might have been introduced by the previous design development step. Requirements based tests do not target potential bugs introduced by the synthesis tool, and are not intended to gain confidence that a certain tool option is working correctly. Finding such bugs during gate level simulation (GLS) or during on-board testing is a stroke of luck, not the result of systematic verification of the synthesis tool output. Thankfully, electronic design automation (EDA) tools are well tested. That said, although silent bugs are rare, they can have dire consequences, particularly in the case of tools that can corrupt the design.
An efficient verification flow catches bugs as soon as possible once they come into existence. Finding a bug in the register transfer level (RTL) model during GLS is costly and highlights deficiencies during RTL verification. Similarly, tracing back an on-board testing failure to a netlist bug introduced by the synthesis tool is both difficult and time consuming.
At present, the most efficient and rigorous verification method to confirm that RTL functionality is preserved during implementation steps, including synthesis and place and route, is formal equivalence checking (EC). Formal technology enables the exhaustive analysis of all input stimuli. Formal tools make no difference between a huge synthesis bug that would cause all simulation tests to fail, and a deep corner case one that could be missed even by extensive GLS and on-board testing. Moreover, debugging failures is much faster. GLS and on-board testing are no substitute for EC.
Sequential Equivalence Checking for FPGAs
Engineers have been applying combinational EC (CEC) routinely in the development of application specific integrated circuits (ASICs) for over fifteen years. Nowadays, virtually no chip reaches production without running formal CEC. This technique relies on mapping the states of two design representations and comparing the logic functions driving each state pair. Formal tools suffer from capacity issues, and state mapping transforms the intractable problem of comparing two large sequential designs into the simpler problem of comparing many small combinational logic cones.
Synthesis tools mapping an RTL design into a specific FPGA family use advanced optimization techniques, including tristate pushing, register duplication, retiming and pipelining. Moreover, safety goals might require the insertion of safety mechanisms like triple modular redundancy (TMR). One-to-one mapping of states is not possible in FPGA flows. Advanced design manipulations increase the risk of introducing errors. The 2016 Wilson Research Group functional verification study found that 75% of safety critical FPGA projects had bugs that escaped to production (this figure includes RTL coding errors).
Nowadays, formal EC is also possible in FPGA projects, thanks to sequential EC (SEC) algorithms that do not need full one-to-one state mapping. In theory, SEC only needs a map of the inputs and outputs of two designs. In practice, tools must be smart in automatically locating the areas where one-to-one mapping is preserved and apply faster CEC algorithms where possible (Figure 2). EC FPGA tools must be independent from synthesis tools and ideally come from a different vendor. However, support for specific device vendors and families is required to automate time consuming, tedious tasks.
EDA tools for EC FPGA are available on the market. OneSpin Solutions is a provider of formal EC tools for ASICs and FPGAs. In 2005, OneSpin started to extend its CEC technology with SEC algorithms. Today, OneSpin has well established relationships with Xilinx, Intel Programmable Solutions Group (formally Altera), and Microsemi. Its EC FPGA solution has been applied to hundreds of projects, including many for safety-critical applications.
Equivalence Checking in the Certification Process
Ideally, applicants should be able to claim certification credit to the authorities for all technical activities performed as part of a DO-254 program. EC can be used for independent output assessment of synthesis and place and route tools. Moreover, EC paired with static timing analysis (STA) provides arguments to port requirements verification credit obtained at the RTL level to the place and route netlist. With this approach, back-annotated GLS—usually slow, hard to debug, and generally effort intensive—could be reduced significantly.
A tool used to claim credit for a DO-254 activity must be qualified. It might be possible to claim independent output assessment of the EC tool by leveraging limited GLS and testing on the physical device.
Certification processes must serve the ultimate goal of producing safe AEH. Complex hardware development needs state-of-the-art functional verification solutions that detect bugs soon after their introduction. Formal EC is the most rigorous, efficient method for detecting functional bugs introduced during implementation steps such as synthesis or place and route. This technology is mature and routinely applied in several domains, including automotive. SEC algorithms, paired with dedicated vendor support, make this powerful technology easy to adopt in FPGA flows.
No solution is perfect, and in general, verification benefits from redundancy: the more the better. Arguments claiming that formal EC is not enough for DO-254 projects can be made with relative ease, but arguments maintaining that GLS and on-board testing are enough to detect potential errors introduced during synthesis and place and route are not technically sound. Rejecting formal EC based on difficulties in integrating it in the certification process can only highlight shortcomings in DO-254 and the certification process itself. Engineers need formal equivalence checking for efficient, rigorous verification of AEH implementation steps.
Sergio Marchese is the Technical Marketing Manager at OneSpin Solutions. He started his career at Infineon Technologies, applying coverage-driven constrained-random simulation and formal methods to verify the TriCore CPU, an architecture widely used in today’s automotive SoCs.
Over the past 16 years, he has worked on solutions in many domains, including communications, consumer, industrial and aerospace, in an effort to leverage the most advanced formal tools and methodologies to implement rigorous and efficient hardware development flows.
Marchese has also built and managed state-of-the-art teams, successfully signing off complex hardware designs solely using formal verification.
Tags: top story