Use ABC to convert AIGER to Verilog, then sat against Yosys

tests/aiger/run-test.sh

@@ -1,24 +1,18 @@
 #!/bin/bash
 
-OPTIND=1
+set -e
-seed=""    # default to no seed specified
+for aig in *.aig; do
-while getopts "S:" opt
+    ../../yosys-abc -c "read -c $aig; write ${aig%.*}_ref.v"
-do
+    ../../yosys -p "
-    case "$opt" in
+read_verilog ${aig%.*}_ref.v
-	S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
+prep
-	   seed="SEED=$arg" ;;
+design -stash gold
-    esac
+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
-shift "$((OPTIND-1))"
-
-# check for Icarus Verilog
-if ! which iverilog > /dev/null ; then
-  echo "$0: Error: Icarus Verilog 'iverilog' not found."
-  exit 1
-fi
-
-echo "===== AAG ======"
-${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger"
-
-echo "===== AIG ======"
-exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aig EXTRA_FLAGS="-f aiger"