diff options
Diffstat (limited to 'tests/aiger')
30 files changed, 214 insertions, 0 deletions
diff --git a/tests/aiger/.gitignore b/tests/aiger/.gitignore new file mode 100644 index 00000000..9a26bb8f --- /dev/null +++ b/tests/aiger/.gitignore @@ -0,0 +1 @@ +/*_ref.v diff --git a/tests/aiger/and_.aag b/tests/aiger/and_.aag new file mode 100644 index 00000000..cadd505f --- /dev/null +++ b/tests/aiger/and_.aag @@ -0,0 +1,8 @@ +aag 3 2 0 1 1 +2 +4 +6 +6 2 4 +i0 pi0 +i1 pi1 +o0 po0 diff --git a/tests/aiger/and_.aig b/tests/aiger/and_.aig new file mode 100644 index 00000000..13c7a0c1 --- /dev/null +++ b/tests/aiger/and_.aig @@ -0,0 +1,5 @@ +aig 3 2 0 1 1 +6 +i0 pi0 +i1 pi1 +o0 po0 diff --git a/tests/aiger/buffer.aag b/tests/aiger/buffer.aag new file mode 100644 index 00000000..211106ed --- /dev/null +++ b/tests/aiger/buffer.aag @@ -0,0 +1,5 @@ +aag 1 1 0 1 0 +2 +2 +i0 pi0 +o0 po0 diff --git a/tests/aiger/buffer.aig b/tests/aiger/buffer.aig new file mode 100644 index 00000000..01df6f1c --- /dev/null +++ b/tests/aiger/buffer.aig @@ -0,0 +1,4 @@ +aig 1 1 0 1 0 +2 +i0 pi0 +o0 po0 diff --git a/tests/aiger/cnt1.aag b/tests/aiger/cnt1.aag new file mode 100644 index 00000000..75598862 --- /dev/null +++ b/tests/aiger/cnt1.aag @@ -0,0 +1,4 @@ +aag 1 0 1 0 0 1 +2 3 +2 +b0 po0 diff --git a/tests/aiger/cnt1.aig b/tests/aiger/cnt1.aig new file mode 100644 index 00000000..6fcf6252 --- /dev/null +++ b/tests/aiger/cnt1.aig @@ -0,0 +1,4 @@ +aig 1 0 1 0 0 1 +3 +2 +b0 po0 diff --git a/tests/aiger/cnt1e.aag b/tests/aiger/cnt1e.aag new file mode 100644 index 00000000..35cd5a48 --- /dev/null +++ b/tests/aiger/cnt1e.aag @@ -0,0 +1,9 @@ +aag 5 1 1 0 3 1 +2 +4 10 +4 +6 5 3 +8 4 2 +10 9 7 +b0 AIGER_NEVER +i0 po0 diff --git a/tests/aiger/cnt1e.aig b/tests/aiger/cnt1e.aig new file mode 100644 index 00000000..7284dd42 --- /dev/null +++ b/tests/aiger/cnt1e.aig @@ -0,0 +1,5 @@ +aig 5 1 1 0 3 1 +10 +4 +i0 po0 +b0 AIGER_NEVER diff --git a/tests/aiger/empty.aag b/tests/aiger/empty.aag new file mode 100644 index 00000000..40c0f00c --- /dev/null +++ b/tests/aiger/empty.aag @@ -0,0 +1 @@ +aag 0 0 0 0 0 diff --git a/tests/aiger/empty.aig b/tests/aiger/empty.aig new file mode 100644 index 00000000..a28373cd --- /dev/null +++ b/tests/aiger/empty.aig @@ -0,0 +1 @@ +aig 0 0 0 0 0 diff --git a/tests/aiger/false.aag b/tests/aiger/false.aag new file mode 100644 index 00000000..bab4a06a --- /dev/null +++ b/tests/aiger/false.aag @@ -0,0 +1,3 @@ +aag 0 0 0 1 0 +0 +o0 po0 diff --git a/tests/aiger/false.aig b/tests/aiger/false.aig new file mode 100644 index 00000000..4dc442d7 --- /dev/null +++ b/tests/aiger/false.aig @@ -0,0 +1,3 @@ +aig 0 0 0 1 0 +0 +o0 po0 diff --git a/tests/aiger/halfadder.aag b/tests/aiger/halfadder.aag new file mode 100644 index 00000000..5bf54d38 --- /dev/null +++ b/tests/aiger/halfadder.aag @@ -0,0 +1,14 @@ +aag 7 2 0 2 3 +2 +4 +6 +12 +6 13 15 +12 2 4 +14 3 5 +i0 x +i1 y +o0 s +o1 c +c +half adder diff --git a/tests/aiger/halfadder.aig b/tests/aiger/halfadder.aig new file mode 100644 index 00000000..83727ee6 --- /dev/null +++ b/tests/aiger/halfadder.aig @@ -0,0 +1,9 @@ +aig 5 2 0 2 3 +10 +6 +i0 x +i1 y +o0 s +o1 c +c +half adder diff --git a/tests/aiger/inverter.aag b/tests/aiger/inverter.aag new file mode 100644 index 00000000..428bad9e --- /dev/null +++ b/tests/aiger/inverter.aag @@ -0,0 +1,5 @@ +aag 1 1 0 1 0 +2 +3 +i0 pi0 +o0 po0 diff --git a/tests/aiger/inverter.aig b/tests/aiger/inverter.aig new file mode 100644 index 00000000..5bec90ae --- /dev/null +++ b/tests/aiger/inverter.aig @@ -0,0 +1,4 @@ +aig 1 1 0 1 0 +3 +i0 pi0 +o0 po0 diff --git a/tests/aiger/notcnt1.aag b/tests/aiger/notcnt1.aag new file mode 100644 index 00000000..e92815f2 --- /dev/null +++ b/tests/aiger/notcnt1.aag @@ -0,0 +1,4 @@ +aag 1 0 1 0 0 1 +2 3 +3 +b0 AIGER_NEVER diff --git a/tests/aiger/notcnt1.aig b/tests/aiger/notcnt1.aig new file mode 100644 index 00000000..f8a667f1 --- /dev/null +++ b/tests/aiger/notcnt1.aig @@ -0,0 +1,4 @@ +aig 1 0 1 0 0 1 +3 +3 +b0 AIGER_NEVER diff --git a/tests/aiger/notcnt1e.aag b/tests/aiger/notcnt1e.aag new file mode 100644 index 00000000..2ed645d8 --- /dev/null +++ b/tests/aiger/notcnt1e.aag @@ -0,0 +1,9 @@ +aag 5 1 1 0 3 1 +2 +4 10 +5 +6 5 3 +8 4 2 +10 9 7 +b0 AIGER_NEVER +i0 pi0 diff --git a/tests/aiger/notcnt1e.aig b/tests/aiger/notcnt1e.aig new file mode 100644 index 00000000..fd7e9450 --- /dev/null +++ b/tests/aiger/notcnt1e.aig @@ -0,0 +1,5 @@ +aig 5 1 1 0 3 1 +10 +5 +i0 pi0 +b0 AIGER_NEVER diff --git a/tests/aiger/or_.aag b/tests/aiger/or_.aag new file mode 100644 index 00000000..0f619dba --- /dev/null +++ b/tests/aiger/or_.aag @@ -0,0 +1,8 @@ +aag 3 2 0 1 1 +2 +4 +7 +6 3 5 +i0 pi0 +i1 pi1 +o0 po0 diff --git a/tests/aiger/or_.aig b/tests/aiger/or_.aig new file mode 100644 index 00000000..05168751 --- /dev/null +++ b/tests/aiger/or_.aig @@ -0,0 +1,5 @@ +aig 3 2 0 1 1 +7 +i0 pi0 +i1 pi1 +o0 po0 diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh new file mode 100755 index 00000000..4fbffcdc --- /dev/null +++ b/tests/aiger/run-test.sh @@ -0,0 +1,54 @@ +#!/bin/bash + +set -e + +OPTIND=1 +abcprog="berkeley-abc" # default to built-in version of abc +while getopts "A:" opt +do + case "$opt" in + A) abcprog="$OPTARG" ;; + esac +done +shift "$((OPTIND-1))" + +# NB: *.aag and *.aig must contain a symbol table naming the primary +# inputs and outputs, otherwise ABC and Yosys will name them +# arbitrarily (and inconsistently with each other). + +for aag in *.aag; do + # Since ABC cannot read *.aag, read the *.aig instead + # (which would have been created by the reference aig2aig utility, + # available from http://fmv.jku.at/aiger/) + echo "Checking $aag." + $abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v" + ../../yosys -qp " +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 + +for aig in *.aig; do + echo "Checking $aig." + $abcprog -q "read -c $aig; write ${aig%.*}_ref.v" + ../../yosys -qp " +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 diff --git a/tests/aiger/toggle-re.aag b/tests/aiger/toggle-re.aag new file mode 100644 index 00000000..b662bb38 --- /dev/null +++ b/tests/aiger/toggle-re.aag @@ -0,0 +1,14 @@ +aag 7 2 1 2 4 +2 +4 +6 8 +6 +7 +8 4 10 +10 13 15 +12 2 6 +14 3 7 +i0 enable +i1 reset +o0 Q +o1 !Q diff --git a/tests/aiger/toggle-re.aig b/tests/aiger/toggle-re.aig new file mode 100644 index 00000000..9d6730f2 --- /dev/null +++ b/tests/aiger/toggle-re.aig @@ -0,0 +1,8 @@ +aig 7 2 1 2 4 +14 +6 +7 +i0 enable +i1 reset +o0 Q +o1 !Q diff --git a/tests/aiger/toggle.aag b/tests/aiger/toggle.aag new file mode 100644 index 00000000..b1a1582d --- /dev/null +++ b/tests/aiger/toggle.aag @@ -0,0 +1,6 @@ +aag 1 0 1 2 0 +2 3 +2 +3 +o0 po0 +o1 po1 diff --git a/tests/aiger/toggle.aig b/tests/aiger/toggle.aig new file mode 100644 index 00000000..68b41763 --- /dev/null +++ b/tests/aiger/toggle.aig @@ -0,0 +1,6 @@ +aig 1 0 1 2 0 +3 +2 +3 +o0 po0 +o1 po1 diff --git a/tests/aiger/true.aag b/tests/aiger/true.aag new file mode 100644 index 00000000..66a9eab4 --- /dev/null +++ b/tests/aiger/true.aag @@ -0,0 +1,3 @@ +aag 0 0 0 1 0 +1 +o0 po0 diff --git a/tests/aiger/true.aig b/tests/aiger/true.aig new file mode 100644 index 00000000..f9bad600 --- /dev/null +++ b/tests/aiger/true.aig @@ -0,0 +1,3 @@ +aig 0 0 0 1 0 +1 +o0 po0 |