summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/vloghtb/common.sh39
-rwxr-xr-xtests/vloghtb/run-test.sh5
-rw-r--r--tests/vloghtb/test_mapopt.sh11
-rw-r--r--tests/vloghtb/test_share.sh27
4 files changed, 52 insertions, 30 deletions
diff --git a/tests/vloghtb/common.sh b/tests/vloghtb/common.sh
index dc8aec08..704afdd9 100644
--- a/tests/vloghtb/common.sh
+++ b/tests/vloghtb/common.sh
@@ -1,7 +1,42 @@
-log_pass() {
+log_pass()
+{
printf "%-15s %s %s %s\n" "$1" "$2" "`printf "%20s" "$2" | tr -d a-zA-Z0-9_ | tr ' ' .`" "pass."
}
-log_fail() {
+log_fail()
+{
printf "%-15s %s %s %s\n" "$1" "$2" "`printf "%20s" "$2" | tr -d a-zA-Z0-9_ | tr ' ' .`" "FAIL."
}
+
+test_equiv()
+{
+ # Usage:
+ # test_equiv <test_name> <synth_script> <sat_options> <mod_name> <vlog_file>
+
+ mkdir -p log_test_$1
+ rm -f log_test_$1/$4.txt
+ rm -f log_test_$1/$4.err
+
+ if ! ../../yosys -q -l log_test_$1/$4.out - 2> /dev/null <<- EOT
+ read_verilog $5
+ proc;;
+
+ copy $4 gold
+ rename $4 work
+
+ cd work
+ $2
+ cd ..
+
+ miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold work miter
+ sat $3 -verify -prove trigger 0 -show-inputs -show-outputs miter
+ EOT
+ then
+ log_fail test_$1 $4
+ mv log_test_$1/$4.out log_test_$1/$4.err
+ exit 1
+ fi
+
+ log_pass test_$1 $4
+ mv log_test_$1/$4.out log_test_$1/$4.txt
+}
diff --git a/tests/vloghtb/run-test.sh b/tests/vloghtb/run-test.sh
index 0e01fd64..3b8a3e9e 100755
--- a/tests/vloghtb/run-test.sh
+++ b/tests/vloghtb/run-test.sh
@@ -7,8 +7,9 @@ wget http://www.clifford.at/yosys/nogit/vloghammer_tb.tar.bz2
tar --strip=1 -xjf vloghammer_tb.tar.bz2
make clean
-make -j4 EXIT_ON_ERROR=1 YOSYS_BIN=$PWD/../../yosys YOSYS_SCRIPT="proc;;" check_yosys
-
rm -rf log_test_*
+
+make -j4 EXIT_ON_ERROR=1 YOSYS_BIN=$PWD/../../yosys YOSYS_SCRIPT="proc;;" check_yosys
make -j4 -f test_makefile MODE=share
+make -j4 -f test_makefile MODE=mapopt
diff --git a/tests/vloghtb/test_mapopt.sh b/tests/vloghtb/test_mapopt.sh
new file mode 100644
index 00000000..9099e2b7
--- /dev/null
+++ b/tests/vloghtb/test_mapopt.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+set -e
+source common.sh
+
+f=$1
+n=$(basename ${f%.v})
+
+test_equiv mapopt "opt; techmap; opt" "-set-def-inputs" $n $f
+
+exit 0
diff --git a/tests/vloghtb/test_share.sh b/tests/vloghtb/test_share.sh
index 88e04281..da221162 100644
--- a/tests/vloghtb/test_share.sh
+++ b/tests/vloghtb/test_share.sh
@@ -1,36 +1,11 @@
#!/bin/bash
set -e
-mkdir -p log_test_share
source common.sh
f=$1
n=$(basename ${f%.v})
-rm -f log_test_share/$n.txt
-rm -f log_test_share/$n.err
+test_equiv share "share -aggressive" "-ignore_div_by_zero" $n $f
-if ! ../../yosys -q -l log_test_share/$n.out - 2> /dev/null <<- EOT
- read_verilog $f
- proc;;
-
- copy $n gold
- rename $n work
-
- cd work
- share -aggressive
- cd ..
-
- miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold work miter
- sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
-EOT
-then
- log_fail test_share $n
- mv log_test_share/$n.out log_test_share/$n.err
- exit 1
-fi
-
-log_pass test_share $n
-mv log_test_share/$n.out log_test_share/$n.txt
exit 0
-