Last summer we took a look at the fact that formal verification is seeing something of a repositioning and resurgence. The holiest of holies is the ability to verify that all possible use cases of a piece of logic have been specified and that all possible outcomes of those use cases have been verified to operate as desired.

It can be viewed as a big jump from no formal verification to the complete set; it’s a change to the design flow, and we all know that the hardest thing to bring about is a methodology change. One of the players in this field, OneSpin Solutions, has brought some marketing magic to this problem in order to make formal more accessible to more designers. I’m sure they wouldn’t want to think of it this way, but they’ve realized that they need to apply a series of gateway drugs to get you hooked, rather than approaching you straight-off with a big-ol’ honkin’ scary-lookin’ needle. Of course, this would imply that formal verification is addictive but harmful and will ultimately be your undoing. As this isn’t the intent of the metaphor, perhaps we should think of it as Helpful Heroin.There is an addiction center san bernadino that can help with overcoming the issues of addiction.

Or, instead of a drug metaphor, we could view it as Frying the Frog – turning up the temperature ever so slightly without the frog noticing and jumping away. Not sure that’s a much happier picture… So we’ll stick with addiction. I just can’t seem to escape it.

One of the barriers to the use of formal is the need to learn SystemVerilog Assertions (SVA) – these are the means by which you can specify your intent. With your intent in place, the tool can then confirm whether or not the RTL correctly achieves that intent. You can think of these as test vectors. When doing tests, the correspondence between RTL and assertions may match exactly, or there may be assertions that are not achieved by the RTL, or the RTL may do things that aren’t found in any of the assertions.

The first of these three cases is what OneSpin refers to as “gap-free” – there’s no difference between intent and actual RTL (assertions = RTL). That’s generally a good thing. The last two cases reflect the existence of gaps. Either the RTL is missing some functionality (assertions > RTL), or the code is doing something extra (RTL > assertions). In the latter case, that could mean that the assertions were incomplete, or it could mean that the RTL is having unintended consequences. Either case merits attention.

OneSpin has graded the ascendency to full formality into six steps (packaged into five product levels, since one pair of them are combined into a single product), requiring progressively more involvement from the designer to achieve full benefits. They refer to the overall family as the 360 MV family, and each of the five members has its own name and increased set of capabilities (for, I would suspect, an increased price… anyone wanna bet against that?)

The first level, 360 MV Inspect, requires nothing of the designer at all. No assertions are needed, and the tool just checks for errors and performs optimizations. It really doesn’t feel like formal verification, which suits OneSpin’s needs just fine, since it leads you unsuspectingly to…

The second level, 360 MV Check, starts to involve assertions. Assuming you are new to them, it requires the use of only the simplest ones. Here you can check for correctness of data types or verify that signal levels are correct. You can decide which assertions to write and which to omit; you’re really just confirming basic properties of the micro-architecture. No testbench is required to check the design at this level, and there is no concept of “completeness.” Intended to feel painless, making it less noticeable when you wake up and find yourself…

At the third level, 360 MV Verify, you can check out complete protocols using more complex assertions. Unlike the Check product level, here a complete set of assertions is needed to cover a given protocol. You may be specifying sequences of events related by timing with a wide range of options. Essentially, you’re checking out what may be complex state machines, and you need to make sure all states (legal and illegal) and transitions (legal and illegal) are covered, at least in theory. More complex debugging is also required in order to relate any detected errors back to the RTL creating the error and the assertions that were violated.

The Verify product actually incorporates two of the six verification levels OneSpin defines. The first of these two is the confirmation that protocol requirements are met. This is one way of specifying how a protocol should work, and it relies solely on assertions. The next level is a capability they refer to as Design Operation verification. It refers to the ability to specify and test specific operations like reading or writing across a bus. You’re not necessarily testing different things as compared to requirements verification; you’re just doing it from a different viewpoint. While the requirements approach involves assertions, the operations approach includes timing diagrams with an associated assertion library. The idea here is to make it easier to create complete testbenches.

You can probably imagine that some of the more complex protocols may require a rather hefty set of assertions in order to completely specify their intended operation. Fully-defined protocols may actually come with their own set of assertions. In this case, the work is even easier, since the code can be immediately verified against those assertions without the need to translate the protocol into assertions yourself. As a note to protocol committees, having assertions included as part of the spec may be a good way to accelerate acceptance of the protocol as well as to confirm that there are no ambiguities in the spec.

The first three levels of functionality, OneSpin will agree, are capabilities that are available in a variety of tools; they are not unique to OneSpin. However, they are the gateway drugs that will hopefully lure you, little by little, over time, into the hard stuff that only OneSpin provides. The three higher functional levels that they identify (one being the operations level already included in the Verify product) they claim as capabilities that can be found nowhere else. So hopefully you’re well acclimated as you arrive at…

The next higher level is called 360 MV Assure; this is where things start to look a bit more like what we think of as more general formal verification and where automatic gap detection starts to play a role. This level of product automates some of what happens in the Verify level by identifying missing assertions. In other words, if the RTL is doing something that the assertions don’t cover, it’s flagged so that assertions can be added (or the RTL can be changed so it doesn’t do whatever thing it’s not supposed to be doing). And of course, once you’re here, it’s only one more step to…

The final level, called 360 MV Certify, is their full-blown flagship product; it’s the crack to which the other levels will inexorably lead you, assuming that your dopamine and serotonin receptors have been suitably rewarded all along the way. This level encompasses their full range of tools to ensure that no gaps exist in the design and to build a comprehensive testbench that can follow the design through to production.

It’s hard to argue that full gap-free verification isn’t a good thing. But, practically speaking, there’s always been a cost barrier associated with it (both in effort and in currency) that has proven tough to surmount. Whether OneSpin has found a way to ease the world into it more smoothly or whether they’re ahead of the game has yet to be proven. Especially in these times, there’s a delicate tension between the need to do more with less and the need to conserve cash. When it costs some cash to do more with less, well, it’s not always clear which side will prevail – productivity or cash.

Of course, we can only hope that the attraction of formal won’t be so compelling that users get so addicted that they resort to petty theft, burglary, and other nefarious means to sustain their productivity habit when the cash runs short. If you start noticing shady-looking nerds hanging out in unoccupied cubicles or in the loading docks of newly-vacated tilt-up low-rise buildings in high-tech industrial parks, then you’ll know things have taken a turn for the worse.

Link: OneSpin 360 MV