Mining hardware assertions with guidance from static analysis

Samuel Hertz, David Sheridan, Shobha Vasudevan

Research output: Contribution to journalArticlepeer-review


We present GoldMine, a methodology for generating assertions automatically in hardware. Our method involves a combination of data mining and static analysis of the register transfer level (RTL) design. The RTL design is first simulated to generate data about the design's dynamic behavior. The generated data is then mined for 'candidate assertions' that are likely to be invariants. The data mining algorithm is a decision-tree-based supervised learning algorithm. These candidate assertions are then passed through a formal verification engine to filter out the spurious candidates. The assertions that are attested as true by the formal engine are system invariants. These are then evaluated by a process of designer ranking that is provided as feedback to the data mining engine. We demonstrate the scalability of GoldMine by showing assertion generation of the RTL of Sun's OpenSparc T2 many-threaded processor. Our results show that GoldMine can generate complex, high coverage assertions for sequential as well as combinational designs in RTL, thereby minimizing human effort in this process. GoldMine assertions distill the random input stimulus space and can be used for calibrating directed tests. They can be used in a regression test suite of an evolving RTL. They are also useful in providing differing perspectives from the designer, as well as hints to designers for manually writing assertions.

Original languageEnglish (US)
Article number6516599
Pages (from-to)952-965
Number of pages14
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number6
StatePublished - 2013
Externally publishedYes


  • Assertion generation
  • data mining
  • logic verification
  • static analysis
  • validation

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering


Dive into the research topics of 'Mining hardware assertions with guidance from static analysis'. Together they form a unique fingerprint.

Cite this