Mentor Graphics has added three branches to its Questa formal verification suite that automate and in some cases streamline the formal verification of coverage checks, common problems hard to detect in RTL, and clock domain crossing.
Questa CoverCheck has been designed to identify and exclude coverage items that can never be reached and also provide feedback to inform a testbench so that it can identify those items that are hard to reach. The goal is to reduce the long time engineers need to spend manually reviewing coverage plans.
Questa AutoCheck is designed to automatically identify common errors on a push-button basis. For issues such as X propagation, deadlock, combo-loop and overflow, the tool generates the assertions that perform the necessary coverage checks without any input (or generation authoring) by the user.
Questa CDC uses coverage checks to identify synchronization, protocol and reconvergence errors in designs that need to cope with multiple asynchronous clocks to ensure that necessary harmonization circuitry has been introduced. Today, some 96% of designs face these clock domain crossing issues, largely a reflection of the proliferation in IP blocks.
Harry Foster, Mentor's chief scientist, said that the new features would both increase productivity - a 5X performance boost is claimed on Questa CDC - and extend the use of formal techniques. The technology has come a long way since it was exclusively a PhD domain in the 1990s, but many users still find some aspects challenging.
"I don't think there's a design that tapes out today that doesn't use formal equivalence checking," Foster said. "And the reason for that it has been automated so that the user doesn't need to be an expert.
"That's what we're now doing here, turning these other tasks into push-button exercises. In many cases, the user won't be personally aware that formal techniques are being used."
The three new coverage-checking tools are available immediately. From more details, click, www.mentor.com/products/fv.