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 |
---|