Architecture

The image below depcits the GoldMine architecture.

Static Analyzer

The Static Analyzer is composed of a Verilog parser and elaborator. The parser constructs a control-data flow graph (CDFG) from a Verilog design. The parser supports a large behavioral subset of the Verilog-2005 hardware description language. The elaborator extracts top module, variable, clock, reset, and cone of influence information from the CDFG.

Data Generator

The Data Generator is composed of a test bench generator, simulator, and data compressor. The test bench generator generates an unconstrained random test bench for the top module in the Verilog design. The simulator uses the test bench to simulate the top module for a user-specified number of cycles and records the value of each variable in each cycle. The data compressor removes duplicate examples from the data set.

Data Miner

The Data Miner uses data generated by the Static Analyzer and Data Generator to generate a set of candidate assertions. The Data Miner can use one of two data mining algorithms. The Best-Gain Decision Forest algorithm will quickly generate a functionally complete set of assertions. However, some of the assertions might be overconstrained. The Prism algorithm will generate a maximally concise and functionally complete set of assertions. However, Prism has higher time complexity than the Best-Gain Decision Forest algorithm. In addition, Prism can generate a large number of assertions.

Formal Verifier

The Formal Verifier constrains the top module by disabling its reset signal and verifies the generated assertions. The Data Miner can use counterexample data generated by the Formal Verifier to refine the set of assertions.