Ordering and Partitioning The next step towards verification consists of converting this network representation into a functional description that represents the output and next state variables as a function of the inputs and current state variables. We use the BDD (binary decision diagram) and its extension the MDD (multivalued decision diagram) to represent boolean and discrete functions. Before creating the MDDs, it is necessary to order the variables in the support of the MDD. This is accomplished by the static_order command, which gives an initial ordering. To undo the current ordering, reinvoke the command flatten_hierarchy. At any stage the current variable ordering can be written out to a file using the write_order command. The build_partition_mdds command computes the transition function MDDs. Depending on the partitioning method selected, the MDDs for the combinational outputs (COs) are built in terms of either the combinational inputs (CIs) or some subset of intermediate nodes of the network. The MDDs built are stored in a DAG called a ``partition''. The vertices of a partition correspond to the CIs, COs, and any intermediate nodes used. Each vertex has a multi-valued function (represented by an MDD) expressing the function of the corresponding network node in terms of the partition vertices in its transitive fanin. Hence, the MDDs of the partition represent a partial collapsing of the network. The inout method represents one extreme where no intermediate nodes are used, and total represents the other extreme where every node in the network has a corresponding vertex in the partition. The frontier method creates vertices for intermediate nodes as necessary in order to control the BDD size. The BDD size at which a new vertex is created is controlled by the parameter partition_threshold. This partition method encompasses the other two (a large value of partition_threshold leads to ``inout'' method and a zero value for partition_threshold leads to ``total''). The partition graph can be printed to a file with the print_partition command. Another related command is the print_partition_stats command that prints statistics on the partition graph.

Contact 

©2002-2018 U.C. Regents