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