Commentary
Comment
sunilk_1
HarshM
nSys offers products and services for accelerating designs while lowering costs. ...
Protect your goal with post-silicon formal verification
Lawrence Loh
7/19/2010 8:03 PM EDT
SoC designers are learning the benefits of applying high-capacity formal verification techniques at every stage of the design. Our formal tools are powerful and versatile enough for a wide variety of tasks such as architectural exploration and RTL verification, all the way through post-silicon debug.
A good rule of thumb to consider how costly a missed bug can be: Finding bugs in model testing is the least expensive option; if it’s found in component test, add 10X to the cost; 10X more in system test; and another 10X if it makes it into production. You do the math. If you thought watching your team go down in the World Cup was depressing, try explaining to your boss how you let a bug loose in the field. Taking the analogy a bit further, using formal in the post-silicon lab is like having a really good goalie, because it’s the only method for finding, fixing, and verifying the fix to shave untold engineering-hours from the design cycle, and maybe even save a job or two along the way.
Post-silicon debug means trying to reproduce bugs seen in the lab using directed-random-simulation and emulation, but often these traditional approaches, unlike formal, are unable to root cause the bug fast enough. Let’s look at a fairly typical scenario.
When a problem is encountered at this late stage it can be hard to debug due to lack of visibility into the silicon in the post-silicon lab. You can find the problem but it is often abstract and not well understood: the chip hangs, not responding, dropping packets, sending out wrong output, etc. The first step is to try to determine exactly what is happening. Many chips have on-chip trace extraction capability, e.g., controls to freeze the chip when certain events are identified or on-chip logic analyzers that allow a selected group of signals to be muxed to external pins. This lets you extract a failure trace, capturing a limited number of signals for a number of cycles before (and maybe after) a problem is detected. The next step is to isolate and root cause the post-silicon bug. At this point it is known that the chip is exhibiting illegal behavior as it can be seen in the trace, but the trace represents the last N cycles of the run and it is not known how this state was reached. Typically, there will be a limited number of signals in the trace and it is difficult to choose the right set of signals to show the problem.

Figure 1 represents this dilemma: The last few cycles of the failing scenario can be observed, but how can the root cause of the problem be found? How can the designer know in which block the bug is located?
Typically, directed-random-simulation is used to isolate the bug, but can it reveal how this state was reached using simulation? It is not clear where the bug is happening as there is weak controllability in simulation and existing methods, but what is known is that it causes block D to act incorrectly. The bug happens after a 3-4 hour run in the lab when a certain kind of traffic is injected (e.g., only for read transactions on bus X). Finding the root cause with directed-random-simulation can be extremely difficult. If it takes four hours of real time with random traffic to hit the bug, how long will it take to reproduce it when simulation time is dramatically slower?
Next: Bug hunt


Robotics Developer
7/21/2010 6:36 PM EDT
I can see the value add for formal verification and would encourage it use. I do see that oftentimes there are resource constraints on the development team and adding another tool is great but requires: people resource, tool investment capital, and time to learn. I could see where many would opt out of the formal verification path only later to come to understand its value.
Sign in to Reply
MHK_#1
7/25/2010 5:01 PM EDT
I have to say I know and want to use formal verification method. I just don’t have an enough time to learn and set this environment. Most of verificationer spends their most of time in a pre-silicon verification. They are just plain busy in architecting and building testbench using simulation and a bit of emulation. In fact, that is what the upper management wants. In other word, no time allowed on another method to learn. Management has a stick to their habit not to go over their visible experience, unless they are forced to explored. Big problem! I am trying not do go in this path. Any easier or quicker way to get a good grip on this formal method?
Sign in to Reply
Alok78
7/29/2010 2:03 PM EDT
Yes, it is all about ROI, which management will understand. Jasper’s approach to formal verification is that there must be a positive return on investment from the very first project. We also provide deep applications support that brings verification engineers, and design engineers, up to speed fast without schedule impact. Using formal justifies the cost and time you mention in many ways, especially finding critical and corner-case bugs which cannot be detected in simulation. Jasper's formal solution can exhaustively verify all design scenarios without any input stimulus or a testbench and can save weeks, if not months of testbench development and random simulation effort, leading to increased confidence in the overall verification process. Jasper is also used across a spectrum of applications ranging from architectural exploration up to post-silicon debug. Jasper focuses on formal verification, it is not just one of many products, so we can really help you change and improve your verification approach. If you are finding that your management thinks there is never any time during, or in between, projects to use a new technology or tool, contact us and we can share some very convincing information on real-world ROI! Please visit http://www.jasper-da.com
Sign in to Reply
HarshM
9/15/2010 7:32 AM EDT
nSys offers products and services for accelerating designs while lowering costs.
nSys is perhaps the only company in the world focused on Verification. Customers are appreciating the option of getting all their VIPs from a single source without having to struggle with different licensing terms, agreements, APIs, simulator versions and training for every VIP.
Most customers also appreciate the flexibility that we offer. You can get annual licenses, Source code licenses and even Unlimited licenses.
We would like to understand how we can be of help in your Verification effort. We would also like to ensure that you do not ever have to develop a VIP and can get proven ones when you need them.
Sign in to Reply
sunilk_1
12/6/2012 4:07 PM EST
Please read my blog for another perspective on Formal Verification:
http://www.designconcommunity.com/author.asp?section_id=2774&doc_id=255322&
Sign in to Reply