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 to
- generate design insights
- identify coverage holes in the test suite
- debug a failing assertion or test.
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.
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).
- Samuel Hertz, David Sheridan and Shobha Vasudevan. Mining Hardware Assertions with Guidance From Static Analysis. IEEE Trans. on CAD of Integrated Circuits and Systems 31 (IEEE TCAD) 32 (6): 952-965(2013) (Please use this for citing GoldMine)
- Shobha Vasudevan, David Sheridan, Sanjay Patel, Bill Tuohy. GoldMine: Automatic generation of assertions using data mining and static analysis, Design Automation and Test in Europe (DATE) 2010:626-629
- Lingyi Liu, David Sheridan, William Tuohy and Shobha Vasudevan, A Technique for Test Coverage Closure Using GoldMine. IEEE Trans. on CAD of Integrated Circuits and Systems (IEEE TCAD)31(5): 790-803 (2012)
- Lingyi Liu, David Sheridan, William Tuohy, Shobha Vasudevan Towards coverage closure: Using GoldMine assertions for generating design validation stimulus, Design Automation and Test in Europe (DATE) 2011: 173-178
- Lingyi Liu, David Sheridan, Viraj Athavale, Shobha Vasudevan: Automatic generation of assertions from system level design using data mining, , International Conference on Formal Methods and Models for Codesign (MEMOCODE ) 2011: 191-200
- Lingyi Liu, and Shobha Vasudevan, Automatic Generation of System Level Assertions from Transaction Level Models. Accepted. Journal of Electronic Testing: Theory and Applications (JETTA) 29(5): 669-684 (2013)
- Lingyi Liu, Chen Hsuan Lin and Shobha Vasudevan, Word Level Feature Discovery to Enhance Quality of Assertion Mining, International Conference on Computer Aided Design ( ICCAD) 2012: 210-217
- Chen-Hsuan Lin, Lingyi Liu and Shobha Vasudevan, Generating concise assertions with complete coverage, ACM Great Lakes Symposium on VLSI (GLSVLSI) 2013, pp 185-190
- Shobha Vasudevan, GoldMine: Automatic assertion generation using data mining and static analysis, Design and Verification Conference, (DVCON) 2011
- Parth Sagdeo, Viraj Athavale Sumant Kowshik and Shobha Vasudevan PRECIS: Inferring Invariants using Program Path Guided Clustering, International Conference on Automated Software Engineering (ASE) 2011: 532-535
- David Sheridan, Lingyi Liu, Hyungsul Kim and Shobha Vasudevan , A Coverage Guided Mining Approach for Automatic Generation of Succinct Assertions. In Proceedings of International Conference on VLSI Design (VLSI Design) 2014 . Best paper award.
- Samuel Hertz, Debjit Pal, Shobha Vasudevan. A Figure of Merit for Assertions in Verification. Asia South Pacific Design Automation Conference (ASPDAC) 2019. To appear.
- Shobha Vasudevan, Samuel Hertz and Lingyi Liu, A Comparative Study of Assertion Mining Algorithms in GoldMine. Book chapter. To appear in Machine Learning Methods in VLSI Computer-Aided Design, Springer. Editors Abe Elfadel, Dunae Boning and Xin Li
- Patent Title: Integration of Data Mining and Static Analysis for hardware Design Verification. Patent number: 9,021,409. Issue date: April 28, 2015.
- Patent Title: Merit Based Characterization of Assertions. Patent number: 9,075,935. Issue date: July 7, 2015.