The Safe Road Trip Thanks To Formal Verification

School’s out, gas is cheap and families in the U.S. are piling into their cars or minivans to take the time-honored cross-country road trip. These days, kids in the backseat don’t need to entertain themselves by spotting the license plates from the 50 U.S. states or picking a fight with their brother or sister. Instead, they can be kept amused with the vehicle’s sophisticated entertainment or Wi-Fi systems.

That’s just the beginning. It won’t be long now before the entire family will be able to sit back, relax and think of the old Greyhound Bus slogan “Leave the Driving to Us.” Or in this case, leave the driving to the autonomous vehicle.

Families in these driverless cars have the impossibly intricate electronic systems to thank for this welcome benefit. In turn, automotive suppliers have the indispensable ISO 26262 automotive standard and formal verification solutions to thank for ensuring their advanced technology is keeping passengers safe, no easy feat.

The functional complexity and silicon density of modern automotive electronic hardware components drive an increased risk of failure. Given the safety-critical nature of these components, failures, both systematic caused during development and random occurring during operation, must be eliminated as much as possible to get vacationing families safely to their destinations.

That comes from rigorous and highly automated development processes to reduce risk of systematic failures caused by human errors and inadequate development practices. Safety mechanisms monitoring hardware for abnormal behavior, caused by wear and tear or other physical effects, can lower random failures from happening.

Formal verification is not a new verification technique and formal property checking tools proved their value over the years for any number of hardware applications. Only recently, advances in ease of use and capacity for other more formal-based methodologies started capturing widespread adoption.

The ability to debug automotive and mission-critical applications may prove to be the most effective use of this technology. Formal solutions are central in many safety-critical hardware development flows, boosting the quality and efficiency of them, and play a significant role in implementing safety measures.

Formal methods are mathematical techniques and tools to specify, design and verify software and hardware systems, recognized as powerful approaches to uncover hardware design bugs that might otherwise escape simulation-based verification and lead to systematic failures.

One characteristic is the ability to examine design behavior exhaustively without the need for input stimuli, and prove that the design never deviates from its intended function as specified by a property or assertion. Simulation tools cannot achieve this level of precision for even the simplest design. A range of hardware development tasks has been improved through the use of formal verification-based solutions, ranging from register transfer level (RTL) design exploration and formal linting to end-to-end verification of critical modules.

Particularly relevant to safety-critical applications is the ability to finely control the injection of faults into hardware models and analyze their sequential effects. Formal verification tools have the potential to perform this task efficiently through both user effort and computational demands without the need for code instrumentation steps.

Formal tools provide significant value for the efficient development of automotive hardware. As complexity grows and engineers have to analyze the behavior of their designs under a wider range of workloads, including malicious inputs, formal verification will be used routinely to develop safety-critical hardware.

In the future, families flocking to the Grand Canyon in June will get there safely in their autonomous vehicles thanks in large measure to formal verification, the powerful technique to uncover hardware design bugs.