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
May 27, 2020
Could life evolve on ice worlds, ocean worlds, ocean worlds covered in ice, halo worlds that are tidally locked with their sun, and rogue worlds without a sun? If so, what sort of life might it be?...
May 26, 2020
I get pleasure from good quality things. Quality is a vague term, but, to me, it is some combination of good design for usability, functionality and aesthetics, along with reliability and durability. Some of these factors can be assessed very quickly; others take time. For ex...
May 26, 2020
#robotcombat #combatrobots #robotwars #WeWantSeason5 #WeGotSeason5 These are some of the most popular hashtags used by a growing number of global BattleBots enthusiasts. Teams from all backgrounds design, build and test robots of all sizes for one purpose in mind: Robot Comba...
May 22, 2020
[From the last episode: We looked at the complexities of cache in a multicore processor.] OK, time for a breather and for some review. We'€™ve taken quite the tour of computing, both in an IoT device (or even a laptop) and in the cloud. Here are some basic things we looked ...

Featured Video

DesignWare 112G Ethernet PHY IP JTOL & ITOL Performance

Sponsored by Synopsys

This video shows the Synopsys 112G Ethernet PHY IP in TSMC’s N7 process passing the jitter and interference tolerance test at the IEEE-specified bit error rate (BER). The IP with leading power, performance, and area is available in a range of FinFET processes for high-performance computing SoCs.

Click here for more information

Featured Paper

Choose the Ideal Bluetooth Protocol for Your Design

Sponsored by Maxim Integrated

Most people do not understand the difference between Bluetooth Low Energy and Bluetooth Basic Rate/Enhanced Data Rate. The emergence of Bluetooth 5 has further confused the landscape. This application note explains the differences and suggests ways to determine the best version for your design.

Click here to download the whitepaper