Alok Jain, distinguished engineer at Cadence, directs the company's R&D efforts in formal verification. When he recently visited Cadence San Jose headquarters, we talked about the status of formal verification technology today and trends developing for 2011. Specifically, we talked about formal analysis (also known as model checking or property checking) as provided in tools such as Incisive Enterprise Verifier.
The following interview includes such topics as formal verification usage trends, benefits, roadblocks, formal coverage metrics, and the growing alignment of simulation and formal verification to speed Silicon Realization. For a more detailed look at formal coverage, see the new blog post by Vinaya Singh, R&D architect at Cadence.
Q: Alok, who uses formal verification tools today?
A: Both designers and verification engineers are using the tools. On the whole, I would say that more verification engineers than designers are using formal tools at this point. The main reason is that designers typically do not have the time or inclination to learn new technologies. However, recently I'm seeing a trend towards more designer use of formal tools.
Another dimension is what I would call levels of expertise. I classify users in three different domains. The first category is the pushbutton, naïve user. This user does not understand the design or the technology, and wants to push a button and get results. There's a large group of users there, and this space may include applications like connectivity checks.
A second category is the average user who has an understanding of the design, and some limited understanding of formal technology and tools, so they know a few commands and options. This includes a verification engineer or designer in a group that's using formal tools to verify some formal-friendly designs such as protocol bridges and arbiters. The third category is the expert user in a large company who does formal day in and day out. This user understands the design completely and can do all sorts of manual, expert-level techniques to crunch the design. This is typically done to fully verify some critical IP blocks in the company. The common thread is that all three types of users are trying to speed convergence with formal verification.
Q: What broad trends do you see going into 2011, in terms of adoption and use of formal technologies?
A: I see 3 broad trends going into 2011.
The first is a renewed focus on designer-level usage, where people will use Incisive Enterprise Verifier or other tools to do some quick design bring-up and sanity testing on their designs.
The second trend I see is a focus on expert usage. We do see core teams trying to do more formal analysis, and using expert-level techniques to overcome capacity and performance problems.
I also see a trend towards alignment of formal analysis with mainstream system-on-chip verification. This involves applications like SoC level connectivity, which has traditionally been done in simulation, and now people want to solve it with formal tools. Another example is the coverage unreachability flow, where people take coverage holes from simulation and use formal to try to prove whether they are reachable or unreachable.
Q: What are the main benefits that users are seeing from formal verification?
A: The first benefit is reduced verification time. A prime example here is pad ring connectivity. I know of a customer who was using simulation to check pad ring connectivity, and it took him three months. Using formal, he was able to do it in two weeks.
The other big benefit is finding bugs early in the design process, so by the time the testbench comes up, you have weeded out a lot of bugs. A third benefit is getting proofs for critical blocks that are not easy to verify with simulation, or for IP that is used in a lot of places, and you really want to make sure there are no bugs in the design.
Q: What are the main roadblocks to a greater adoption of formal verification?
A: I think the first one is mindset. There's a mindset that formal is black magic, or is only for the expert, and cannot be used by the average person. Users who are very simulation-oriented don't want to think outside the box and don't think about formal. Another obstacle is skill set. To learn formal you need to learn a few things, such as assertion languages like SVA [SystemVerilog assertions] or PSL [Property Specification Language]. A third roadblock is tools and methodologies. In spite of all the advances formal still has capacity problems, and can only be used for limited design sizes and limited design styles.
Q: Incisive Enterprise Verifier combines simulation and formal verification. Why do this? How does one complement the other?
A: First let's consider how they are different. Simulation is very graceful, and the reason I say "graceful" is that it can handle any kind of design style and almost any kind of capacity. However, it's not exhaustive - you can only verify a limited part of the design. Formal is exhaustive, but it has limited capacity and works with limited design styles. The intent of IEV [Incisive Enterprise Verifier] is to leverage the strengths of both.
One example is the assertion-driven simulation capability in IEV. This is a capability to quickly bring up a design without requiring the user to write elaborate testbenches.
Another example is the searchpointing and guidepointing capabilities in IEV that can be used to find deep corner case bugs. You can use simulation to get to some specific design state, and from there on use formal. For example, you might expect to find a bug after a FIFO is filled. You can use simulation to fill the FIFO and thereafter use formal analysis to find the bug.
Q: Can a block be verified entirely with formal technology?
A: Typically customers use both simulation and formal. But there are some instances where you can avoid simulation completely. One example is pad ring connectivity; if you prove it, you don't need to do any simulation at all. There are also some kinds of blocks that are very well suited for formal. These include protocol-oriented blocks and arbiters. You can verify such blocks completely with formal analysis, avoiding the need for any simulation.
Q: Is there such a thing as formal coverage? If so, what formal metrics could be applied?
A: We can talk about two kinds of formal coverage - formal input coverage, and formal output coverage. Formal input coverage is based on constraints. You write constraints to define the environment of the design. With formal input coverage you're trying to understand how many of the behaviors are allowed by constraints, or how good your constraints are. If lines in your code become unreachable and you get low formal input coverage, it probably means you over-constrained your design.
With formal output coverage, you're looking at what part of the design the assertions covered after they were proven. One very crude metric is assertion density. Perhaps you have one assertion for 100 lines of code - that doesn't guarantee correctness of the assertions. There is also the notion of "assertion completeness" based on mutation coverage, where people try to figure out how much of the design has been verified, but use of this is very limited.
These are not simulation metrics - they are very specifically formal metrics. Simulation metrics are things like pass/fail test coverage, code coverage and functional coverage.
Q: So, how does one compare simulation metrics to formal metrics?
A: That is the biggest problem we have today. At a high level, the way I put it is that formal and simulation speak two different languages as they describe different aspects of the verification intent. Typically, neither tries to leverage the other. We want to be able to say that, if you've done some formal on a block, you can get credit for that and avoid some redundant simulation. But that doesn't happen today because formal and simulation speak different languages. We are trying to change that with a formal metric-driven capability.
Q: It will be very interesting to hear about that! Meanwhile, what do you most want readers to understand about formal verification?
A: It has value. It is here to stay. If you're not using it today, you should seriously consider it.