blob: 79d716472d735642bd8921d3778cfe7c7a2f3c0f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
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
|