1. A method for generating assertions of a hardware design to aid verification in an electronic design automation (EDA) system, the method comprising: accessing trace data of a hardware design, wherein the trace data is a sequence of recorded netlist node values of the hardware design, obtained while the hardware design executed one or more tests; accessing a predetermined set of predicates of the hardware design by a computer, wherein each predicate represents a Boolean relation among netlist nodes in the hardware design; projecting the trace data over the set of predicates by a computer to generate a second trace; computing a set of states based on the second trace by the computer, wherein each state is a complete assignment of the set of predicates at one moment in time; producing a set of logical consequences from the set of states by the computer; and enumerating each logical consequence as an assertion by the computer.