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
Jan 27, 2020
Everybody writing software wants it to perform according to its specification and to be reliable. I hope that this is a safe assumption. There are 3 things to be done to achieve these goals: design well; implement carefully; test thoroughly. None of these are optional. A care...
Jan 27, 2020
I see switches everywhere: toggle switches, slider switches, rotary switches, pushbutton switches, magnetic switches, reed switches, mercury switches, smart switches, and'€¦ the list goes on....
Jan 24, 2020
[From the last episode: We looked at the different ways memory can be organized in different kinds of systems.] Let'€™s look at a scenario: you run a restaurant, but you'€™re short on funds to hire people. So you'€™re your own chief cook and bottle-washer. You do everyt...
Jan 23, 2020
Embedded design trends typically revolve around three main ideas: faster data rates, smaller form factors and cost-effective solutions. Those design trends drive the theme for the 2020 Embedded Tech Trends forum: The Business and Technology Forum for Critical and Intelligent ...

Featured Video

Automotive Trends Driving New SoC Architectures -- Synopsys

Sponsored by Synopsys

Today’s automotive trends are driving new design requirements for automotive SoCs targeting ADAS, gateways, connected cars and infotainment. Find out why it is essential to use pre-designed, pre-verified, reusable automotive-optimized IP to meet such new requirements and accelerate design time.

Drive Your Next Design to Completion Today with DesignWare IP® for Automotive SoCs