Formal verification using cached search path information to verify previously proved/disproved properties

An apparatus, comprising:

• a processor;
• and a non-transitory computer-readable storage medium storing instructions that, when executed by the processor, cause the processor to perform a method for formally verifying multiple sequentially-generated versions of a circuit design including performing a separate formal verification session for each said circuit design version using an associated property set including multiple properties, wherein each said formal verification session involves one of (a) proving that each said property is true with respect to an associated said circuit design version, and (b) disproving each said property with respect to said associated circuit design version, the method comprising:
• during a first said formal verification session involving a first circuit design version and a first associated property set including a first property, applying first search operations to said first circuit design version according to a formal verification search strategy to prove/disprove said first property, and storing first search path information that is generated in accordance with said applied first search operations, wherein said first search path information includes a sequential set of said first search operations applied to said first circuit design version during said first search operations that achieved one of a first proof object that proves said first property, and a first counterexample that disproves said first property;
• and
• during a second said formal verification session, which is performed after the first formal verification session and involves a second circuit design version and a second associated property set including said first property, performing a search-path verification process including utilizing at least a portion of said stored first search path information to determine whether said first property is proven/disproven in said second circuit design version.

A computer implemented method for formally verifying multiple sequentially-generated versions of a circuit design including performing a separate formal verification session for each said circuit design version using an associated property set including multiple properties, wherein each said formal verification session involves one of (a) proving that each said property is true with respect to an associated said circuit design version, and (b) disproving each said property with respect to said associated circuit design version, the method comprising:

• during a first said formal verification session involving a first circuit design version and a first associated property set including a first property, applying first search operations to said first circuit design version according to a formal verification search strategy to prove/disprove said first property, and storing first search path information that is generated in accordance with said applied first search operations, wherein said first search path information includes a first reset state and a sequential set of said first search operations applied to said first circuit design version during said first search operations that achieved one of a first proof object that proves said first property, and a first counterexample that disproves said first property;
• and
• during a second said formal verification session, which is performed after the first formal verification session and involves a second circuit design version and a second associated property set including said first property, performing a search-path verification process including utilizing at least a portion of said stored first search path information to determine whether said first property is proven/disproven in said second circuit design version.