System and method for guiding and optimizing formal verification for a circuit design

A method for guiding formal verification for a circuit design in circuit simulation software to optimize the time required for verification of the circuit design, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. manually modifying the analysis region if verification of the circuit design over the analysis region results in a determination that the analysis region is not verified including the steps of:
• 1. selecting a signal in the analysis region;
• and
• 2. adding a portion of the circuit design relating to the signal in the analysis region having the step of adding a portion of an articulated fan-in driving the signal to the analysis region including adding a portion of the articulated fan-in driving the selected signal that is turned-on by current value assignments in a plot window to the analysis region;
• and
• repeating steps b–c until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize the time required for verification of the circuit design the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. manually modifying the analysis region if verification of the circuit design over the analysis region results in a determination that the analysis region is not verified including the steps of:
• 1. selecting a signal in a plot window;
• and
• 2. adding a reset portion of an articulated fan-in of the selected signal in the analysis region;
• and
• repeating steps b–c until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize the time required for verification of the circuit design, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. manually modifying the analysis region if verification of the circuit design over the analysis region results in a determination that the analysis region is not verified including the steps of:
• 1. the user selecting an articulation point inside the analysis region;
• and
• 2. removing an articulated fan-in of the articulation point from the analysis region or adding an articulated fan-in driving the selected articulation point to the analysis region;
• and
• repeating steps b–c until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize the time required for verification of the circuit design, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. manually modifying the analysis region if verification of the circuit design over the analysis region results in a determination that the analysis region is not verified including the steps of:
• 1. a. the user selecting at least one signal in the analysis region from a plot window, wherein each signal is selected at a specific time cycle;
• 2. b. generating a triple based on each selected signal, wherein a triple comprises the name of the selected signal, the specific time cycle of selection and the value of the selected signal at the specific time cycle;
• 3. c. generating a rule based on the triples;
• 4. d. verifying the rule separately;
• and
• 5. e. verifying the circuit design using the rule as an assumption for the analysis region;
• repeating steps b–c until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize time required for verification process, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. identifying candidate signals for modification of the analysis region if verification of the circuit design results in a determination that the circuit design is not verified including the step of identifying articulation points corresponding to the analysis region as the candidate signals;
• d. automatically modifying the analysis region using the candidate signals;
• and
• e. manually modifying the analysis region if there are no appropriate candidate signals;
• and
• repeating steps b–e until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize time required for verification process the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. identifying candidate signals for modification of the analysis region if verification of the circuit design is false results in a determination that the circuit design is not verified;
• d. automatically modifying the analysis region using the candidate signals including the step of prioritizing the candidate signals on the basis of productivity choices;
• and
• e. manually modifying the analysis region if there are no appropriate candidate signals;
• and
• repeating steps b–e until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize time required for verification process, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. identifying candidate signals for modification of the analysis region if verification of the circuit design results in a determination that the circuit design is not verified;
• d. automatically modifying the analysis region using the candidate signals including at least one of the steps of:
• 1. expanding the analysis region by including an articulated fan-in corresponding to the highest-productivity choices that are located at the boundary of the analysis region, and
• 2. removing the articulated fan-in corresponding to the highest-productivity choices that are located inside the analysis region from the analysis region;
• and
• e. manually modifying the analysis region if there are no appropriate candidate signals;
• and
• repeating steps b–e until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize time required for verification process, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. identifying candidate signals for modification of the analysis region if verification of the circuit design results in a determination that the circuit design is not verified;
• d. automatically modifying the analysis region using the candidate signals;
• and
• e. manually modifying the analysis region if there are no appropriate candidate signals including the steps of:
• 1. defining an abstraction created in response to the low productivity choices in the analysis region;
• 2. proving the abstraction in the circuit design separately;
• and
• 3. verifying the circuit design using the abstraction in the analysis region;
• and
• repeating steps b–e until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize time required for verification process, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. identifying candidate signals for modification of the analysis region if verification of the circuit design is false results in a determination that the circuit design is not verified;
• d. automatically modifying the analysis region using the candidate signals;
• and
• e. manually modifying the analysis region if there are no appropriate candidate signals including the steps of:
• 1. defining an assumption created in response to low productivity choices in the analysis region;
• 2. proving the assumption in the circuit design separately;
• and
• 3. verifying the circuit design using the assumption in the analysis region;
• and
• repeating steps b–e until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize time required for verification process, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. identifying candidate signals for modification of the analysis region if verification of the circuit design is false results in a determination that the circuit design is not verified;
• d. automatically modifying the analysis region using the candidate signals;
• and
• e. manually modifying the analysis region if there are no appropriate candidate signals including the steps of:
• 1. the user selecting at least one signal in the analysis region from a Plot window, wherein each signal is selected at a specific time cycle;
• 2. generating a triple based on each selected signals, wherein a triple comprises the name of the selected signal, specific time cycle of selection and the value of the selected signal at the specific time cycle;
• and
• 3. generating a rule based on the triples;
• 4. verifying the rule separately;
• and
• 5. verifying the circuit design using the rule as an assumption for the analysis region;
• and
• repeating steps b–e until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize time required for verification process, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region including having a user deciding that there is an error in the circuit design in case there are no high-productivity choices;
• c. identifying candidate signals for modification of the analysis region if verification of the circuit design is false results in a determination that the circuit design is not verified;
• d. automatically modifying the analysis region using the candidate signals;
• and
• e. manually modifying the analysis region if there are no appropriate candidate signals;
• and
• repeating steps b–e until the circuit design is verified or until a user identifies an error in the circuit design.

A method for guiding formal verification for a circuit design in circuit simulation software to optimize the time required for the verification process, the method comprising the steps of:

• a. identifying an analysis region for verifying the circuit design;
• b. verifying the circuit design by applying formal verification over the analysis region;
• c. identifying articulation points corresponding to the analysis region as analysis region modification choices;
• d. automatically modifying the analysis region using an articulated fan-in of the analysis region modification choices if verification of the circuit design over the analysis region results in a determination that the analysis region is not verified;
• repeating steps b–d until the circuit design is verified;
• and
• repeating steps b–d until a user identifies an error in the circuit design.

A system for guiding formal verification of a circuit design in circuit simulation software to optimize time required for verification process, the system comprising:

• a. a GUI for enabling a user to input information;
• b. an Analysis Region Selection tool for selecting an analysis region for verifying the circuit design;
• c. a Formal Verification tool for verifying the circuit design using the selected analysis region and verified user defined rules;
• and
• d. a Productivity Choice Determination tool to determine high-productivity choices for expanding the analysis region if verification fails.

A system for guiding formal verification of a circuit design in circuit simulation software to optimize time required for verification process, the system comprising:

• a. a GUI for enabling a user to input information;
• b. an Analysis Region Selection tool for selecting an analysis region for verifying the circuit design;
• c. a Formal Verification tool for verifying the circuit design using the selected analysis region and verified user defined rules;
• and
• d. an Articulation Point Selection tool to identify articulation points corresponding to the analysis region to choose smaller analysis region for circuit verification.

A system for guiding formal verification of a circuit design in circuit simulation software to optimize time required for verification process, the system comprising:

• a. a GUI for enabling a user to input information;
• b. an Analysis Region Selection tool for selecting an analysis region for verifying the circuit design;
• c. a Formal Verification tool for verifying the circuit design using the selected analysis region and verified user defined rules;
• and
• d. a Rule Verifier for verifying user defined rules for the analysis region.

A system for guiding formal verification of a circuit design in circuit simulation software to optimize time required for verification process, the system comprising:

• a. a GUI for enabling a user to input information;
• b. an Analysis Region Selection tool for selecting an analysis region for verifying the circuit design;
• c. a Formal Verification tool for verifying the circuit design using the selected analysis region and verified user defined rules;
• and
• d. a database for storing a set of triples based on a set of signals selected by the user.

A system for guiding formal verification of a circuit design in circuit simulation software to optimize time required for verification process, the system comprising:

• a. a GUI for enabling a user to input information;
• b. an Analysis Region Selection tool for selecting an analysis region for verifying the circuit design;
• c. a Formal Verification tool for verifying the circuit design using the selected analysis region and verified user defined rules;
• d. a Productivity Choice Determination tool to determine high-productivity choices for expanding the analysis region if verification fails;
• e. an Articulation Point Selection tool to identify articulation points corresponding to the analysis region to choose smaller analysis region for circuit verification;
• f. a Rule Verifier for verifying user defined rules for the analysis region;
• and
• g. a database for storing a set of triples based on a set of signals selected by the user.