diff options
| author | Eddie Hung <eddie@fpgeh.com> | 2019-06-07 11:05:36 -0700 |
|---|---|---|
| committer | Eddie Hung <eddie@fpgeh.com> | 2019-06-07 11:05:36 -0700 |
| commit | ebe29b66593414d0317879359d1f1d1f61a9ecc4 (patch) | |
| tree | afcc4b47234b312bf52e58e2f5662dfaed392fca /tests/aiger | |
| parent | 1b113a05742377f5b18d52bc5bf50b1991e88c19 (diff) | |
| download | yosys-ebe29b66593414d0317879359d1f1d1f61a9ecc4.tar.gz yosys-ebe29b66593414d0317879359d1f1d1f61a9ecc4.tar.bz2 yosys-ebe29b66593414d0317879359d1f1d1f61a9ecc4.zip | |
Use ABC to convert AIGER to Verilog, then sat against Yosys
Diffstat (limited to 'tests/aiger')
| -rwxr-xr-x | tests/aiger/run-test.sh | 36 |
1 files 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" |