None of my assertions are passing. They’re all inconclusive. What should I do?
Answered by Anshul Jain | May 6, 2020
First of all, please don’t throw them away. Trust me, they are useful.
It’s painful to see engineers throwing away their hard work just because the formal tools are conservative about how they report results and tag bounded proofs as inconclusive. We just need to go one step further and analyse these results to find the good news in them.
Hint — every inconclusive result usually comes with a number attached to it.
Read on for the complete answer…
All formal verification tools have historically been conservative in terms of expressing the results they produce after running a property. Unless the tool has found an invariant for the property, they cannot not mark it as “pass/proven”. However, most engines in formal verification tools can, and do, provide a bound up to which the exhaustive search has been done. Here is where the human layer of intelligence needs to be applied. Let’s see what human intelligence we are talking about.
Just like one does not necessarily need all the money in the world to take a (financial) retirement, similarly, an engineer does not require the formal tool to prove each and every property before signing-off a design using formal verification. So, how can one retire/sign-off?
There is a common answer to the question. And the answer is — know your bound. Find out how much money/depth do you need before you retire/sign-off. Sit-down, clear the fog, and start working towards identifying the required proof depth (RPD) of the checkers which will cover the design well enough to root out all the bugs it has.
RPD calculation is a seemingly daunting and boring task that’s fairly easy to put off especially when you are young in formal land. Afterall, the general expectation is that a formal tool should sort everything out, but what if it doesn’t? You end up putting yourself and the design in a less than ideal situation.
Now, how to come out of analytical paralysis and identify your RPD? Following 6 step guide from the DVCon 2014 2nd best paper “Sign-off with bounded formal verification proofs” will set you in the right direction of calculating required proof depth for formal sign-off. Let’s dig in…
Start by finding out the bare minimum. Code covers on the output control signals and determine the number of cycles the design takes to propagate the inputs received to the outputs. Once you have a starting point, keep layering the effect of cases like design initialisation, multiple streams of data, errors etc. By now, we should have an initial number (say N) which we can start calling as RPD. We will fine tune the RPD in the coming steps.
Identify the building blocks of the design. Such as state machines, FIFOs, counters, linked lists etc. Again, implement covers to estimate how many cycles it takes to reach interesting states of these building blocks. A good exercise would be to code covers for all the state transitions of a state machine inside your design. These covers will fetch you enough information to estimate how many cycles are required to cover the logic for the entire state machine. Once you have the depth details for all the interesting states of various building blocks used in your design, do your math (mostly add) as per their arrangement of these building blocks in the design. This step will most likely increase (say by 𝚫a) your RPD from the previous step.
Cover interesting corners
Now comes the most important of listing the functional coverage targets for interesting corners of the design. You will need a lot of brainstorming here. Work with designers and your fellows in the verification team to identify those interesting corners of the design which will take longest cycles to hit. Once the list of functional coverage targets is ready, code them as covers, run the covers and arrive at the depth which will be required to hit that last mile in the design. Again, this step will most likely increase your RPD from the previous step (say by 𝚫b)
That’s it, calculations done! RPD = N + 𝚫a + 𝚫b
We now have a goal in the form of RPD to achieve and formally sign-off the design. So, if the achieved proof depth of your assertions has already exceeded RPD, you are good to sign-off.
But, wait, just like our math exams, it is always a good habit to validate your calculations to be sure. Refer to section V, subsection D, E, F of the DVCon paper for ways to validate your RPD calculation. The paper includes two detailed case studies to help understand the process of calculating required proof depth in detail.
Question from the case study, validation steps? — #AskOski