Site icon The Foretellix CTO Blog – AI safety

Is a Universal Verification Framework possible?

Yoav Hollander

Summary: This post investigates the (slightly crazy) idea of creating “one universal verification framework for everything”, and claims that while the goal itself is probably impossible (for now), some interesting and worthwhile sub-goals are perhaps possible.

As many people (including myself) have discussed before, there is no single “verification community”: there are really many verification “tribes”, corresponding to verification areas (mainly split mainly by industry, but also by other factors). They have different terminologies and different belief systems (about what’s important and how to do things).

So the current state of (multi-area) verification looks like this (details of the various areas will be given later):

This blog is trying, in a small way, to remove that cloud (e.g. via the terminology page). But why stop there?

So here is a funny question: Can a “Universal Verification Framework” (UVF) be constructed? I mean an actual, single tool / tool-suite which will work (with suitable “plugins” and options) for most of those areas/tribes?

In other words, is the following picture possible:

At first glance (and perhaps at all subsequent glances 😉 ) this looks fairly crazy. It may not even be possible to create a single-industry verification framework, let alone a multi-industry UVF.

Those industries are very different in their verification practices and those differences are not just arbitrary, historical whims. For instance, it makes sense for security verification to concentrate on “negative testing”, while everybody else mainly does “positive testing”. Similarly, Machine Learning verification has to be black-box, because Machine Learning systems are, almost by definition, opaque. And so on.

So this is a crazy idea. But I find it an interesting crazy idea: I think we can learn a lot from investigating it. And there are very good reasons wanting it to succeed (e.g. the fact that complex systems are increasingly composed of multiple areas). And even if UVF itself is impossible, perhaps we can at least move along the arrow marked “progress” below:

BTW, IBM’s Haifa Research Lab sort-of went for option 3: They developed a team, a methodology and some SW modules (a constraint engine, a coverage engine, an analytics engine etc.), and used those to create multiple verification tools for different areas (in HW, SW and security). See for instance here.

The rest of this post is organized as follows:

Notes:

 The various areas and how they are different

Here is a short, superficial list of some of the related industries, and how their verification practices differ:

Why a UVF is probably impossible (for now)

As we saw above, the various areas are pretty different, verification-wise. So if we want to do something which will work for all of them, we’ll have to go to a least common denominator. And the obvious common denominators (e.g. a C compiler) hardly count as pieces of a UVF.

Also, trying to force things into a framework can lead to lovely inventions like the mini-car / kitchen-blender combo (“Why would anybody want to buy two separate multi-speed engines?”).

Another reason why UVF may never happen is that there are already a bunch of alternatives to it:

Why UVF may still happen (in some sense)

 While there are excellent reasons to suspect UVF is impossible, there are also strong (and growing) reasons for UVF. The main ones are:

And now for the details:

As verification becomes more important, UVF becomes more compelling: There is sort of a “Maslow’s hierarchy of verification needs” (like Maslow’s hierarchy of human needs). Consider the following figure:

Many of these areas are fast-moving fields. The leading lights there are busy inventing the design side of the area, with verification playing second fiddle. But if / when verification becomes more important, UVF will suddenly look a lot more attractive.

Take autonomous vehicles: As far as I know, AV verification is currently a lot less than 50% of the AV engineering effort. This is not because these guys don’t care about safety: In fact, they expend a lot of effort into safety (better vision algorithms, better reaction logic and so on). It is just that safety verification still plays second fiddle.

This is probably the right trade-off for now. But it could change fairly quickly. Here is one way this could happen:

As this happens in more and more areas, regulators / lawmakers may also push for uniform ways to assess safety and quality-of-verification, and thus for uniform multi-area terminologies, concepts and rules: To avoid confusion, it makes sense to have similar rules and terminologies for e.g. AVs, civilian UAVs and domestic robots (where applicable).

It succeeded in one area (HW modules): In the HW modules area, there is a single, agreed-upon technique for verification (CDV), as represented by Hardware Verification Languages (HVLs). There is even (to a lesser extent) a single agreed-upon methodology (UVM).

This started about 20 years ago, and is now an acknowledged fact: most module verification is done that way, in spite of the fact that the verified modules / subsystems are extremely different from each other: Ethernet controllers, ALUs, cache subsystems, anything – even analog HW blocks are (slowly) joining the fold.

And if you say “wait, that’s just one area, not multi-area”, I’ll forgive you – you are simply too young to remember how these different HW module kinds seemed like different kingdoms at the time.

Note that a similar unification is starting to happen in the area of SoC/LL SW. Further, the unified result may end up having some similarity to CDV.

UVF can save a huge amount of repetitive effort: The CDV revolution mentioned above brought extreme savings, removing waste in training, documentation, tool creation, integration of multi-module verification environments, and so on. These savings point the way to what may be possible with UVF, if we can do it.

And the higher up an area climbs in that Maslow hierarchy, the bigger the savings: So now they also want fancy failure clustering? Check. Automatic selection of tests based on change to the DUT? Check. The huge matrix of fancy-verification-function cross verification-sub-area, currently being randomly filled by research and industry, could be replaced by a single best-of-breed vector.

Bigger systems need multiple areas: Consider AVs again. While they belong to the IAS area, they actually need multiple other areas:

If each of these has its own, very-different-and-incompatible verification framework, then:

UVF will take a big step towards solving those problems.

Many of the differences are not absolute, but rather a matter of degree: What may look like a binary difference (some areas need it, others don’t) often emerges to be something other areas also need, except to a lesser degree.

For instance, security is about negative testing and everything else is mainly about positive testing, but negative testing (what the DUT does upon erroneous input) is still pretty important for other areas.

Thus, the next chapter will go through some of the differences and discuss how they could be reconciled in a tentative UVF.

Reconciling the verification differences between the areas

Here are some verification dimensions on which verification tribes differ. For each of these, I suggest how UVF should handle the conflict.

Summary

 UVF seems impossible (for now), and yet perhaps necessary (eventually). What should be do about it?

My own intuition is that upside is too big to miss completely, so we should do something about it. Here are some ideas:

Comments are very welcome.

Notes

I’d like to thank Ziv Binyamini, Sandeep Desai, Yaron Kashai, Amiram Yehudai and Matan Vax for reviewing previous drafts of this post.

17-Nov-2015: My HVC 2015 presentation about this is available here.

 

Exit mobile version