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