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
Jul 17, 2025
Why do the links in Outlook emails always open in the Microsoft Edge web browser, even if you have another browser set as your default?...

featured paper

Maximize Power Efficiency in Embedded Applications with Agilex™ 5 E-Series FPGAs and SoCs Memory Solutions

Sponsored by Altera

Learn how Altera Agilex™ 5 FPGAs and SoCs deliver up to 1.9× lower system power than Zynq UltraScale+ without sacrificing performance. This white paper dives into real benchmark data, memory interface efficiency, and architectural advantages that make Agilex 5 the smart choice for embedded, vision, and AI edge applications. Optimize for power, performance, and design simplicity.

Click to read more

featured chalk talk

Automotive MOSFETs
Sponsored by Mouser Electronics and Infineon
In this episode of Chalk Talk, Joseph Sara and Amelia Dalton explore the mega trends motivating MOSFET innovation and the details of Infineon’s cutting-edge MOSFET solutions. They also explore the benefits of Infineon’s OptiMOS 7 platform and how you can take advantage of Infineon MOSFETs for your next design.
Jul 21, 2025
1,702 views