Dynamic Re-ordering

Dynamic ordering of variables may be enabled and disabled using the dynamic_var_ordering command. Dynamic ordering is a technique to reorder the MDD variables to reduce the size of the existing MDDs. Available methods for dynamic reordering are window and sift . Dynamic ordering (especially using sift) may be time consuming, but can often reduce the size of the MDDs dramatically.

Dynamic ordering is best invoked explicitly (using the dynamic_var_ordering -f <method> option) after the build_partition_mdds and print_img_info commands. If dynamic ordering finds a good ordering, then you may wish to save this ordering (using write_order < file>) and reuse it (using static_order -s < method ><file>). With option dynamic_var_ordering -e < method> dynamic ordering is automatically invoked once a certain threshold on the overall MDD size is reached. Enabling dynamic ordering may slow down the verification, but it can make the difference between completing and not completing a verification task.