aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-03-09 20:38:59 +0000
committerMichalis Pardalos <m.pardalos@gmail.com>2021-03-09 21:04:54 +0000
commiteffa7bf4c59bb229a5db17fcea3e9c1889145cba (patch)
treedc6b795c35296f154ea03be72f24e0a81cef1345
parentf2475c07f2c44b5463f5f1ef610e0713ddc01888 (diff)
downloadvericert-effa7bf4c59bb229a5db17fcea3e9c1889145cba.tar.gz
vericert-effa7bf4c59bb229a5db17fcea3e9c1889145cba.zip
Parallelize runner script, make it work on other benchmarks
-rwxr-xr-xbenchmarks/polybench-syn/run-vericert.sh53
-rwxr-xr-xbenchmarks/run-vericert.sh78
2 files changed, 78 insertions, 53 deletions
diff --git a/benchmarks/polybench-syn/run-vericert.sh b/benchmarks/polybench-syn/run-vericert.sh
deleted file mode 100755
index bf3e850..0000000
--- a/benchmarks/polybench-syn/run-vericert.sh
+++ /dev/null
@@ -1,53 +0,0 @@
-#! /bin/bash
-
-#set up
-while read -r benchmark ; do
- echo "Running $benchmark"
- clang -Wall -Werror -fsanitize=undefined "$benchmark".c -o "$benchmark".o
- ./"$benchmark".o > "$benchmark".clog
- cresult="$(cut -d' ' -f2 "$benchmark".clog)"
- echo "C output: $cresult"
- { time ../../bin/vericert -DSYNTHESIS $@ --debug-hls "$benchmark".c -o "$benchmark".v ; vericert_result=$? ; } 2> "$benchmark".comp
- iverilog -o "$benchmark".iver -- "$benchmark".v
- iverilog_result=$?
-
- timeout 1m ./"$benchmark".iver > "$benchmark".tmp
- if [ $? -eq 124 ]; then
- timeout=1
- else
- veriresult="$(tail -1 "$benchmark".tmp | cut -d' ' -f2)"
- fi
- cycles="$(tail -4 "$benchmark".tmp | head -1 | tr -s ' ' | cut -d' ' -f3)"
- ctime="$(head -2 "$benchmark".comp | tail -1 | xargs | cut -d' ' -f2 | cut -d'm' -f2 | sed 's/s//g')"
- echo "Veri output: $veriresult"
-
- if [ -n "$timeout" ]; then
- echo "FAIL: Verilog timed out"
- result="timeout"
- elif [ "$vericert_result" -ne 0 ]; then
- #Undefined
- echo "FAIL: Vericert failed"
- result="compile error"
- elif [ "$iverilog_result" -ne 0 ]; then
- #Undefined
- echo "FAIL: iverilog failed"
- result="elaboration error"
- elif [ -z "$veriresult" ]; then
- #Undefined
- echo "FAIL: Verilog returned nothing"
- result="timeout"
- elif [ "$veriresult" == "x" ]; then
- # Don't care
- echo "FAIL: Verilog returned don't cares"
- result="dontcare"
- elif [ "$cresult" -ne "$veriresult" ]; then
- # unequal result
- echo "FAIL: Verilog and C output do not match!"
- result="incorrect result"
- else
- echo "PASS"
- result="pass"
- fi
- name=$(echo "$benchmark" | awk -v FS="/" '{print $NF}')
- echo "$name,$cycles,$ctime,$result,$cresult,$veriresult" >> exec.csv
-done < benchmark-list-master
diff --git a/benchmarks/run-vericert.sh b/benchmarks/run-vericert.sh
new file mode 100755
index 0000000..eb23047
--- /dev/null
+++ b/benchmarks/run-vericert.sh
@@ -0,0 +1,78 @@
+#! /bin/bash
+
+# Kill children on Ctrl-c. I have no idea how or why this works
+trap 'trap " " SIGTERM; kill 0; wait;' SIGINT SIGTERM
+
+function error() { echo "$1" >&2; }
+function crash() { echo "$1" >&2; exit 1; }
+function info() { echo "$1" >&2; }
+
+[ $# -ge 1 ] || crash "Usage: $0 <benchmark-suite>"
+benchmark_dir="$1"
+
+[ -f "$benchmark_dir/benchmark-list-master" ] || crash "$benchmark_dir/benchmark-list-master does not exist"
+
+vericert=../bin/vericert
+[ -x $vericert ] || crash "Vericert executable does not exist or is not marked as executable. Did you run make; make install?"
+
+function run_benchmark() {
+ benchmark_rel="$1"
+ benchmark="$benchmark_dir/$benchmark_rel"
+ [ -f "$benchmark.c" ] || { error "$benchmark.c does not exist"; return; }
+
+ info "[$benchmark] Running"
+ clang -Wall -Werror -fsanitize=undefined "$benchmark".c -o "$benchmark".o
+ ./"$benchmark".o > "$benchmark".clog
+ cresult=$(cut -d' ' -f2 "$benchmark.clog")
+ info "[$benchmark] C output: $cresult"
+ { time ../bin/vericert -DSYNTHESIS --debug-hls "$benchmark.c" -o "$benchmark.v" ; vericert_result=$? ; } 2> "$benchmark".comp
+
+ iverilog -o "$benchmark".iver -- "$benchmark".v
+ iverilog_result=$?
+
+ timeout 10m ./"$benchmark".iver > "$benchmark".tmp
+ if [ $? -eq 124 ]; then
+ timeout=1
+ else
+ veriresult="$(tail -1 "$benchmark".tmp | cut -d' ' -f2)"
+ fi
+ cycles="$(tail -4 "$benchmark".tmp | head -1 | tr -s ' ' | cut -d' ' -f3)"
+ ctime="$(head -2 "$benchmark".comp | tail -1 | xargs | cut -d' ' -f2 | cut -d'm' -f2 | sed 's/s//g')"
+ info "[$benchmark] Veri output: $veriresult"
+
+
+ if [ -n "$timeout" ]; then
+ info "[$benchmark] FAIL: Verilog timed out"
+ result="timeout"
+ elif [ "$vericert_result" -ne 0 ]; then
+ #Undefined
+ info "[$benchmark] FAIL: Vericert failed"
+ result="compile error"
+ elif [ "$iverilog_result" -ne 0 ]; then
+ #Undefined
+ info "[$benchmark] FAIL: iverilog failed"
+ result="elaboration error"
+ elif [ -z "$veriresult" ]; then
+ #Undefined
+ info "[$benchmark] FAIL: Verilog returned nothing"
+ result="timeout"
+ elif [ "$veriresult" == "x" ]; then
+ # Don't care
+ info "[$benchmark] FAIL: Verilog returned don't cares"
+ result="dontcare"
+ elif [ "$cresult" -ne "$veriresult" ]; then
+ # unequal result
+ info "[$benchmark] FAIL: Verilog and C output do not match!"
+ result="incorrect result"
+ else
+ info "[$benchmark] PASS"
+ result="pass"
+ fi
+ name=$(echo "$benchmark" | awk -v FS="/" '{print $NF}')
+ echo "$name,$cycles,$ctime,$result"
+}
+
+while read -r benchmark_rel; do
+ run_benchmark "$benchmark_rel" >> "$benchmark_dir-exec.csv" &
+done < "$benchmark_dir/benchmark-list-master"
+wait