A coverage guided mining approach for automatic generation of succinct assertions

Machine learning techniques are widely employed for automatic assertion generation in hardware verification. Our previous method Goldmine uses a decision tree based approach for mining assertions and does not have design coverage related feedback. The assertions are unaware of the design, over-constrained and have low expressiveness. We introduce a coverage guided mining approach for mining assertions from simulation traces. Our approach combines association rule learning, greedy set covering and formal verification. It circumvents the exhaustive rule generation of association mining using coverage feedback. The algorithm has been implemented as one part of GoldMine The tool can be downloaded from the website: http://goldmine.csl.illinois.edu. Experiments using a variety of designs, including USB, PCI and OpenRisc, show that the assertions generated by coverage guided association mining cover an average of 6.14 times input space than those generated by decision tree based mining algorithms. We also show that the coverage guided association mining produces an average of 2.75 times fewer propositions per assertion than decision tree based mining. All these mean the assertions generated by coverage guided association mining are more succinct, and of higher value for hardware design verification.