read_blif_mv eisenberg.mv
init_verify
compute_reach
dynamic_var_ordering -f sift
write_order order
flatten_hierarchy
static_order -s input_and_latch order
build_partition_mdds
compute_reach -v 1
dynamic_var_ordering -f sift
print_fairness
lang_empty -d 0
model_check -d 0 agtrue
model_check -d 0 affalse
read_fairness eisenberg.fair
print_fairness
lang_empty -d 0
model_check -d 0 affalse
time
quit -s