aboutsummaryrefslogtreecommitdiffstats
path: root/benchmarks/polybench-syn/run-vericert.sh
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-08-26 19:27:17 +0100
committerMichalis Pardalos <m.pardalos@gmail.com>2021-08-26 19:27:17 +0100
commitb067e5c7b0ecce9ffbf21e9c4a7ff96328dec2ba (patch)
treed36a28e84827fe0bb8d7b87d9afa8475b7b2008e /benchmarks/polybench-syn/run-vericert.sh
parent4dca6dbd48d3e71eb550297d3325555f5e039bb8 (diff)
parent0c021173b3efb1310370de4b2a6f5444c745022f (diff)
downloadvericert-b067e5c7b0ecce9ffbf21e9c4a7ff96328dec2ba.tar.gz
vericert-b067e5c7b0ecce9ffbf21e9c4a7ff96328dec2ba.zip
Merge branch 'oopsla21' into sharing-merge
Diffstat (limited to 'benchmarks/polybench-syn/run-vericert.sh')
-rwxr-xr-xbenchmarks/polybench-syn/run-vericert.sh41
1 files changed, 41 insertions, 0 deletions
diff --git a/benchmarks/polybench-syn/run-vericert.sh b/benchmarks/polybench-syn/run-vericert.sh
new file mode 100755
index 0000000..6cf4cd9
--- /dev/null
+++ b/benchmarks/polybench-syn/run-vericert.sh
@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+
+rm exec.csv
+
+top=$(pwd)
+ #set up
+while read benchmark ; do
+ echo "Running "$benchmark
+ ./$benchmark.gcc > $benchmark.clog
+ cresult=$(cat $benchmark.clog | cut -d' ' -f2)
+ echo "C output: "$cresult
+ ./$benchmark.iver > $benchmark.tmp
+ veriresult=$(tail -1 $benchmark.tmp | cut -d' ' -f2)
+ cycles=$(tail -2 $benchmark.tmp | head -1 | tr -s ' ' | cut -d' ' -f2)
+ echo "Verilog output: "$veriresult
+
+ #Undefined checks
+ if test -z $veriresult
+ then
+ echo "FAIL: Verilog returned nothing"
+ #exit 0
+ fi
+
+ # Don't care checks
+ if [ $veriresult == "x" ]
+ then
+ echo "FAIL: Verilog returned don't cares"
+ #exit 0
+ fi
+
+ # unequal result check
+ if [ $cresult -ne $veriresult ]
+ then
+ echo "FAIL: Verilog and C output do not match!"
+ #exit 0
+ else
+ echo "PASS"
+ fi
+ name=$(echo $benchmark | awk -v FS="/" '{print $NF}')
+ echo $name","$cycles >> exec.csv
+done < benchmark-list-master