From ebe29b66593414d0317879359d1f1d1f61a9ecc4 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 7 Jun 2019 11:05:36 -0700
Subject: [PATCH] Use ABC to convert AIGER to Verilog, then sat against Yosys
---
tests/aiger/run-test.sh | 36 +++++++++++++++---------------------
1 file changed, 15 insertions(+), 21 deletions(-)
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index e0a34f023..70300d305 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -1,24 +1,18 @@
#!/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
+set -e
+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
-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"