Patent ID: 8589837

Claim:
A computer-implemented method for simplifying a netlist via an inductive trace lifting within a multi-algorithm verification framework, the method comprising: a processor of a computing device deriving first unreachable state information that can be utilized to simplify the netlist; performing a simplification of the netlist utilizing the first unreachable state information; determining whether the first unreachable state information can be inductively proved on an original version of the netlist; and in response to the first unreachable state information not being inductively provable on the original version of the netlist: projecting the first unreachable state information to a minimal subset; and said adding the projected unreachable state information as an invariant to further constrain a child induction process, wherein adding the projected first unreachable state information as an invariant ensures that any resulting induction counterexamples can be mapped to valid induction counterexamples on the original version of the netlist before undergoing the simplification.