A basic part of verification is the creation of completion criteria. Some cases will be exercised before the completion of verification, but not all interesting cases. Completion criteria are created based on the assumption (though we are sometimes not aware of it) that the behavior correctness of the exercised cases implies the behavior correctness of all other interesting cases.
This assumption is true if at least one of the exercised cases is similar enough to each of the remaining interesting cases. Making this assumption uncarefully can cause huge loss (e.g. the famous pentium bug) but it wastes money and time to have too many exercised cases similar enough to each of the remaining interesting cases.
Ideally, we should exercise a case only if it can catch any bug that other excercised cases cannot catch. It is clearly impossible to exercise all interesting cases, but proving the value of a case is better only if it is easier than actually exercising this case in verification. We provide the first practical solution to determine the value of the cases to be exercised. Overall, it can be much faster than exercising the cases on the real chip! As the result, the verification coverage can get much higher in much shorter time, and the verification cost (including debugging) can often get much lower than $1 per trillion cases (or the same number of functional coverage points).
Our solution proves a "similarity class" of cases, which is defined as that the behavior correctness of any case in the similarity class is mathematically equivalent to the behavior correctness of all cases in the similarity class. A similarity class is typically very big because many input bits over many clock cycles can have different values among the cases and many register initial values can, too. Our solution proves a big bundle of such big similarity classes quickly.
Our solution generates Verilog code of two short cases if a similarity class is proven not true. These 2 cases are as similar as possible, but one can show a bug on any normal simulator while the other cannot. The code handles both checking and driving, and it also shows the defined similarity classes. The code defining similarity classses can be either manually created or be generated mostly from a normal simulation run. Therefore, it works with all popular verification flows smoothly. It has been used with impressive successes in big projects at multiple (big and small) companies.
Copyright © 2011 Superior Logic Corporation