US Patent 7926020 Methods for automatically generating assertions

One embodiment of the present invention provides a method that automatically generates assertions of a hardware design. The method includes accessing a trace and a set of predicates of the hardware design. Then, the trace is projected over the set of predicates to generate a second trace. Then, a new set of states of the second trace is computed and the result is represented as a logical formula. The formula is reduced by logic optimization techniques. And finally, a set of logical consequences of the logic formula is produced and each logical consequence is enumerated as an assertion.