OBDD variable ordering using sampling based schemes
First Claim
Patent Images
1. A method of determining a variable order for building a Boolean Decision Diagram (BDD) for a Boolean function forming a Boolean space, the Boolean function representing a circuit design, comprising:
- forming samples of the Boolean space representing the Boolean function;
building test BDDs for the samples using a plurality of test variable orders; and
determining the variable order using information regarding the size of the test BDDs.
1 Assignment
0 Petitions
Accused Products
Abstract
A system and method for determining variable orders for decision diagrams. The variable orders are determined by sampling subspaces of a Boolean space representing a function or circuit. The subspaces are formed in a variety of ways, including through the use of abstraction, decomposition, partial assignments, and circuit subspaces.
-
Citations
36 Claims
-
1. A method of determining a variable order for building a Boolean Decision Diagram (BDD) for a Boolean function forming a Boolean space, the Boolean function representing a circuit design, comprising:
-
forming samples of the Boolean space representing the Boolean function;
building test BDDs for the samples using a plurality of test variable orders; and
determining the variable order using information regarding the size of the test BDDs. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15)
-
-
16. A method of building BDDs representing a Boolean function, the Boolean function defining a Boolean space of a circuit design, comprising:
-
preprocessing the circuit design by examining a plurality of subspaces of the Boolean space of the circuit design;
determining a variable order based on the examination of the plurality of subspaces; and
building a BDD representing the Boolean function using the variable order as an initial variable order. - View Dependent Claims (17, 18, 19, 20)
-
-
21. A method using a computer for determining variable orders for a circuit design, the variable order being used to build binary decision diagrams (BDDs) of the circuit design, the circuit design having a set of primary inputs and outputs, comprising:
-
partitioning the circuit design;
building BDDs for portions of the partitioned circuit design using a set of variable orders; and
determining the effectiveness of the variable orders. - View Dependent Claims (22, 23, 24)
simulating the circuit for subsets of primary input variables; and
selecting subset of primary input variables.
-
-
24. The method of claim 21 wherein building binary decision diagrams comprises:
-
selecting a set of variable orders; and
applying a set of abstraction functions using the set of variable orders.
-
-
25. A computer-implemented method of developing binary decision diagrams for a circuit, the circuit having a set of primary inputs and outputs and a set of logic components interconnected by nodes, comprising:
-
partitioning the circuit design;
building binary decision diagrams for subsets of the partitioned circuit design; and
evaluating the variable orders.
-
-
26. A computer-implemented method of creating reduced ordered binary decision diagrams for a circuit design comprising:
-
sampling at least one subspace of the circuit design; and
selecting a variable order based on the sampling of at least one subspace of the circuit design. - View Dependent Claims (27)
building a first BDD for a subspace of the circuit design;
building a second BDD for a subspace of the circuit design; and
comparing parameters related to the first and second BDDs.
-
-
28. A method for determining an optimal variable order for building a BDD for a circuit design, the circuit design having a set of primary inputs and a set of primary outputs, comprising:
-
sampling the circuit design to produce samples;
testing variable orders using the samples produced by sampling the circuit design; and
refining the variable orders.
-
-
29. A method for determining an initial variable order for building a decision diagram for a function representing a circuit design, the circuit design having primary inputs, at least one primary output, and internal nodes, comprising:
-
determining an abstraction function;
building decision diagrams for a plurality of internal nodes;
applying the abstraction function to the decision diagrams for the plurality of internal nodes to obtain abstract decision diagrams for the plurality of internal nodes; and
building an abstract decision diagram for the at least one primary output using dynamic variable reordering, the abstract decision diagram for the at least one primary output being based in part on the abstract decision diagrams for the plurality of internal nodes. - View Dependent Claims (30, 31, 32, 33)
determining a second abstraction function;
building decision diagrams for a plurality of internal nodes;
applying the second abstraction function to the decision diagrams for the plurality of internal nodes to obtain second abstract decision diagrams for the plurality of internal nodes;
building a second abstract decision diagram for the at least one primary output using dynamic variable reordering, the second abstract decision diagram for the at least one primary output being based in part on the second abstract decision diagrams for the plurality of internal nodes; and
wherein the abstract decision diagram for the at least one primary output has a final variable order and the second abstract decision diagram for the at least one primary output has a second final variable order; and
selecting between the final variable order and the second final variable order based on a comparison of parameters related to the abstract decision diagram for the at least one primary output and the second abstract decision diagram for the at least one primary output, the selection resulting in a selected variable order.
-
-
33. The method of claim 32 wherein the parameters are the size of the abstract decision diagram for the at least one primary output and the size of the second abstract decision diagram for the at least one primary output.
-
34. A method for determining an initial variable order for building a decision diagram for a function representing a circuit design, the circuit design having primary inputs, at least one primary output, and internal nodes, comprising:
-
building a decomposed decision diagram for the at least one primary output, the decomposed decision diagram having decomposition points;
assigning a first set of values to the decomposition points; and
building a plurality of decision diagrams for the at least one primary output using the values assigned to the decomposition points, each of the plurality of decision diagrams using a different one of a plurality of initial variable orders. - View Dependent Claims (35, 36)
-
Specification