Over-constraints for formal verification

A method comprising:

• receiving, by a formal verification electronic design automation (EDA) application executing on a computing platform, an initial evaluation of a given circuit design of an integrated circuit (IC) chip, the given circuit design of the IC chip comprising a list of properties for the IC chip, wherein the list of properties includes a list of assertions for the IC chip;
• extracting, by the formal verification EDA application, a counter-example trace from the initial evaluation, wherein the counter-example trace characterizes a set of signals of the given circuit design of the IC chip over a plurality of cycles that reaches a state in which a given assertion of the list of assertions does not hold true;
• identifying a subset of signals in the counter-example trace that remain in a specific constant value over the plurality of cycles;
• generating a set of over-constraints based on the subset of signals that remain in a specific constant value;
• receiving a modified circuit design based on the counter example trace, wherein the modified circuit corresponds to the given circuit design modified based on the counter-example from the initial evaluation;
• and
• setting over-constraints for an over-constrained formal verification of the modified circuit design that includes each over-constraint of the set of over-constraints.

A system comprising:

• a non-transitory memory to store machine readable instructions;
• and
• a processor to access the memory and execute the machine readable instructions, the machine readable instructions comprising:
• a formal verification electronic design automation (EDA) application, the formal verification EDA application being configured to:
• receive an initial formal verification of a given circuit design of an integrated circuit (IC) chip, the given circuit design comprising a list of properties for the IC chip, wherein the list of properties includes a list of assertions for the IC chip, wherein the initial formal verification includes a counter-example trace that characterizes a set of signals of the given circuit design of the IC chip over a respective plurality of cycles that reach a state in which a given assertion of the list of assertions does not hold true;
• identify a subset of signals in the counter-example that remain in a specific constant value over the plurality of cycles;
• generate a set of over-constraints for an over-constrained formal verification of the given circuit design of the IC chip based on the identified subset of signals;
• receive a modified circuit design based on the counter example trace, wherein the modified circuit corresponds to the given circuit design modified based on the counter-example from the initial evaluation;
• and
• execute the over-constrained formal verification for the modified circuit design of the IC chip that applies each over-constraint of the set of over-constraints, wherein the over-constrained formal verification has a smaller state space than the initial formal verification.