editor's blog
Subscribe Now

Using Formal to Help Simulation

While simulation is the granddaddy of verification, there are thorny problems that simulation doesn’t handle well, and formal analysis has gradually come of age over the years to attack those problems. So the two technologies end up working side by side on different issues to complete the verification plan.

While that is still largely true, Mentor has added a feature to their Questa verification platform to allow the formal part to help the simulation part. The formal part can help determine the simulation coverage; the feature is called CoverCheck.

The formal analysis engine can walk through the code and determine both unreachable code – you’ll simulate forever trying to reach that, with no improvement – and a sensitization path to hard-to-reach code. It’s essentially saying, “Don’t bother going here; you’re wasting your time. And for these other bits, here’s how you cover them.”

Unreachable code is dead code, and for some applications, dead code is verboten. Mission- and safety-critical design practices tend to require that every requirement be traceable to code and all code be traceable back to a requirement. So dead code, by definition, since it doesn’t do anything, can’t be tied to a requirement. While Mentor isn’t aware of anyone taking this next step yet, CoverCheck could be used to excise such code.

In addition, they’ve added a more classical formal feature called AutoCheck. It looks for common problems in the code (think “lint,” but different problems). Examples of the things it can verify are X-propagation, combinatorial loops, state machine deadlock, and overflow.

Both CoverCheck and AutoCheck are push-button automatic.

Finally, they announced performance improvements in their clock-domain crossing (CDC) formal capability.

You can find more in their release.

Leave a Reply

featured blogs
Dec 5, 2019
In November, we wrapped up our technical debt cleanup, upgraded several of our back-end APIs, and rolled out several small user-experience updates throughout Samtec.com. These updates will pave the way for some exciting new applications and e-e-commerce features in 2020. Here...
Dec 5, 2019
Hello everyone! I am Aravind R, Principal Support AE at Cadence, and I have been supporting various users at our customer sites to generate and validate various formats of standard cell and IO... [[ Click on the title to access the full blog on the Cadence Community site. ]]...
Dec 4, 2019
At their recent Open Innovation Platform (OIP) Ecosystem Forum held in Santa Clara, CA, TSMC named Mentor as their OIP Partner of the Year in four categories during the awards luncheon: Joint Development of 6nm Design Infrastructure Joint Delivery of SoIC Design Solution Join...
Dec 4, 2019
Any reasonable thinking being knows that the Earth cannot possibly be flat -- if it were, cats would have pushed everything off it by now!...
Nov 29, 2019
[From the last episode: We saw what it means for an electronic system to sleep.] You'€™re on a phone call having a conversation, and you hear the sound that indicates that someone else is trying to call you. So excuse yourself to the person you'€™re talking to and quick t...