GoldMine: Automatic assertion generation using data mining and static analysis

What

GoldMine is a tool suite of algorithms for automatic assertion generation. Verification is the process of checking that the implemented design (hardware) meets the required specification. With the growing number of transistors in an integrated circuit, the task of verification is far more challenging than the development of the system itself (the distribution of time and resources is roughly 70-30 between verification and development). Problems in verification are in the complexity class NP and worse, presenting a major intellectual challenge to the community. Among the chief challenges in verification is property specification, or the expression of desired intent from a system. The whole verification process hinges on "knowing what one is looking for". To painstakingly write these properties can take many man-months

Assertions are manually generated summaries of system specification that are useful throughout the system development cycle. Assertions have emerged as a popular candidate verification solution (a recent study mentions an increase from 37% to 69% in assertion usage over 3 years). However, assertion generation is as yet a manually intensive task that is very difficult for designers not trained in verification and temporal logics.

How

GoldMine combines statistical, dynamic methods (data mining) with static, deterministic methods (source code static analysis and formal verification). Data mining algorithms make inferences about the dynamic behavioral data of the system, while formal verification is used to check the truth/falsehood of the inferences. Static source code analysis of RTL is used to provide domain guidance to the data miner. Such inferred assertions can capture complex functional and temporal properties of the hardware, which can surpass assertions generated by human reasoning. At present, GoldMine uses 7 specialized data mining algorithms along with complex RTL static analysis technology. GoldMine has enabling technologies for assertion generation like estimating RTL statement coverage of assertions and word level assertion generation, both of which are research problems with no good existing solutions. GoldMine is able to rank assertions automatically with respect to their value in the system design.

And so what...

Several EDA tools have burgeoned in the area of automatic assertion generation. Many of the product teams have approached Prof. Vasudevan over the past 3 years with proposals for collaboration. Two leading EDA companies (name withheld for IP confidentiality) have licensed GoldMine. GoldMine is being developed as a product by a leading EDA company. GoldMine is also popular among users of the technology. It is being licensed by UIUC to many users. Users of GoldMine include Qualcomm Inc., Broadcomm Corporation, Oracle Corporation, Huawei Technologies, AMD, Texas Instruments and IBM. GoldMine was judged one of the most popular tools at DVCon, which is a verification industry practitioners' conference. ). GoldMine is being used by several universities teaching RTL design, to automatically grade assignments designed by students in Verilog RTL. Our team provides technical support to 17 universities including CMU, Princeton, UC Berkeley that are using GoldMine for research purposes.

Broader impact of solution

GoldMine automates a ubiquitous but currently manual system design process. This has a broad impact on utilization and channeling of human and computing resources within the system's verification cycle. The marriage of statistical and static analysis methods to infer domain specific knowledge is a "meta-technique" that can be used in other domains where we need to analyze the systems that we build. This "GoldMine principle" has already been applied across the board- to software testing, real time software performance analysis, embedded and system level functional checking as well as in ensuring security and privacy of systems.

Resources

  • GoldMine can be downloaded from the GoldMine websitefor research and academic purposes. If you are a commercial entity that wants access to the tool, please contact Prof. Shobha Vasudevan by email.

    • 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)
    • Samuel Hertz, David Sheridan and Shobha Vasudevan. A Combination of Data Mining and Static Analysis to Automatically Infer Assertions IEEE Trans. on CAD of Integrated Circuits and Systems 31 (IEEE TCAD) 32 (6): 952-965(2013)
    • 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, Shobha Vasudevan Towards coverage closure: Using GoldMine assertions for generating design validation stimulus, Design Automation and Test in Europe (DATE) 2011: 173-178
    • Shobha Vasudevan, GoldMine: Automatic assertion generation using data mining and static analysis, Design and Verification Conference, (DVCON) 2011
    • Hyungsul Kim, David Sheridan, Sungjin Im, Shobha Vasudevan, Tarek Abdelzaher and Jiawei Han, Signature Pattern Covering via Local Greedy Algorithm and Pattern Shrink, , 2011 International Conference on Data Mining ( ICDM) 2011: 330-339
    • 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
    • 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
    • Shobha Vasudevan, David Sheridan ,Lingyi Liu and Hyung Sul Kim INTEGRATION OF DATA MINING AND STATIC ANALYSIS FOR HARDWARE DESIGN VERIFICATION. U.S. Patent Application No.20130019216 (pending)