1. A method of generating assertions for verification of an integrated circuit hardware design expressed at a register transfer level (RTL) for variables of interest, the method executable by a computer having a processor and memory, the method comprising: running, by the processor, dynamic simulation traces through the RTL design to generate simulation data; extracting, by a static analyzer, domain-specific information about the RTL design comprising a control flow graph for variables of interest; executing, using the processor, a data mining algorithm with the simulation data and the domain-specific information as inputs, to generate a set of candidate assertions for each variable of interest through machine learning with respect to the domain-specific information, the candidate assertions being likely invariants; conducting, using the processor, formal verification on the RTL design with respect to each candidate assertion by outputting as invariants the candidate assertions that pass a formal check; iteratively feeding back into the data mining algorithm a counterexample trace generated by each failed candidate assertion that violates the formal check, each counterexample trace including at least one additional variable in the RTL design not previously input into the data mining algorithm; and outputting, using the processor, the invariants generated from at least two iterations of executing the data mining algorithm, at least one of which is executed with one or more counterexample traces, which improves coverage of a state space of the RTL design with the at least one additional invariant.