Shobha Vasudevan

In hardware verification, assertions play a vital role in proving the correctness of a design. Assertions can be used to debug a design before it is manufactured as well as ensure proper functionality after the actual chip has been produced. Assertions are especially valuable in hardware, where a design cannot be changed after it is released to customers, in contrast to software, where a product can easily be patched to fix bugs.

Even though assertions are very valuable, they can put a considerable drain on the resources of the project. The time spent writing assertions can greatly delay a product's launch, allowing competitors with inferior testing standards to get their products out first. In addition, engineers who could be necessary for other tasks are needed to spend their time creating the assertions. There is also no guarantee that a set of assertions created by a team of humans is even going provide a high amount of coverage of a design.

The solution to this problem is Goldmine, a system for the automatic generation of assertions using data mining and static analysis. Decreasing the reliance on humans for assertion generation will decrease time to market and free up engineers for other roles in the design cycle. Goldmine has the potential to produce a set of assertions for a design that has a higher coverage than the average team of humans could produce.

There are several stages that make up the GoldMine tool chain. The first stage is the Data Generator, where target RTL is simulated and a trace is producing that gives the state of all inputs, outputs, and internal signals at the positive edge of each clock cycle. Typically, the inputs are randomized to produce a trace that displays a wide variety of functionality of the circuit. However, directed tests may also be used.

Static analysis is also used on the RTL to help give more domain information to the data miner. A logic cone analyzer can be used to determine which signals have no relation to the target output. This data can be used to remove signals from the search space that cannot possibly have any relation with the this output, making data mining more efficient.

Given the static analysis and simulation trace data, the A-Miner stage looks for relationships between the target output and any inputs or internal signals. The data mining method used is called a Decision Tree. This method makes recursive splits on the simulation data to try and isolate suspected functionality. Once some relationship between the output and inputs or internal signals is found to happen 100% of the time, a candidate assertion is produced. This produces a set of assertions that are likely to be true.

A Formal Verifier is used in the next stage to determine the validity of each candidate assertion. This technique analyzes the RTL to determine if an assertion is true all of the time or if it can be violated in some way. If the rule is false, a counterexample is produced which gives an example of an input stimulus that violates the specified assertion. This counterexample can then be added to the simulation trace which gives the assertion less than 100% confidence. This allows the decision tree to continue to partition the input space and produce more candidate assertions. Eventually, this can produce a set of all true assertions that can be used to verify the design.

The assertions that GoldMine produces are able to achieve very high input space coverage, which is described as percentage of possible input stimulus covered by the set of assertions. These assertions with high input space coverage can even be generated with very limited simulation data. Results also show that the counterexamples from formal verification can also be used as directed tests to cover any parts of the design that were not covered during the initial simulation of the design. These tests are shown to given higher coverage of a design than random or directed tests alone. GoldMine is still in a very early stage of development, which means that there is still a lot of growth potential. When the project reaches maturity, it will be able to ensure design stability and decrease time to market, making it an invaluable asset to any verification team.

Send us an email if you would like to get access to Goldmine software for research use.