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
Aug 9, 2022
The ARMMS RF and Microwave Society is an independent professional society comprised of individuals with interest in the design and measurement of devices and products operating at RF and Microwave frequencies.'¯ The Society serves as a focal point for discussions on a wide r...
Aug 3, 2022
With the completion of the Azure Sky wind farm in Texas, we explore the impact of renewable energy, waste reduction, and more on our sustainability efforts. The post A Change in the Wind: Synopsys’ Sustainability Efforts Grow with a Wind Farm in Texas appeared first on...
Jul 27, 2022
It's easy to envisage a not-so-distant future when sophisticated brain-computer interfaces become available for general-purpose infotainment use....

featured video

Reduce SWaP with Multi-physics Aware 3D Heterogeneous Package Design

Sponsored by Synopsys

In this edition of the Synopsys Aerospace and Defense Newsletter, Synopsys invites their partner, Ansys, to discuss joint solutions that help customers create systems with lower size, weight, and power (SWaP) through 3D heterogeneous integration (3DHI).

Watch the video interview or read it in the online newsletter

featured chalk talk

Mission Critical Electrical Controls

Sponsored by Mouser Electronics and Littelfuse

If you are working on a mission-critical design, there is a very important list of requirements that you will need to consider for your electromechanical controls including how well they have been tested, availability of inventory, and the quality of the components. In this episode of Chalk Talk, Amelia Dalton chats with John Saathoff from Littelfuse electromechanical solutions offered by Hartland Controls, the benefits Hartland brings to the table when it comes to mission-critical designs, and how you can get started using Hartland Controls for your next design.

Click here for more information about Hartland Controls from Littelfuse