Method and System for Performing Heuristic Constraint Simplification

• US 20080066033A1
• Filed: 11/15/2007
• Published: 03/13/2008
• Est. Priority Date: 09/22/2005
• Status: Active Grant

• Current Assignee: GlobalFoundries, Inc.
• Original Assignee: Hary Mony, Jason Baumgartner, Robert Kanzelman, Viresh Paruthi
• Inventors: KANZELMAN, ROBERT, BAUMGARTNER, JASON, MONY, HARY, PARUTHI, VIRESH
• Granted Patent: US 7,793,242 B2
• Time in Patent Office: Days
• US Class Current: 716/5
• 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 system, said system comprising:

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

means for applying structural reparameterization 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 first computer-design 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.

2. The computer verification 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.

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

4. The computer verification system of claim 3, further comprising means for adding said candidate gate as a second computer-design constraint.

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

6. The computer verification system of claim 5, further comprising:

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

means for performing verification of said design.

7. The computer verification system of claim 1, further comprising:

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

means for performing verification of said design.