diff options
Diffstat (limited to 'scripts/synth.sh')
-rwxr-xr-x | scripts/synth.sh | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/scripts/synth.sh b/scripts/synth.sh new file mode 100755 index 0000000..79d7164 --- /dev/null +++ b/scripts/synth.sh @@ -0,0 +1,32 @@ +#!/usr/bin/bash + +set -x + +scriptsdir=$(dirname "$(readlink -f "$BASH_SOURCE")") + +if [[ -z "$1" ]]; then + parallel=1 +else + parallel=$1 +fi + +if [[ -z "$2" ]]; then + output=$(pwd) +else + output=$2 +fi + +if [[ -z "$3" ]]; then + source=$(pwd) +else + source=$3 +fi + +echo "copying directory structure from $source to $output" +mkdir -p $output +rsync -am --include '*/' --include '*.v' --exclude '*' $source/ $output/ + +echo "executing $parallel runs in parallel" +cat $scriptsdir/../benchmarks/polybench-syn/benchmark-list-master | \ + xargs --max-procs=$parallel --replace=% \ + $scriptsdir/synth-ssh0.sh % $output |