1 files changed, 33 insertions, 20 deletions
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index e0a34f023..e56d0fa80 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -1,24 +1,37 @@
 #!/bin/bash
 
-OPTIND=1
-seed=""    # default to no seed specified
-while getopts "S:" opt
-do
-    case "$opt" in
-	S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
-	   seed="SEED=$arg" ;;
-    esac
-done
-shift "$((OPTIND-1))"
-
-# check for Icarus Verilog
-if ! which iverilog > /dev/null ; then
-  echo "$0: Error: Icarus Verilog 'iverilog' not found."
-  exit 1
-fi
+set -e
 
-echo "===== AAG ======"
-${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger"
+for aag in *.aag; do
+    # Since ABC cannot read *.aag, read the *.aig instead
+    # (which would have been created by the reference aig2aig utility)
+    ../../yosys-abc -c "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
+    ../../yosys -p "
+read_verilog ${aag%.*}_ref.v
+prep
+design -stash gold
+read_aiger -clk_name clock $aag
+prep
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 16 miter
+"
+done
 
-echo "===== AIG ======"
-exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aig EXTRA_FLAGS="-f aiger"
+for aig in *.aig; do
+    ../../yosys-abc -c "read -c $aig; write ${aig%.*}_ref.v"
+    ../../yosys -p "
+read_verilog ${aig%.*}_ref.v
+prep
+design -stash gold
+read_aiger -clk_name clock $aig
+prep
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 16 miter
+"
+done