In the early days of formal verification technology, some advocates thought it would replace block-level simulation. While this works for certain types of blocks, nowadays we see formal analysis technology as a complement to simulation that has some strengths – such as an ability to quickly find interesting states – and weaknesses, most notably limited capacity. Simulation overcomes capacity limits, but can miss tough corner-case bugs and leave deep coverage points unexercised. What if we could combine simulation and formal analysis, and leverage the strengths of both?
Cadence this week announced Incisive Enterprise Verifier (IEV), an integrated verification solution that includes all the capabilities of the Incisive Enterprise Simulator (IES) and Incisive Formal Verifier (IFV). An IEV user can run simulation or formal analysis, just as they were run before. What IEV adds is a “dual power” capability that provides a tight integration between simulation and formal analysis, adding several new capabilities to the verification arsenal. These capabilities allow designers and verification engineers to find additional bugs, and to exercise interesting coverage points in the design that could not be achieved with standalone formal analysis or simulation.
One new capability, said Sarah Lynne Cooper Lundell, senior product marketing manager at Cadence, is property-driven simulation. Typically, assertions in simulation are passive, and simply act as monitors. With IEV, assertions can actually drive stimulus into the design. This is especially helpful in the design bring-up stage, where you can use assertions to simulate and find bugs. The same assertions can be used for simulation, formal analysis, and acceleration or emulation, enabling verification reuse.
Another new capability is formal-assisted simulation. Here, you identify an interesting state you want to reach, and formal analysis gets you to that state very quickly. Simulation takes over from there. It would be harder to reach that state with simulation alone due to the probabilistic nature of simulation-based stimulus.
A third new capability is simulation-assisted formal analysis. In this case, you stop the simulation after reaching a certain point in time, and turn on the formal engine to take a deeper look and explore around that state. You can run a full formal analysis, but it isn’t a full formal proof because you’re not going back to reset and proving a property over all possible conditions. Simulation-assisted formal analysis allows you to find deep bugs and coverage points without facing the capacity limits of traditional formal tools.
Tom Anderson, product marketing director at Cadence, provided an example of how simulation and formal analysis can work together. “Imagine a scenario in which a processor has to hit a certain sequence of instructions at the same time as a cache miss and an interrupt. It takes thousands of cycles to set up and is probably not reachable from reset in pure formal analysis. But by simulating and jumping around to interesting places in the design while leveraging the power of formal analysis at appropriate points, you have a much better chance of being able to hit that scenario.”
Another advantage of combining simulation with formal analysis is an ability to find coverage points that could be missed by simulation or formal analysis alone. Today, Tom noted, there’s an assumption that all coverage is gathered from simulation. But because IEV can work with SystemVerilog Assertion (SVA) or Property Specification Language (PSL) coverage properties, and because Cadence has a unified coverage database, a coverage point hit in formal analysis is treated no differently from a coverage point hit with simulation. In either case you can choose to bring it into the same database, check it off, and call it done.
All of IEV’s dual power capabilities can be used early in the verification flow, before a testbench is created. “With the combination of formal analysis and simulation engines, you are able to find bugs earlier in the process,” Sarah noted. “You don’t have to wait for a testbench to be available to do deeper verification. When you get to the testbench environment, you can better focus your efforts because you are working with cleaner blocks. IEV is also helpful in the final stage of verification, providing metrics that increase your overall confidence level that you are done. ”
The net result, Sarah said, will be improved productivity. “This will lead to a shift in which formal analysis will become a bigger part of mainstream verification, and not just something done on the side by experts. IEV’s dual power integration of formal analysis and simulation engines will enable widespread usage, and I expect over time IEV will become a standard solution on design and verification engineers’ desktops,” she said.
Whatever the claims, no one verification technology can solve all problems. Our best option is to leverage the advantages of all available technologies and apply them as most appropriate. Incisive Enterprise Verifier is an important step in this direction.