read_blif_mv fpmpy.mv
flatten_hierarchy
static_order
dynamic_var_ordering -e sift
build_partition_mdds
check_invariant -A 1 fpmpy.inv
model_check fpmpy.ctl
quit -s