Features

Requirements

GoldMine runs on most 64-bit linux variants. GoldMine uses Synopsys Verilog Compiler Simulator (VCS) to generate random simulation data. If VCS is not available, then GoldMine can accept VCD files on the command line. GoldMine uses Cadence Incisive Formal Verifier (IFV) to formally verify the assertions it generates. If IFV is not available, then GoldMine will label the assertions it generates as "unverified."

Static Analyzer

The static analyzer extracts information from the Verilog source code.

The Verilog parser supports a large behavioral subset of the Verilog-2005 grammar. The parser constructs a model to support hierarchical static elaboration, automatic clock detection, automatic reset detection, bounded logic cone of influence computation, variable ranking, and assertion coverage computation.

The bounded logic cone of influence computation determines the set of variables that can affect the value of a given target variable. The bounded cone of influence improves the algorithmic and qualitative performance of GoldMine.

The static analyzer uses an algorithm based on the PageRank citation ranking algorithm to rank variables in a given design. GoldMine can use the ranks to select an important set of target variables or rank assertions.

Coming Soon

The static analyzer will be able to compute the Verilog code coverage of an assertion. GoldMine will be able to use the coverage computation to rank assertions.

The static analyzer will be able to determine a relevant set of word-level predicates. GoldMine will be able to use the word-level predicates to generate word-level assertions.

Data Generator

The data generator generates an unconstrained random test bench and executes it using a Verilog simulator. Currently, the data generator uses Synopsys VCS.

Coming Soon

The data generator will be able to generate a constrained random test bench. In addition, the data generator will be able to use Icarus Verilog.

Data Miner

The data miner extracts assertions from the Verilog simulation data. The data miner can use one of two engines: Best-Gain Decision Forest or Prism.

The Best-Gain Decision Forest engine learns hierarchical relationships amongst variables. It executes quickly but can generate overconstrained assertions.

The Prism engine learns concise relationships amongst variables. It executes more slowly than the Best-Gain Decision Forest engine, but it will not generate overconstrained assertions. The Prism engine can generate a large number of assertions.

Coming Soon

The Association Mining engine will be able to learn relationships amonst variables with high input space coverage. It will execute more slowly than the Best-Gain Decision Forest and Prism engines, but it will generate a small set of assertions with high input space coverage.

Formal Verifier

The formal verifier verifies the generated assertions. Currently, the formal verifier uses Cadence IFV.

Assertion Analyzer

The assertion analyzer computes metrics for the generated assertions to measure assertion correctness, readability, and coverage.

The assertion analyzer computes the percentage of true assertions amongst the generated assertions to measure assertion correctness.

The assertion analyzer computes the average number of propositions and temporal length per assertion to measure assertion readability.

The assertion analyzer computes the average simulation coverage per assertion to measure assertion coverage.

Coming Soon

The assertion analyzer will be able to compute additional metrics to measure assertion coverage, subtlety, and unexpectedness. In addition, the assertion analyzer will be able to rank assertions.