[14] | 1 | |
---|
| 2 | build_partition_mdds - build a partition of MDDs for the flattened network |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | build_partition_mdds [-h] [-i] [-n <list>] [-s <num>] [-t <seconds>] [-v] |
---|
| 6 | [<method>] |
---|
| 7 | |
---|
| 8 | Build the MDDs of a flattened network. Depending on the method selected, the |
---|
| 9 | MDDs for the combinational outputs (COs) are built in terms of either the |
---|
| 10 | combinational inputs (CIs) or in terms of some subset of intermediate nodes |
---|
| 11 | of the network. The MDDs built are stored in a DAG called a "partition". The |
---|
| 12 | vertices of a partition correspond to the CIs, COs, and any intermediate |
---|
| 13 | nodes used. Each vertex has a multi-valued function (represented by MDDs) |
---|
| 14 | expressing the function of the corresponding network node in terms of the |
---|
| 15 | partition vertices in its transitive fanin. Hence, the MDDs of the partition |
---|
| 16 | represent a partial collapsing of the network. |
---|
| 17 | |
---|
| 18 | This command must be preceded by the commands flatten_hierarchy and |
---|
| 19 | static_order. The partition built is stored with the network for use by |
---|
| 20 | other commands, such as simulate, compute_reach, model_check, etc. This |
---|
| 21 | command has no affect when invoked on a network that already has a |
---|
| 22 | partition. To remove the existing partition of a network, reinvoke |
---|
| 23 | flatten_hierarchy. |
---|
| 24 | |
---|
| 25 | The choice of method determines which intermediate nodes are used. The inout |
---|
| 26 | method represents one extreme where no intermediate nodes are used, and |
---|
| 27 | total represents the other extreme where every node in the network has a |
---|
| 28 | corresponding vertex in the partition. If no method is specified on the |
---|
| 29 | command line, then the value of the flag partition_method is used (this flag |
---|
| 30 | is set by the command set partition_method), unless it does not have a |
---|
| 31 | value, in which case the forntier method is used. The different methods |
---|
| 32 | available are: |
---|
| 33 | |
---|
| 34 | inout Expresses the combinational outputs in terms of the combinational |
---|
| 35 | inputs. |
---|
| 36 | |
---|
| 37 | total The partition built is isomorphic to the combinational part of the |
---|
| 38 | network. The function of each node is expressed in terms of its |
---|
| 39 | immediate fanins. If the -i is used the function attached to each |
---|
| 40 | vertex is computed as a function of the combinational inputs. |
---|
| 41 | |
---|
| 42 | partial Builds a partition using the intermediate nodes specified with the |
---|
| 43 | -n option or the -f option. |
---|
| 44 | |
---|
| 45 | frontier (default) Builds a partition creating vertices for the |
---|
| 46 | intermediate nodes as needed in order to control the BDD size. The |
---|
| 47 | threshold value for the BDD size can be set by the parameter |
---|
| 48 | "partition_threshold". This method encompasses both "inout" (set |
---|
| 49 | partition_threshold parameter to infinity) and "total" (set |
---|
| 50 | partition_threshold parameter to 0). |
---|
| 51 | |
---|
| 52 | boundary Builds a partition in a fashion that preserves all nodes that are |
---|
| 53 | Input/Output nodes of any hnode in the hierarchy rooted at the |
---|
| 54 | current hnode. |
---|
| 55 | |
---|
| 56 | Command options: |
---|
| 57 | |
---|
| 58 | -h |
---|
| 59 | Print the command usage. |
---|
| 60 | |
---|
| 61 | -i |
---|
| 62 | Build the multi-valued functions of each partition vertex in terms of |
---|
| 63 | the combinational inputs, rather than in terms of its transitive |
---|
| 64 | fanin vertices. |
---|
| 65 | |
---|
| 66 | -n <list> |
---|
| 67 | Used in conjunction with the partial method. List is a comma |
---|
| 68 | separated list of network nodes to use as intermediate nodes in the |
---|
| 69 | partition. |
---|
| 70 | |
---|
| 71 | -s <num> |
---|
| 72 | Level of severity of a post-computation check applied to the |
---|
| 73 | partition data structure (0 by default, meaning no check). |
---|
| 74 | |
---|
| 75 | -t <seconds> |
---|
| 76 | Time in seconds allowed to build the partition. If the computation |
---|
| 77 | time goes above that limit, the process of building the partition is |
---|
| 78 | aborted. The default is no limit. |
---|
| 79 | |
---|
| 80 | -v |
---|
| 81 | Turn on the verbosity. |
---|
| 82 | __________________________________________________________ |
---|
| 83 | |
---|
| 84 | Last updated on 20100410 00h02 |
---|