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
Jun 12, 2025
We truly do live in a world that would have been considered to be a far-flung science fiction future only a few short decades ago...

featured paper

Shift Left with Calibre Pattern Matching: Trust in design practices but verify early and frequently

Sponsored by Siemens Digital Industries Software

As integrated circuit (IC) designs become increasingly complex, early-stage verification is crucial to ensure productivity and quality in design processes. The "shift left" verification approach, enabled by Siemens’ Calibre nmPlatform, helps IC design teams to identify and resolve critical issues much earlier in the design cycle.

Click to read more

featured chalk talk

Machine Learning on the Edge
Sponsored by Mouser Electronics and Infineon
Edge machine learning is a great way to allow embedded devices to run applications that can collect sensor data and locally process that data. In this episode of Chalk Talk, Amelia Dalton and Clark Jarvis from Infineon explore how the IMAGIMOB Studio, ModusToolboxā„¢ Software, and PSoC and AURIXā„¢ microcontrollers can help you develop a custom machine learning on the edge application from scratch. They also investigate how the IMAGIMOB Studio can help you easily develop and deploy AI/ML models and the benefits that the PSoCā„¢ 6 Artificial Intelligence Evaluation Kit will bring to your next machine learning on the edge application design process.
Aug 12, 2024
56,373 views