Formal Verification Of AI Processor Datapaths In Automotive Applications

There aren’t many electronic applications that require correctness, safety, and security more than automobiles and other road vehicles. Owners rely on their cars operating properly and reliably at all times. The very lives of drivers, passengers, and those nearby are at risk if a vehicle misbehaves.

The situation grows more serious with every innovation in automotive electronics. With a modern advanced driver assistance system (ADAS), the car is in control during portions of the driving time. The driver may have time to correct an unsafe situation, but this is less and less possible as the level of autonomous operation grows.

By the time that truly self-driving vehicles arrive, it is likely that there will be no manual controls at all, so human intervention will be impossible. Everything will rely on the correctness of the electronics design, and on the safety and security of the system.

An alpha particle flipping a memory bit or silicon aging effects must not compromise operation. Functional safety standards such as ISO 26262 mandate that faults be detected and either corrected or neutralized. Further, the system must be safe from attacks by malicious agents that can endanger lives as surely as a chip failure.

These strict requirements put enormous demands on the process of verification for automotive electronics. Engineers must be certain that their designs are correct, safe, and secure long before they are deployed in the field. Unfortunately, the same trends that make verification more important, including ADAS and self-driving, are also making designs much harder to verify.

Cars now contain much more than servos and simple microcontrollers. The chips used in today’s electronic control units (ECUs) are some of the largest and most complex in the world. They include highly sophisticated processors with parallel datapaths and deep pipelines. Artificial intelligence (AI), particularly machine learning (ML), plays a huge role in advanced transportation systems and requires powerful processors.

When the need for certainty arises, chip development teams think of formal verification. Unlike simulation-based testing, formal algorithms prove that a design is correct under all possible scenarios. This guarantees that the verification team has not forgotten to write a specific test and thereby missed a design bug because some bit of functionality was never checked.

Applying formal verification to the complex pipelined AI processing chips used in modern automotive electronics may not be an obvious solution. Historically, formal methods have been seen as more appropriate for control logic than for datapaths.

However, a bug in a datapath could result in chip misbehavior just as surely as an error in a state machine. There are well-known examples of design flaws where a tiny percentage of the operands for a particular arithmetic operation produced the wrong answer. In an automotive chip, one wrong answer can result in catastrophe.

When engineers talk about formal verification, they usually have in mind proving that the design matches a set of assertions, or properties, defining the intended behavior. This approach works well for control logic but is more challenging for datapaths. With arithmetic operations, there are a huge number of paths between inputs and outputs, so mathematically considering every possible scenario is computationally intensive.

Fortunately, it turns out that there is an easier way to verify AI processor datapaths in ECUs. Formal algorithms can be used to prove that the register transfer level (RTL) design matches a specification written at a higher functional level in C/C++. Such reference models already exist in virtually every chip project since they are used for architectural analysis and software development.

A recent webinar presented an example of using a formal solution to verify a finite impulse response (FIR) filter, which accumulates a series of multiplication results. Such a filter might appear in automotive electronics as part of the radar system that provide insight into the surrounding environment and gauges distance from nearby objects. A FIR filter is representative of other types of datapaths because its final result depends upon previous results.

Another interesting aspect of FIR filters is that they can be implemented with all the multipliers in parallel, with a single multiplier reused over multiple cycles, or as a hybrid of the two. Formal verification is equally applicable to all these implementations. The FIR4 design used in the webinar contains four multipliers. Since these are identical, the approach chosen first verified a single multiplier and then applied that result to the full design.

The functionality of the multiplier can be expressed in C/C++ simply as “a * b” where the variables represent the multiplier and the multiplicand. The Synopsys VC Formal solution and its Datapath Validation (DPV) App were used to prove that the RTL implementation of the multiplier matched the C/C++ expression. This required minimal setup, primarily just mapping the input and outputs between the two presentations.

Once the multiplier was proven correct, an assume-guarantee methodology was used on the overall FIR design. By assuming that each multiplier’s output was the product of its inputs, the details of the RTL implementation were abstracted out. The resulting formal analysis of the remaining RTL was highly efficient and proved that the overall FIR design matched the C/C++ reference model of the intended functionality.

This approach is very flexible, supporting both hand-written C/C++ models and those generated by the MathWorks MATLAB environment. All common datapath operations are supported, including addition, subtraction, multiplication, division, and square root. The assume-guarantee methodology extends the solution to any complex design, including CPUs, GPUs, DSPs, and the convolutional neural networks (CNNs) common in AI/ML applications.

Synopsys VC Formal DPV provides exhaustive validation for datapath designs, including those in ECUs and other critical applications. Developers can achieve datapath signoff without any testbenches required. For more on this industry-leading solution, and full details of the FIR filter verification example, watch the webinar here.