We present GoldMine, a methodology for generating assertions automatically in hardware. Our method involves a combination of data mining and static analysis of the register transfer level (RTL) design. The RTL design is first simulated to generate data about the design's dynamic behavior. The generated data is then mined for “candidate assertions” that are likely to be invariants. The data mining algorithm is a decision-tree-based supervised learning algorithm. These candidate assertions are then passed through a formal verification engine to filter out the spurious candidates. The assertions that are attested as true by the formal engine are system invariants. These are then evaluated by a process of designer ranking that is provided as feedback to the data mining engine. We demonstrate the scalability of GoldMine by showing assertion generation of the RTL of Sun's OpenSparc T2 many-threaded processor. Our results show that GoldMine can generate complex, high coverage assertions for sequential as well as combinational designs in RTL, thereby minimizing human effort in this process. GoldMine assertions distill the random input stimulus space and can be used for calibrating directed tests. They can be used in a regression test suite of an evolving RTL. They are also useful in providing differing perspectives from the designer, as well as hints to designers for manually writing assertions.

We propose a methodology to generate input stimulus to achieve coverage closure using GoldMine, an automatic assertion generation engine that uses data mining and formal verification. GoldMine mines the simulation traces of a behavioral register transfer level (RTL) design using a decision tree based learning algorithm to produce candidate assertions. These candidate assertions are passed to a formal verification engine. If a candidate assertion is false, a counterexample trace is generated. In this paper, we feed these counterexample traces to iteratively refine the original simulation trace data. We introduce an incremental decision tree to mine the new traces in each iteration. The algorithm converges when all the candidate assertions are true. We formally prove that our algorithm will always converge and capture the complete functionality of each output of a sequential design on convergence. We show that our method always results in a monotonic increase in simulation coverage. We also present an output-centric notion of coverage, and argue that we can attain coverage closure with respect to this notion of coverage. We elaborate the technique step by step using a nontrivial arbiter design. Experimental results to validate our arguments are presented on several designs from Rigel, OpenRisc, and SpaceWire. Some practical limitations to achieve 100% coverage and the differences between final decision tree and binary decision diagram are discussed.

We present a methodology to generate input stimulus for design validation using GoldMine, an automatic assertion generation engine that uses data mining and formal verification. GoldMine mines the simulation traces of a behavioral Register Transfer Level (RTL) design using a decision tree based learning algorithm to produce candidate assertions. These candidate assertions are passed to a formal verification engine. If a candidate assertion is false, a counterexample trace is generated. In this work, we feed these counterexample traces to iteratively refine the original simulation trace data. We introduce an incremental decision tree to mine the new traces in each iteration. The algorithm converges when all the candidate assertions are true. We prove that our algorithm will always converge and capture the complete functionality of an output on convergence. We show that our method always results in a monotonic increase in simulation coverage. We also present an output-centric notion of coverage, and argue that we can attain coverage closure with respect to this notion of coverage. Experimental results to validate our arguments are presented on several designs from Rigel, OpenRisc and SpaceWire.

Pattern mining is a fundamental problem that has a wide range of applications. In this paper, we study the problem of finding a minimum set of signature patterns that explain all data. In the problem, we are given objects where each object has an item set and a label. A pattern is called a signature pattern if all objects with the pattern have the same label. This problem has many interesting applications such as assertion mining in hardware design and identifying failure causes from various log data. We show that the previous pattern mining methods are not suitable for mining signature patterns and identify the problems. Then we propose a novel pattern enumeration method which we call Pattern Shrink. Our method is strongly coupled with another novel method that is very similar to finding a local optimum with a negligible loss in performance. Our proposed methods show a speedup of more than ten times over the previous methods. Our methods are flexible enough to be extended to mining high confidence patterns, instead of signature patterns.

System level modeling is widely employed at early stages of system development for simplifying design verification and architectural exploration. Assertion based verification has become a well established part of RTL verification methodology. In the traditional assertion based verification flow, assertions are manually written. In this paper, we generate assertions from system level designs using GoldMine, an automatic assertion generation engine that uses data mining and static analysis. Candidate assertions are mined in the form of frequent patterns in the simulation traces of the system level designs. We consider both cycle accurate and transaction level designs and develop a methodology for the mining of each. For cycle accurate designs, we use both a decision tree based supervised learning algorithms as well as a coverage guided association mining algorithm to search for correlations in the simulation trace. For transaction level designs, sequential pattern mining is applied to generate frequent sequences of function calls and events from traces. We also use a symbolic execution engine to generalize the parameters and return values of the functions to help the data miner find relevant behavior. We show that our technique generates meaningful assertions on both a cycle accurate RISC CPU design and a transaction level AMBA-based DMA controller.

We present GOLDMINE, a methodology for generating assertions automatically. Our method involves a combination of data mining and static analysis of the Register Transfer Level (RTL) design. We present results of using GoldMine for assertion generation of the RTL of a 1000-core processor design that is still in an evolving stage. Our results show that GoldMine can generate complex, high coverage assertions in RTL, thereby minimizing human effort in this process.