by Bryon Moyer, EE Journal
For years, when we have thought “functional safety” or “safety-critical design,” we’ve pictured airplanes, spaceships, and weapons. All of these systems rely on tons of electronics, and they have to work properly or else bad things happen – either lots of time and money lost or lives lost.
And so, for years, the “mil/aero” world has been its own special thing. Some companies specialize in that business because margins can be good. Others stay away because design cycles are long and unpredictable, and there can be tons of paperwork – and who needs that, right?
Meanwhile, OneSpin has also newly addressed this space. Their approach to dealing with systematic errors harkens back to messaging they were using many years ago: gap-free verification. This gets to the notion that, given a set of design requirements, the design should behave in a way that meets all the requirements and nothing more than those requirements. Every element of the design should be necessary and sufficient. Any behavior that lies outside those specified in the requirements become an issue. So, clearly, this is something that OneSpin has cut its teeth on.
For random errors, however, they have an approach different from – and potentially complementary to – Austemper’s. OneSpin’s Dave Kelf noted that, after simulation-based fault analysis, there typically remain on the order of a couple hundred uncertain faults that need to be checked manually. And real-world speed is such that one can address roughly one such fault per day. But, of course, OneSpin does everything using formal analysis rather than simulation, so this issue goes away.
OneSpin has three applications for handling random errors. FPA starts by pruning non-propagatable faults from future analysis. After all, if a fault occurs and it never gets to or affects an output, did it really happen? Truly navel-gazing stuff, but, from a practical standpoint, time need not be spent on such faults. You could say that such faults are self-handling.
FLA then looks at fault-handling circuits to prove that they work. OneSpin had to add some functionality to their tools to make this second tool work – something that might sound trivial: force and release. Those are, in fact, trivial to do in a simulator, because they’re event-based commands that blend well with a simulation mindset. But they’re not so obvious with formal verification – and yet they were necessary for proving that an injected fault can be handled.
Finally, they have FDA, which quantifies fault coverage. It still requires some time to run – weeks for a large-scale design – but there’s no need to generate scenarios or vectors, as is needed with simulation. And there’s none of the uncertainty and dispositioning that are required for simulated faults, saving literally hundreds of engineer-days.
There’s even some talk with Austemper to see whether a formal engine might be more effective than simulation for Austemper’s Kaleidoscope tool. This is the “complementary” bit that I referred to. It’s not certain whether this will happen, but it shows how different solutions may overlap in constructive ways.