read_blif_mv elevator.mv
# move to a sub module
cd e1
init_verify
# the following should pass
check_invariant -d 0 emodel.inv
read_fairness emodel.fair
# the following should pass the first formula and fail the second
model_check -d 0 emodel.ctl
write_blif_mv emodel.mv
write_blif -c -e elevator.enc emodel.blif
read_blif -e elevator.enc emodel-simp.blif
init_verify
comb_verify emodel.mv
# move back up to the root
cd ..
init_verify
dynamic_var_ordering -f sift
print_img_info
dynamic_var_ordering -f sift
write_order order
# fast flatten - do not need to check tables at this point
flatten_hierarchy
static_order -s input_and_latch order
build_partition_mdds
print_img_info
dynamic_var_ordering -f sift
# the following takes 15 sec on cad. There are 674077 reached states
# reached in 26 BFS.
compute_reach -v 1
read_fairness elevator.fair
check_invariant -d 0 elevator.inv
# this is so slow. maybe not good for regression testing
#lang_empty -d 0
quit -s