OBDD variable ordering using sampling based schemes

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.

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.

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.

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.

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.

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.