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
Jan 22, 2021
Amidst an ongoing worldwide pandemic, Samtec continues to connect with our communities. As a digital technology company, we understand the challenges and how uncertain times have been for everyone. In early 2020, Samtec Cares suspended its normal grant cycle and concentrated ...
Jan 22, 2021
I was recently introduced to the concept of a tray that quickly and easily attaches to your car'€™s steering wheel (not while you are driving, of course). What a good idea!...
Jan 22, 2021
This is my second post about this year's CES. The first was Consumer Electronics Show 2021: GM, Intel . AMD The second day of CES opened with Lisa Su, AMD's CEO, presenting. AMD announced new... [[ Click on the title to access the full blog on the Cadence Community...
Jan 20, 2021
Explore how EDA tools & proven IP accelerate the automotive design process and ensure compliance with Automotive Safety Integrity Levels & ISO requirements. The post How EDA Tools and IP Support Automotive Functional Safety Compliance appeared first on From Silicon...

featured paper

Overcoming Signal Integrity Challenges of 112G Connections on PCB

Sponsored by Cadence Design Systems

One big challenge with 112G SerDes is handling signal integrity (SI) issues. By the time the signal winds its way from the transmitter on one chip to packages, across traces on PCBs, through connectors or cables, and arrives at the receiver, the signal is very distorted, making it a challenge to recover the clock and data-bits of the information being transferred. Learn how to handle SI issues and ensure that data is faithfully transmitted with a very low bit error rate (BER).

Click here to download the whitepaper

Featured Chalk Talk

RF Interconnect for Wireless Applications

Sponsored by Mouser Electronics and Amphenol RF

The 5G revolution puts daunting demands on antenna technology. With massive MIMO and mm wave, 5g opens a whole new era in antenna solutions. In this episode of Chalk Talk, Amelia Dalton chats with Owen Barthelmes and Kelly Freeman of Amphenol RF about 5G antenna technology, and how Amphenol RF’s HD-EFI connector solution can help you with your next 5G design.

Click here for more info about Amphenol RF 5G Wireless Connectors