An automatic assertion generation tool


Vision

GoldMine started as a tool for assertion generation in hardware (RTL) design back in 2009. It was the first published methodology/tool that applied machine learning for assertion generation. Assertion generation refers to the automation of the manual, tedious, ad-hoc and incomplete process of writing assertions. The principle of GoldMine is simple but powerful. Machine learning algorithms are guided by automatic algorithms that can statically analyze the state space of the system. The domain knowledge of the static analysis algorithms and formal verification could be leveraged as an oracular, iterative mechanism to direct the learning process. This interaction between a statistical inductive inference engine and a static analysis engine could be used repeatedly to generate assertions that surpass manual assertions in quality. GoldMine also has a ranking strategy that can rank assertions on the basis of coverage, importance, expectedness and complexity.

GoldMine has a Verilog RTL parser, a symbolic execution engine, a static analysis engine, a ranking engine and several machine learning algorithms implemented as part of the source code. These can be used outside of assertion generation such as:

  1. generate design insights
  2. identify coverage holes in the test suite
  3. debug a failing assertion or test.

Impact

GoldMine is a large and open source code base. It has been licensed by three leading EDA companies and forms the basis of a commercial product since 2013. Multiple graduate and undergraduate students have worked on it since 2009. It has been licensed and used by multiple semiconductor companies including Qualcomm, IBM, Oracle, Broadcom and Intel. It has won multiple research awards and has also been used by universities to provide a regression test for their Verilog design course projects.GoldMine has a Verilog RTL parser, a symbolic execution engine, a static analysis engine, a ranking engine and several machine learning algorithms implemented as part of the source code. These can be used outside of assertion generation to (i) generate design insights (ii) identify coverage holes in the test suite (iii) debug a failing assertion or test.

Contribution

The principle behind GoldMine has been used beyond design verification. It has been (or is being) used in software testing, autonomous vehicle verification, neural network architecture validation, reliability, and design interpretability.

The software invariant generation tool we developed is called PRECIS. It performed significantly better than its predecessors that did software invariant generation (DAIKON and other tools).

A quick intro of GoldMine from Prof. Vasudevan