GoldMine software technology is an automated assertion generation tools to aid with the hardware design verification process. It uses data mining and static analysis to generate propositional and temporal assertions in Verilog RTL.

The suite also includes:

• A Figure of Merit Evaluation feature - for evaluating and ranking assertions. 
• Code Coverage Evaluations - for estimating the code covered by an assertion.
• Word Level Assertion Generation tool to make assertions more usable than those generated at bit level. 

For more information, visit the goldmine website: http://goldmine.csl.illinois.edu/ [2]