read_blif_mv arbiter.mv
flatten_hierarchy
build_partition_maigs
bounded_model_check -m1 -k5 -v1 arbiter.ltl
time
quit -s