Method and system for performing heuristic constraint simplification

• US 7,315,996 B2
• Filed: 09/22/2005
• Issued: 01/01/2008
• Est. Priority Date: 09/22/2005
• Status: Expired due to Fees

• Current Assignee: GlobalFoundries, Inc.
• Original Assignee: International Business Machines Corporation
• Inventors: Paruthi, Viresh, Mony, Hari, Baumgartner, Jason R., Kanzelman, Robert L.
• Primary Examiner(s): Lin; Sun James
• Application Number:
  US11/232,764
• Publication Number:
  US 20070067746A1
• Time in Patent Office: 831 Days
• Field of Search: 716/5, 716/3, 716/4, 716/18
• 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 reparameterization 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 steps of:

selecting a first computer-design constraint for simplification;

applying structural reparameterization 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 a 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 a step of creating a candidate gate as said initial value of said first computer-design constraint.

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

5. The method of claim 4, further comprising a 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 a design for use with said first computer-design constraint; and

performing verification of said design.