next up previous
Next: FSM Traversal and Image Up: Verification In VIS Previous: Ordering and Partitioning

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.



Roderick Bloem
2001-05-21
Contact 
©2002-2018 U.C. Regents