Industry Leaders Panel: Did We Create the Verification Gap? - Part 8

Industry Leaders Panel: Did We Create the Verification Gap? - Part 8

 

Download the MP3

Transcript

Part 8
Male #10: Hi, this is (Saad Sahir) from NVIDIA, formal verification team.  So from a formal verification team perspective, we really like the assertions.  However, we see that a lot of people are using UVM test benches and checkers.  Now, one big challenge that we see is that the (sounds like:  DV) team and the formal verification team write their own checkers.  So what are your thoughts on combining a set of checkers which are not assertions but that can be reused in the simulation UVM environment as well as in the formal verification environment?
 
Male #3: I don't think assertions have anything to do with it in the sense that particularly if I'm doing like an end-to-end proof, a very complicated proof on a block, most of that code is going to be modeling code.  And maybe one tiny little assertion says, "My modeling code doesn't get into a bad state," you know.  I certainly could use that in a simulation environment, too, if I chose to.  Nothing prevents me.  But, again, that requires discipline, that requires right up front planning.  What am I going to do in formal (inaudible) simulation?  How am I going to leverage between this?  It – where you run into problems is when it's totally ad hoc and people go off and – without any planning right up front and don't do that.  So…
 
Male #2: What I would ask then is, other than just for feeling good, what would be the point of having the same assertions in simulation and emulation – not emulation, but formal verification?  Of course, in formal, assuming constraints are probably set, there are more coverage.  So if you've proven them in formal, why would you keep carrying them in simulation, again, for additional safety?  Hopefully you'd want to go after different things.  Same thing with emulation.  I get customers who ask, "Well, we want the exact same (sounds like:  VIP) running on emulation and simulation."  I said, "Well, why?  They have different purpose."  In emulation, you cannot violate timing, you cannot violate the protocol, you can't change anything, you can't change the schedule of your HTMI video frame; whereas, in simulation, you can.  You verify different things with different engines or different methodology.  So it's a good thing, but…
 
Male #3: Yes.  So, is there a reason you want to do that?
 
Male #10: Well, the reason I ask was because usually at NVIDIA, we have different – in simulation, they write their own UVM-based checkers.  Right?  And later on in the design when we have formal verification resources available, they come and jump on it.  And if they have existing checkers, we can actually try and include them in the formal verification environment, as opposed to understanding the spec and writing our own checkers.
 
Male #2: But you having to re-understand the spec I think is a good thing, too, because you come at it from a different perspective, especially when you come in with an assertion mindset.  It's different when somebody comes in from a high level verification where you abstract states and delays and pipeline stages.
 
Mike Stellfox: But yet still, like we've seen good success.  I mean, the nice thing about an assertion is it does electronically capture the intent.  And so we have seen good success, at least for protocol, you know, if you're looking at it like an interface, especially standard interfaces and so on, being able to capture that if you're doing formal verification first or, you know, simulation, capturing those assertions for the bus protocol or the interface protocol and doing that once.  Right?  And there is a benefit in that, you know, if you're verifying at one level and you're – especially if you're doing formal verification on the interface, you want to be able to prove the assumptions that you had around that in a simulation-based environment based on how you constrained it.  And we've seen customers do that very successfully, you know.  It does require the discipline to build and plan for your assertions in such a way that they can be leveraged cross those domains.