Improving simulation results with formal-based technology

When it comes to formal methods, many engineers are skeptics. Perhaps this is due to value propositions that have been pitched over the years that have over-promised yet under-delivered in terms of results. Or perhaps it is due to the advanced skills that have traditionally been required to achieve predictable and reliable results. After all, historically this was the case—dating back to the mid-nineties when formal techniques were only adopted by companies that could afford a dedicated team of formal experts with PhDs.

So, what’s changed today? The emergence of functional verification solutions targeted at specific problem domains, which blend simulation with formal-based techniques in a seamless way to improve results. In other words, the application of formal-based technology is not just for experts anymore! In fact, everyone can reap the benefits of formal analysis today with very little effort.

One example of this blending of simulation with formal-based techniques is in the area of accelerating the process of code coverage closure with the new Questa CoverCheck solution. Closing code coverage typically involves many engineering weeks of effort to manually review code coverage holes to determine if they are unreachable and can be safely ignored—or figuring out exactly how to handcraft special tests to cover them during simulation. Questa CoverCheck makes it easy for non-expert users to leverage formal-based technology to complete this process by automatically identifying the set of unreachable coverage items in a design, and then guiding the user to create tests for the reachable items that have not been covered yet. This process, illustrated in the figure below, is push-button, low-effort, and requires no expertise with formal techniques. In addition, no assertions are required nor expertise in assertion languages. It is a beautiful example of how formal-based technology is blended with simulation to form a solution that improves both productivity and quality of results.

Another example of how formal-based technology is being used today to complement simulation is with AutoCheck, which is part of the Questa Formal solution. For example, there is a class of bugs that cannot be found using RTL simulation due to a simulation effect known as X-state optimism. These bugs might be found during gate-level simulation, but this occurs very late in the design flow when it is costlier to fix. By using AutoCheck, engineers are able to identify and correct X-state issues early in the design flow, before simulation occurs. In addition to X-state issues, AutoCheck uses formal-based technology to verify a wide range of common RTL errors that are difficult or impossible to find during RTL simulation. It is another example of a push-button, low-effort solution where assertion-language and formal expertise is not required. What’s new in the latest Questa Formal release is significant improvements in engine performance and capacity, along with multicore support.

Questa CDC is one more example of how formal-based technology is being used today to complement simulation. Today, we see about 94% of all designs have multiple asynchronous clock domains. Verifying that a signal originating from one clock domain will safely be registered in a different asynchronous clock domain is not possible using traditional RTL simulation since state element setup and hold times are not modeled, which means that metastability issues will not be verified. Again, these bugs might be found later in the flow during gate-level simulation where it is costlier to fix. Static timing analysis, although effective at finding timing issues within a single or synchronous clock domains is unable to identify issues across asyncrhonous clock domains. This is an area with formal-based technology, such as Questa CDC, can help. What’s new in the latest Questa CDC release is support for unlimited design sizes through hierarchical CDC analysis along with a 5X improvement in performance.

To learn what’s new with Questa Formal-Based Technology, see our recent press release. Or check out the Questa Cover Check, Questa CDC and Questa Formal links.