Method and apparatus for improving efficiency of constraint solving

• US 20070005533A1
• Filed: 05/02/2005
• Published: 01/04/2007
• Est. Priority Date: 05/02/2005
• Status: Active Grant

• Current Assignee: Synopsys Incorporated
• Original Assignee: Synopsys Incorporated
• Inventors: Saxena, Vikram, Iyer, Mahesh
• Granted Patent: US 7,353,216 B2
• Time in Patent Office: Days
• US Class Current: 706/19
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

Techniques are presented for identifying blockable subsets. Blockable subsets can increase the efficiency by which solutions to a constraint set representation (CSR) can be found. Nodes of a blockable subset can be marked as “blocked” and learning or implication procedures, used as part of a CSR solving process, can be designed to skip nodes marked as blocked. The identification of a particular blockable subset is typically associated with certain conditions being true. If and when the conditions no longer hold, the nodes of the blockable subset need to be unblocked. One type of blockable subset can be identified during the operation of an implication engine (IE) by a technique called justified node blocking (JNB). Another type of blockable subset can be identified by a technique called pivot node learning (PNL). PNL can be applied in-between application of an IE and application of case-based learning.

Claims

1. A method for determining a solution to a set of constraints, comprising:

identifying a pivot cone;

applying a learning procedure to the pivot cone; and

marking the nodes of the pivot cone as blocked.

2. The method of claim 1, further comprising:

skipping a node, for application of an implication, if the node is marked as blocked.

3. The method of claim 1, further comprising:

skipping a node, for application of a learning procedure, if the node is marked as blocked.

4. The method of claim 1, further comprising:

unmarking a node, marked as blocked as a result of a current state, when a constraint set representation is reverted to an earlier state.

5. The method of claim 1, further comprising:

unmarking a node marked as blocked when a state variable changes.

6. The method of claim 1, further comprising:

determining whether a property applies to each basis node of the pivot cone, after a state variable changes, and, if the property applies to all basis nodes, keeping the pivot cone marked as blocked.

7. The method of claim 6, wherein the step of determining whether a property applies further comprises:

determining that the property applies to a basis node if a range of the basis node, after the state variable changes, encompasses a set of values equal to, or smaller than, a set of values of a range of the basis node prior to the state variable change.

8. The method of claim 1, wherein the step of identifying a pivot cone further comprises:

identifying a pivot node.

9. The method of claim 8, wherein the step of identifying a pivot node further comprises:

identifying whether a range of a candidate pivot node is a singleton value.

10. The method of claim 8, wherein the step of identifying a pivot node further comprises:

identifying whether a candidate pivot node is a primary input.

11. The method of claim 8, wherein the step of identifying a pivot node further comprises:

identifying whether an operator of a candidate pivot node is complete.

12. The method of claim 8, wherein the step of identifying a pivot node further comprises:

identifying whether at least one input node, of a candidate pivot node, has a non-singleton value range.

13. The method of claim 8, further comprising:

identifying a subset, of a transitive fanin of the pivot node, for inclusion in the pivot cone.

14. The method of claim 13, wherein the step of identifying a subset further comprises:

identifying whether a candidate node, for inclusion in the subset, has all paths, to any primary output, passing through the pivot node.

15. The method of claim 13, wherein the step of identifying a subset further comprises:

identifying whether a candidate node, for inclusion in the subset, has a complete operator.

16. The method of claim 8, further comprising:

identifying a set of basis nodes, of the pivot cone, that contains only one node with a non-singleton range.

17. The method of claim 16, wherein the step of identifying a set of basis nodes further comprises:

permitting a candidate node, for inclusion in the set of basis nodes, to be included in the set of basis nodes if it represents an incomplete operator.

18. The method of claim 16, wherein the step of identifying a set of basis nodes further comprises:

permitting a candidate node, for inclusion in the set of basis nodes, to be included in the set of basis nodes if it represents a primary input.

19. The method of claim 1, further comprising:

marking as blocked, prior to applying the learning procedure, nodes not of the pivot cone.

20. The method of claim 1, wherein the learning procedure is recursive learning.

21. The method of claim 20, wherein the depth of recursion is not limited.

22. A data-processing system for determining a solution to a set of constraints, comprising the following sub-systems:

a sub-system configured to identify a pivot cone;

a sub-system configured to apply a learning procedure to the pivot cone; and

a sub-system configured to mark the nodes of the pivot cone as blocked.

23. A computer program on a computer readable medium, having computer-readable code devices embodied therein, for determining a solution to a set of constraints, the computer program comprising:

computer readable program code devices configured to identify a pivot cone;

computer readable program code devices configured to apply a learning procedure to the pivot cone; and

computer readable program code devices configured to mark the nodes of the pivot cone as blocked.