Method and system for performing heuristic constraint simplification

• US 20070067746A1
• Filed: 09/22/2005
• Published: 03/22/2007
• Est. Priority Date: 09/22/2005
• Status: Active Grant

• Current Assignee: GlobalFoundries, Inc.
• Original Assignee: International Business Machines Corporation
• Inventors: Paruthi, Viresh, Kanzelman, Robert, Mony, Hari, Baumgartner, Jason
• Granted Patent: US 7,315,996 B2
• Time in Patent Office: Days
• US Class Current: 716/107
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A method for performing verification is disclosed. The method includes selecting a first computer-design constraint for simplification and applying structural reparamaterization to simplify the first computer-design constraint. In response to determining that the first computer-design constraint is not eliminated, the first computer-design constraint is set equal to a dead-end state of the constraint. A structural preimage of the first computer-design constraint is created, in response to determining that a combination of a target and the dead-end state of the first computer-design constraint is equal to a combination of the target and the structural preimage of the first computer-design constraint, the first computer-design constraint is set equal to the structural preimage.

Claims

1. A computer-verification method comprising the steps of:

selecting a first computer-design constraint for simplification;

applying structural reparamaterization to simplify said first computer-design constraint;

in response to determining that said first computer-design constraint is not eliminated, setting said first computer-design constraint equal to a dead-end state of said first computer-design constraint;

creating a structural preimage of said first computer-design constraint; and

in response to determining that a combination of a target and said dead-end state of said first computer-design constraint is equal to a combination of said target and said structural preimage of said first computer-design constraint, setting said first computer-design constraint equal to said structural preimage.

2. The method of claim 1, further comprising the step of, in response to determining that said combination of said target and said dead-end state of said first computer-design constraint implies a combination of said target and said structural preimage with trace prefixing, identifying an initial value of said first computer-design constraint.

3. The method of claim 2, further comprising the step of creating a candidate gate as said initial value of said first computer-design constraint.

4. The method of claim 3, further comprising the step of adding said candidate gate as a second constraint.

5. The method of claim 4, further comprising the step of setting said first computer-design constraint to said structural preimage of said first computer-design constraint.

6. The method of claim 5, further comprising,

receiving a design for use with said first computer-design constraint;

and

performing verification of said design.

7. The method of claim 1, further comprising:

receiving said design for use with said first computer-design constraint; and

performing verification of said design.

9. The system of claim 1, further comprising means for, in response to determining that said combination of said target and said dead-end state of said first computer-design constraint implies a combination of said target and said structural preimage with trace prefixing, identifying an initial value of said first computer-design constraint.

10. The system of claim 9, further comprising means for creating a candidate gate as said initial value of said first computer-design constraint.

11. The system of claim 10, further comprising means for adding said candidate gate as a second constraint.

12. The system of claim 11, further comprising means for setting said first computer-design constraint to said structural preimage of said first computer-design constraint.

13. The system of claim 12, further comprising,

means for receiving a design for use with said first computer-design constraint;

and

means for performing verification of said design.

8. A computer verification system, said system comprising:

means for selecting a first computer-design constraint for simplification;

means for applying structural reparamaterization to simplify said first computer-design constraint;

means for, in response to determining that said first computer-design constraint is not eliminated, setting said first computer-design constraint equal to a dead-end state of said constraint;

means for creating a structural preimage of said first computer-design constraint; and

means for, in response to determining that a combination of a target and said dead-end state of said first computer-design constraint is equal to a combination of said target and said structural preimage of said first computer-design constraint, setting said first computer-design constraint equal to said structural preimage.

14. The system of claim 8, further comprising:

means for receiving said design for use with said first computer-design constraint; and

means for performing verification of said design.

15. A machine-usable medium having a plurality of instructions processable by a machine embodied therein, wherein said plurality of instructions, when processed by said machine, causes said machine to perform a computer-verification method comprising:

selecting a first computer-design constraint for simplification;

applying structural reparamaterization to simplify said first computer-design constraint;

in response to determining that said first computer-design constraint is not eliminated, setting said first computer-design constraint equal to a dead-end state of said constraint;

creating a structural preimage of said first computer-design constraint; and

in response to determining that a combination of a target and said dead-end state of said first computer-design constraint is equal to a combination of said target and said structural preimage of said first computer-design constraint, setting said first computer-design constraint equal to said structural preimage.

16. The machine-usable medium of claim 15, wherein said method further comprises the step of, in response to determining that said combination of said target and said dead-end state of said first computer-design constraint implies a combination of said target and said structural preimage with trace prefixing, identifying an initial value of said first computer-design constraint.

17. The machine-usable medium of claim 16, wherein said method further comprises the step of creating a candidate gate as said initial value of said first computer-design constraint.

18. The machine-usable medium of claim 17, wherein said method further comprises the step of adding said candidate gate as a second constraint.

19. The machine-usable medium of claim 18, wherein said method further comprises the step of setting said first computer-design constraint to said structural preimage of said first computer-design constraint.

20. The machine-usable medium of claim 19, wherein said method further comprises,

receiving a design for use with said first computer-design constraint;

and

performing verification of said design.