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
April 29th, 2009 at 1:05 pm
Hi Jon,
A complex topic indeed, and I think several things are being mixed up here. When an RTL and gate level description are shown to have the same functionality, then this is equivalence checking and something that formal methods have managed to solve well. as you say, this is not functional verification. Equivalence checking is a garbage-in, garbage-out kind of tool. It shows you that if the RTL is wrong, then the gates will be equally wrong.
Now the RTL description has to be functionally verified. That is what the existing testbenches are used for, and formal methods can be used to prove properties about that RTL. The solutions we have today are fair at best as they cannot – as you correctly state – tells us that everything works under all conditions. (There is one formal companies that claims it can).
When we move up to the system level, the testbench languages and methodologies that exist today are woefully inadequate. They rely on timing rather than sequencing, they have the wrong notions of concurrency. In addition, we require much longer tests than would normally be considered for RTL verification. For example, we need to boot a cell phone, have it connect to the base-station and initiate a call.
Now if we think about formal and system-level descriptions, there is no reason why they cannot do it. Sure the tools on the market today are not the right ones. They deal with clock cycles. But a system is still basically a state machine with a datapath and properties can be applied to them. Given the abstraction that have happened between the RTL and the system level, formal may well be able to handle fairly large systems.
So no – system level and formal is not an oxymoron. It is just that the market for it today is too small for it to exist.
April 30th, 2009 at 8:08 am
I think the mistake is thinking of ESL as “big RTL”.
ESL is a completely different discipline that allows software developers to test their code on a working model. It also allows system wide performance measurement.
But, I think asking it to provide an adequate description of the implementation is to ask it for too much.
If one tries to capture enough information in ESL to verify RTL, then one might as well write RTL.
May 1st, 2009 at 4:38 am
What are we really trying to do with our abstract model? We have something we would like a system to do, we invent an approach we believe will address the need. This “theory” of a possible solution maps onto our abstract model of the solution, functional verification of this abstract model would be our “experiment” to verify our theory.
We can formally prove attributes of our theory which will help us more fully understand the theory. We need to appreciate that proving the attributes proves that what we intended to do is what we did, this does not prove that our theory was correct.
One significant value of abstract modeling is a better understanding of our intentions. I have heard people justify not doing abstract modeling because it cannot be formally verified. I believe we need to focus on the increased understanding we achieve through abstract modeling appreciating the value it brings today without expecting it to guarantee that our theory is correct.
May 2nd, 2009 at 1:54 pm
Not an oxymoron, but all you can verify is that your algorithms are correct, and unless your design is specified in a way tools understand it’s going to be difficult to do. The bulk of verification is about verifying that the algorithms are implemented correctly by down-stream tools and designers. If synthesis and compiler tools guaranteed correct results formal at ESL would make more sense, but given the statistical nature of building on Silicon I think the best you can ever do is a probability that something will work.
However, it is worth noting Einstein’s theories were covered by Godel’s theory that from within a system there are certain things that cannot be proved, and that doesn’t apply to systems we design, so it should be possible to prove that an ESL design is (in some way) “correct”.
I haven’t seen much happening in formal verification of software, so I suspect it’s a long way to getting good formal tools for ESL – at least with current software techniques.
May 4th, 2009 at 12:58 pm
I think the problem of formally checking the model is the same problem ESL has been facing all along and that is each model may have a different level of abstraction making an easy comparison an extremely difficult proposition.
What are we comparing the model against? The RTL? The entire system? The parts of the system in our control? RTL is probably a very limited view of the complete system, being focused typically on a single ASIC. If we’re comparing against the system some of the pieces may not be developed internally and hence the understanding and control over these pieces may be limited. So direct comparison is likewise limited. And if we are just comparing the parts under our control we may still have limited understanding of how these may be ultimately implemented because the drivers and firmware may not be written for months after the ASIC specification is complete and RTL development is nearing completion.
Another complexity arises when a model is created for analysis of the system where the model may not implement all of the error handling and housekeeping features of a design making a direct automated comparison along the lines of LEC impossible.
I think the best we can hope for is to have the requirements for the system and its components specified in a property spec language and use those to drive the development of the model and the system assuring that both meet the specs. However, unless the properties and model are written in enough detail there is still no guarantee that the model will meet the requirements in the same manner as the system implementation.
In the end we verify the model the same way we verify the RTL. We write tests and check the output and when there is a difference or unexpected result we evaluate the differences and determine if the test or the model is correct.
May 13th, 2009 at 6:32 am
It seems Jon discusses two topics; formmally verifying that my ESL model is correct, then formally verifying my ESL model matches my RTL.
I’m not even sure how its theoretically possible to formally verify a model against itself. Perhaps we can call that “linting”. I can check that certain rules are not violated in my ESL model.
ESL to RTL formal verification is difficult. First, its not 100% needed. Since the only way to functionally verify (I like the term “validate” for this as well) the ESL model is to simulate it, I have an extremely good testbench for the RTL (not withstanding the problems of moving from non-timed to timed domain.) But, we do hit the problem of simulation run-time.
So, in my reasoning, formal verification of ESL to RTL is addressing a runtime issue.
Formal verification of RTL to gates, is primarily concerned with complete coverage, which our RTL testbench cannot guarantee. In other words, even if we ran our complete testsuite at the gate level, we still expect formal equivelence checking to do a better job.
So, the first order ROI of RTL to gate formal/equivelance checking is less bugs in your chip. The first order ROI of ESL to RTL formal is reduced simulation time.
Given that ESL to RTL formal will not and cannot replace RTL simulation (at least in our lifetimes…), I do not see great demand for it.
December 9th, 2009 at 4:29 am
Hi thanks to everyone..
This is what I was searching for… “ESL and Functional Verification in one page”