feature article
Subscribe Now

Acquiring More Addicts

Easing into Formal Verification

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.

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

10 thoughts on “Acquiring More Addicts”

  1. Pingback: GVK Biosciences
  2. Pingback: Agen Win
  3. Pingback: GVK BIO
  4. Pingback: Earn Money Online
  5. Pingback: friv
  6. Pingback: ADME Services
  7. Pingback: article
  8. Pingback: iraq Seo

Leave a Reply

featured blogs
Oct 23, 2020
Processing a component onto a PCB used to be fairly straightforward. Through hole products, a single or double row surface mount with a larger center-line rarely offer unique challenges obtaining a proper solder joint. However, as electronics continue to get smaller and conne...
Oct 23, 2020
[From the last episode: We noted that some inventions, like in-memory compute, aren'€™t intuitive, being driven instead by the math.] We have one more addition to add to our in-memory compute system. Remember that, when we use a regular memory, what goes in is an address '...
Oct 23, 2020
Any suggestions for a 4x4 keypad in which the keys aren'€™t wobbly and you don'€™t have to strike a key dead center for it to make contact?...
Oct 23, 2020
At 11:10am Korean time this morning, Cadence's Elias Fallon delivered one of the keynotes at ISOCC (International System On Chip Conference). It was titled EDA and Machine Learning: The Next Leap... [[ Click on the title to access the full blog on the Cadence Community ...

featured video

Demo: Low-Power Machine Learning Inference with DesignWare ARC EM9D Processor IP

Sponsored by Synopsys

Applications that require sensing on a continuous basis are always on and often battery operated. In this video, the low-power ARC EM9D Processors run a handwriting character recognition neural network graph to infer the letter that is written.

Click here for more information about DesignWare ARC EM9D / EM11D Processors

featured paper

An engineer’s guide to autonomous and collaborative industrial robots

Sponsored by Texas Instruments

As robots are becoming more commonplace in factories, it is important that they become more intelligent, autonomous, safer and efficient. All of this is enabled with precise motor control, advanced sensing technologies and processing at the edge, all with robust real-time communication. In our e-book, an engineer’s guide to industrial robots, we take an in-depth look at the key technologies used in various robotic applications.

Click here to download the e-book

Featured Chalk Talk

Consumer Plus 3D NAND SD Cards

Sponsored by Panasonic

3D NAND has numerous advantages, like larger capacity, lower cost, and longer lifespan. In many systems, 3D NAND in SD card form is a smart move. In this episode of Chalk Talk, Amelia Dalton chats with Brian Donovan about SD 3D NAND in applications such as automotive.

Click here for more information about Panasonic Consumer Plus Grade 3D NAND SD Cards