The Verification Conundrum

When constrained random test pattern generation became the de facto way to verify designs, reference models became necessary to check that a design was producing the correct output. These were often distributed across several models, such as checkers, scoreboards and assertions.

Another model that had to be created was the coverage model. It was required because you had to know if a generated test was actually useful, and exercise some aspect of the design that had not been tested previously. The generation of the initial model defined the important aspects of a design that you wanted to make sure got exercised. Coverpoints and covergroups were defined, and although these do not actually correspond to functionality being stimulated and checked, they were deemed a good enough proxy. In my personal view, this was a wrong decision made by the industry, and a very expensive one.

You cannot have a discussion with any verification person before crosses are discussed. They will quickly say that if you have defined a set of coverpoints, then you will also be concerned about the crosses of those, and soon you get to an intractable problem. That last part is very true because the total number of states in most realistic designs is such that you can never get it into all states, and thus it can never be fully verified. But – and this is a big ‘but’ – you never have to.

There are many forms of coverage, such as line coverage, toggle coverage, decision and branch coverage. The list goes on, but there is one I believe is very important and often ignored – path coverage. That is usually ignored, because if it is used in its unrolled form, it is also intractable. It doesn’t include every path a design could follow in the code. Instead, it is the complete functionality of the design as implemented. But – and here is the other big ‘but’ – that is a much smaller level of intractable.

The place where these two come together is by defining the notion of a unique piece of hardware. If a piece of hardware has been tested and shown to work, then it will always work, in every case, unless there is some other piece of hardware contained in it that is only exercised under some unique condition. It is this last part of the statement that scares everyone into going down the path of coverpoint crosses. However, if there is no unique piece of hardware to start with, then it is all a big waste of time. Still, it does mean that you need to buy another emulator.

Let us use a very simple example, and forgive it for being so simple. It should convey the important message. The concept scales through abstraction. Assume there is a statement in RTL code that says, if a > 42 then do ‘x’ otherwise do ‘y’. We will also assume that the operator ‘>’ has been formally verified and thus we know it always works and there are no unique pieces of code hidden in there. Now we can look at the conditional. There are a total of two paths in that statement and they result in us doing either ‘x’ or ‘y’. The values needed to fully verify the conditional are two, or perhaps three if you also want to put in some degree of coverage for software engineers always being off by 1. The values are 41, 42, and 43.

Hopefully nobody disagrees yet, but if you do, please tell me why. I am also assuming that the synthesis tool works and it does not inject any bugs.

If we now replace the register ‘a’ with a register bank, say 16 registers, then it would be reasonable to say that we may want to ensure that the line of code still works when the source data comes from each of those registers. In doing so, we have verified the path and multiplexers that direct the correct data to the operator. Next comes the first controversial bit. If we now duplicate that code and place it somewhere else, what needs to be verified? We need to know if the operator is indeed the same operator, and if it is, it should also be using exactly the same hardware to multiplex and move the data. It should not be necessary to do all the original verification again, only verify the paths taken and the code executed in each of those paths, because there is no unique hardware involved. There can be no bugs hidden in there.

The same reasoning is true if we were to add an output register into the code paths and even write the result out to that same register bank. Once we have verified that the first statement always correct writes the result to the correct register, then so long as no unique hardware has been used, it is not necessary to do it for every statement. And it certainly does not mean that for coverage we need the cross of the input registers, the output registers, and every operator and every instance of that operator that exists in the code.

Coverage is completely lacking any notion of unique hardware. While the example I have used is simple, the concept should be extensible. Path coverage can help to show where unique code is, and it should be possible to use that to reduce the crazy number of crosses that need to be executed. While it is not possible to do this in the fullest sense, because path coverage is actually the same thing as formal in some senses, i.e., covers all possible inputs and sequences of inputs, it does not have to explore all paths. It is only used to exclude redundant cases, which can easily be identified and thus reduce the verification burden.

There is something in my mind that says I must be missing something, because I have been advocating for this for almost 30 years, and nobody has agreed with me and done something about it.