OBDD variable ordering using sampling based schemes

• US 6,389,374 B1
• Filed: 11/05/1998
• Issued: 05/14/2002
• Est. Priority Date: 06/03/1998
• Status: Expired due to Term

• Current Assignee: Fujitsu Limited
• Original Assignee: Fujitsu Limited
• Inventors: Lu, Yuan, Jain, Jawahar
• Primary Examiner(s): FREJD, RUSSELL WARREN
• Application Number:
  US09/187,055
• Time in Patent Office: 1,286 Days
• Field of Search: 703/2, 703/14, 716/5, 716/2, 716/7, 716/3
• US Class Current: 703/2
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

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.

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.

2. The method of claim 1 wherein the step of forming samples the Boolean space comprises obtaining subspaces using partial assignments.

3. The method of claim 1 wherein the step of forming samples the Boolean space comprises creating abstract BDDs.

4. The method of claim 1 wherein the step of forming samples of the Boolean space comprises creating decomposed BDDs.

5. The method of claims 2, 3 or 4 wherein the test BDDs are built using dynamic reordering.

6. The method of claims 2, 3, or 4 further comprising the step of estimating parameters, the parameters influencing the step of forming samples of the Boolean space.

7. The method of claim 6 wherein the step of estimating parameters comprises determining a set of primary input variables for abstraction.

8. The method of claim 7 wherein the determining the set of primary input variables for abstraction is accomplished by simulating a portion of the circuit design for a plurality of subsets of primary input variables.

9. The method of claim 8 wherein the set of primary input variables for abstraction is determined to be the subset of primary input variables which provide a maximum amount of coverage of the circuit design.

10. The method of claim 6 wherein the step of estimating parameters comprises determining a set of decomposition points.

11. The method of claim 10 wherein the decomposition points are determined randomly.

12. The method of claim 10 wherein the decomposition points are determined by nodes at which a BDD grows beyond a threshold value.

13. The method of claim 10 wherein the decomposition points are determined by nodes at which a BDD operation exceeds a predetermined computer resource amount.

14. The method of claim 11, 12, or 13 wherein the decomposition points are assigned a value.

15. The method of claim 14 wherein the decomposition points are assigned a value derived from a simulation of the circuit design.

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.

17. The method of claim 16 wherein the step of preprocessing comprises building BDDs for a plurality of subspaces using a plurality of possible variable orders for each subspace.

18. The method of claim 17 wherein the plurality of possible variable orders are initial variable orders and the building of BDDs is accomplished using dynamic variable reordering.

19. The method of claim 18 wherein the step of preprocessing further comprises selecting a plurality of secondary variable orders, the plurality of secondary variable orders forming a subset of the plurality of possible variable orders, based on a parameter related to the BDDs built in the building of the BDDs.

20. The method of claim 19 wherein the step of preprocessing further comprises building BDDS for a plurality of subspaces using the plurality of secondary variable orders.

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.

22. The method of claim 21 wherein determining the effectiveness of the variable orders depends on the sizes of the BDDs built using the variable order.

23. The method of claim 21 wherein partitioning the circuit design comprises:

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.

27. The computer-implemented method of claim 26 wherein selecting a variable order comprises:

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.

30. The method of claim 29 wherein the abstract decision diagram for the at least one primary output has a final variable order, and the method further comprises selecting the final variable order as an initial variable order for building a decision diagram for the at least one primary output.

31. The method of claim 29 wherein the plurality of internal nodes comprises a cutset of the internal nodes of the circuit design.

32. The method of claim 29 further comprising:

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.

35. The method of claim 34 wherein the decomposition points correspond to nodes of the circuit design, and method further comprises simulating the circuit design with at least one test vector, observing values at the nodes of the circuit design corresponding to the decomposition points, and forming the first set of values based on the observed values.

36. The method of claim 35 wherein the building the plurality of decision diagrams for the at least one primary output using the values assigned to the decomposition points is done using dynamic variable reordering.