read_blif_mv prodcell.mv
flatten_hierarchy
static_order -s input_and_latch prodcell.ord
build_partition_mdds
incremental_ctl_verification -n -D2 -s prodcell.ctl
flatten_hierarchy
static_order -s input_and_latch prodcell.ord
build_partition_mdds
set image_farside_method 1
model_check -c -r -D0 -i -v2 -d1 prodcell.ctl
quit -s