summaryrefslogtreecommitdiff
path: root/tests/vloghtb/common.sh
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-07-21 14:08:13 +0200
committerClifford Wolf <clifford@clifford.at>2014-07-21 14:40:57 +0200
commit668306d00f47989d1f66d139351e63fe2465961c (patch)
tree178c4b43fdc732eb7e7de099afa23cfbb2717425 /tests/vloghtb/common.sh
parent550ac3587302c6c95892c66db2cfa3788b2b5c42 (diff)
Various improvements in test/vloghtb
Diffstat (limited to 'tests/vloghtb/common.sh')
-rw-r--r--tests/vloghtb/common.sh39
1 files changed, 37 insertions, 2 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
+}