Optimize IFV run scripts

ifv/go.sh

@@ -23,6 +23,18 @@ ifv \
 	+bind_top+bind_info \
 	+nocopyright \
 	-q \
+	# +nohal \
+	# +disable_xcheck \
+	# +bb_gen \
 	# +gui
 
-simvisdbutil -vcd $WORK_DIR/examples -output $EXAMPLE_DIR/counter.vcd -overwrite >/dev/null 2>&1
+# Export counter-example as VCD file
+
+if [ ! -z "$(ls $WORK_DIR/examples)" ]; then
+	echo "Converting counter-example to VCD ..."
+	simvisdbutil \
+		-vcd $WORK_DIR/examples \
+		-output $EXAMPLE_DIR/counter.vcd \
+		-overwrite \
+		>/dev/null 2>&1
+fi

ifv/run.tcl

@@ -4,11 +4,23 @@
 
 reset
 
-clock -add clk -width 1 -period 1 -offset 0
+# clock -add clk1 -width 1 -period 2
+# clock -add clk2 -width 1 -period 2
+# clock -add clk3 -width 1 -period 2
+clock -add clk -width 1 -period 2
 
+force reset 0
+run 2
 force reset 1
+run 2
 
-run 4
+clock -show
+
+# The supported values are 'Auto', 'Axe', 'Axe1', 'Axe2', 'Sword', 'Sword1',
+# 'Sword2', 'Bow', 'Bow1', 'Bow2', 'Bow3', 'Hammer', 'Hammer1', 'Spear',
+# 'Spear1', 'Spear2'.
+
+# define engine hammer
 
 init -load -current
 
@@ -21,8 +33,23 @@ constraint -add -pin reset 0 -reset
 define effort 5 minutes
 define delay_assertion 2
 
+# Disable design partitioning algorithm. This cuts down the verification test
+# of the incorrect arbiter circuit (with tied inputs optimization) fom 30 down
+# to 20 seconds.
+define halo off
+
+# brings it down to 16
+define witness_check off
+
+report
+
+# exit
+
+# check -show
+
 prove
 
-debug circuit.u1.deadlock_free -sstexport examples -overwrite
+# debug system.no_multiple_grants -sstexport examples -overwrite
+debug u1.deadlock_free -sstexport examples -overwrite
 
 exit