The Many Flavors of Equivalence Checking: Part 4, How SLEC Brings Automated, Exhaustive Formal Analysis to Safety Mechanism Verification
[Preface / reminders: Part 1 of this series focused on synthesis validation with LEC and SLEC, Part 2 describes how SLEC brings automated, exhaustive formal analysis to ECO/bug fix verification, and Part 3 talked about Low Power Clock Gating logic verification
While the advent of autonomous vehicles has sparked new interest in verifying the robustness of safety critical systems when struck by random faults, this has long been a challenge for medical devices, avionics, and anything that has what is politely referred to as a “high cost of failure”. Whatever the end-application, the overarching goal is for the given product to detect the incoming fault(s), and then react in a safe manner. Depending on the system and its environs, sometimes just detecting and reporting a fault to the user is all that’s needed. Of course there are many cases where it must also continue to safely operate in some automated manner; at least long enough to execute a safe shutdown sequence.
Digging down to the RTL digital design level, the circuitry that handles these functions is commonly called a safety mechanism. At a minimum this logic needs to detect any faults – whether they come from signals that literally get stuck (from various decay or damage phenomena over time), or from transient effects (electronic noise, temperature effects, moisture, even stray cosmic rays!). Next, depending on the system’s requirements, this logic can also support “fail safe” operation; potentially even “absorbing” the fault and keeping everything running as if nothing happened. Fortunately, there are many popular and effective safety mechanism designs that will put you in the ballpark of your particular application’s requirements (ECC, CRC, TMR, and so on). But as with all designs, (paraphrasing) the devil is in the verification.
The traditional safety mechanism verification approach is intuitive: an EDA tool will systematically introduce fault signals into carefully selected points in the Verilog, SystemVerilog, or VHDL model of the Device Under Test (DUT); and a testbench monitors whether the safety mechanism reacts property depending on the passage or failing of the corresponding directed or constrained-random tests.
Putting aside for the moment the tremendous challenge of selecting where exactly to apply faults in the circuit to achieve the highest level of verification per the test, and/or to meet regulatory specifications (a process well-explained in this white paper), the simulation testing process itself is inherently not exhaustive. No matter how well constructed your simulation testbench may be, there is still the chance that a fatal corner-case goes undetected. Clearly this a big problem when the name-of-the-game in safety-critical verification is to achieve perfection.
Enter an Exhaustive, Formal-Based Approach
As outlined by Figure 1 below, the formal-based Questa SLEC tool can be applied to exhaustively verify a safety mechanism’s ability to detect and mitigate faults.
Specifically, recall that Questa SLEC exhaustively compares the behavior of two blocks of RTL code. In this flow, “RTL A” is the regular DUT and the safety mechanism logic with NO faults, and “RTL B” is “RTL A” WITH faults added. Simply stated, if any difference in behavior is detected between the A and B, it means there is a flaw in the safety mechanism logic to mitigate the injected fault(s). (The “Fault Generation and Reduction” aspect that complements this flow is described in detail in the aforementioned whitepaper) Not only does this analysis run significantly faster than other approaches (and you don’t have to spend any time writing a testbench), it is exhaustive thanks to formal algorithms being used under-the-hood.
As you might imagine, many of the customers that are using this flow are a cross-section of automotive semiconductor suppliers, and companies that are eager to break into this market. The common thread is the need for an exhaustive formal analysis – without having to learn formal itself, and letting the automation take care of the details so they can focus on the bigger picture.
But Wait, There’s More …
This series of posts have covered a lot of ground, showing how just this one type of automated formal technology can be used to quickly (and exhaustively) address a very wide variety of verification challenges better than any other approach. (And I didn’t even cover some of the more prosaic Questa SLEC flows, like exhaustively verifying Verilog and VHDL implementations of the same IP behave identically) In Part 5, I’ll tabulate all the flows for quick reference.
Until then, may your power consumption be low, and your throughput be high!
Joe Hupcey III,
for the Questa Formal team
Reference links:
Verification Academy White Paper: Formal Techniques for Optimizing ISO 26262 Fault Analysis
Verification Horizons, June 2018: It’s Not My Fault! How to Run a Better Fault Campaign Using Formal
Tech Design Forum, June 2018: Formal fault analysis for ISO 26262: Find faults before they find you
Part 1: Synthesis Validation with LEC and SLEC (a/k/a the Most Popular Formal Apps Ever)
Part 2: How SLEC Brings Automated, Exhaustive Formal Analysis to ECO/Bug Fix Verification
Part 3: How SLEC Brings Automated, Exhaustive Formal Analysis to Low Power Clock Gating Verification
