Performance in terms of time taken is obviously important in all aspects of verification, especially formal verification.
One of the largest factors in performance is how the problem is specified to the tool by the user code, namely the properties themselves. This webinar shows how to describe the problem using a combination of SVA properties and auxiliary code (HDL helper code) in order to increase performance.
Initially this can seem very counter-intuitive and the best way to learn is by example.
Performance in terms of time taken is obviously important in all aspects of verification.
When using formal this presents a big problem if we are looking for conclusive PASS/FAIL results because one does not know how long it will take to reach that conclusive answer, i.e. you learn nothing until the result appears.
There are several aspects of performance over which the user has no control, for example, how good the tool algorithms are.
There are circumstances where the user is limited by pragmatic or financial limits, for example, how many processors are available, how much memory is available, how many licences do I have, and so on.
Clearly tools have methodologies and user controllable settings which can improve performance.
However, one of the largest factors in performance is how the problem is specified to the tool by the user code, namely the properties themselves. It is not good enough to describe functionally correct properties. They have to be efficient for formal as well otherwise one never obtains a result within an acceptable time.
This webinar focuses primarily on how to describe the problem using a combination of SVA properties and auxiliary code (HDL helper code).
Describing the problem in this way can yield very large increase in performance, however many people do not even consider using auxiliary code because they are unaware of it. Furthermore, some classes of common problem cannot be described solely by SVA at all, which is often a surprise to many people. Therefore, for some problems there is no alternative to using auxiliary code.
It can initially seem very counter-intuitive and alien how to describe the problem using a combination of auxiliary code and properties and it does take some time to develop this skill. The only way to learn is by example and that is the intent of this webinar.
The word performance describes observed results vs. some predefined expectation. Many people often don’t understand or think about their expectations of formal. For example, some peoples understanding of what formal is solely used for is to achieve exhaustive proofs on 100% of their properties. This is almost always unrealistic. In this webinar we will discuss other use models for formal and hence how to have an understanding of what we can realistically achieve.