Is ESL Formal Verification An Oxymoron?

I’ve had a number of conversations recently trying to understand what verification means for ESL and higher level models. It seems that most of the people I talk to are looking for a guarantee, they want formal verification, a proof that the design is doing what it should do. To qualify that a bit, most of the people I interact with are closely involved and influenced by the hardware implementation flows. They are used to having tools for formal verification to provide guarantees that the gate level implementation does exactly what the RTL did and that the rest of the downstream processes have not broken their design. On the surface it’s a nice thing to want but does it really make sense?

The point of a high-level model is to capture the intent of the design, the design does exactly what it is defined to do, and the model is the definition of what the design does. This circular logic appears to make a formal proof somewhat problematic. To refine the kind of formal verification I’m thinking of, and what I hear many people asking for, it is a self-contained proof that the design is correct. Comparing the RTL and gate level, this proof is achieved without simulation vectors and no interpretation of the intent is required.  At some point this will be possible between the system level model and the RTL, but this isn’t really possible for the system level itself.

So what is possible?  Functional verification: exercising the design in the way it will be used and verifying that the system does what I expect it to do.  I can track coverage statistics, I can verify that the use modes are covered and that the various modes of the system are exercised, but for today’s complex systems it is virtually impossible to deliver exhaustive function coverage. Going back to Einstein’s quote above, functional verification can give me better confidence that my design will deliver what I want, but there is always the possibility that a new situation will produce an unexpected response.  Ultimately the more abstract models are allowing us to perform more complete functional verification, covering more of the actual use cases, running the software and processing the data that the system would actually be responsible for.  The value of system level modeling is in helping us understand the implications of our intent, helping us to explore the possibilities of manipulating and responding to some stimulus in an interesting and useful way.  By doing this we can ensure that we understand what we want to build and we can formally verify that we build what we want.  We cannot formally prove that the intended behavior is always the right behavior.  With more functional verification we gain confidence in understanding what we want, but alas self contained formal verification of the intent of a design is not something we can or should expect to achieve.

–Jon McDonald, technical marketing engineer, Mentor Graphics