source: vis_dev/vis-2.1/share/help/build_partition_mddsCmd.txt @ 14

Last change on this file since 14 was 11, checked in by cecile, 13 years ago

Add vis

File size: 4.1 KB
Line 
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
Note: See TracBrowser for help on using the repository browser.