aboutsummaryrefslogtreecommitdiffstats
path: root/scripts
diff options
context:
space:
mode:
Diffstat (limited to 'scripts')
-rw-r--r--scripts/docker/Dockerfile2
-rw-r--r--scripts/docker/artifact.org12
-rw-r--r--scripts/docker/artifact.pdfbin273128 -> 273122 bytes
-rw-r--r--scripts/quartus_synth.tcl2
-rwxr-xr-xscripts/synth-ssh-bambu.sh28
-rwxr-xr-xscripts/synth-ssh.sh28
-rw-r--r--scripts/synthesis-results.org4
-rwxr-xr-xscripts/synthesis-results.scm4
8 files changed, 12 insertions, 68 deletions
diff --git a/scripts/docker/Dockerfile b/scripts/docker/Dockerfile
index c66df6d..480acc9 100644
--- a/scripts/docker/Dockerfile
+++ b/scripts/docker/Dockerfile
@@ -9,7 +9,7 @@ ADD legup_polybench_syn.tar.gz /data/legup-polybench-syn
ADD legup_polybench_syn_div.tar.gz /data/legup-polybench-syn-div
ADD data.tar.gz /data
-RUN git clone --recursive https://github.com/ymherklotz/vericert
+RUN git clone --recursive https://github.com/___/vericert
WORKDIR /vericert
RUN git checkout oopsla21
diff --git a/scripts/docker/artifact.org b/scripts/docker/artifact.org
index fa0a936..ec8025d 100644
--- a/scripts/docker/artifact.org
+++ b/scripts/docker/artifact.org
@@ -13,7 +13,7 @@ This artifact should support the claims made in the paper "Formal Verification o
The artifact is available on Github, specifically on the ~oopsla21~ branch:
-https://github.com/ymherklotz/vericert
+https://github.com/___/vericert
#+latex: \noindent
This release is also archived on Zenodo permanently:
@@ -23,7 +23,7 @@ http://doi.org/10.5281/zenodo.5093839
#+latex: \noindent
However, for the purposes of this artifact review, a Docker image has been set up:
-https://hub.docker.com/repository/docker/ymherklotz/vericert
+https://hub.docker.com/repository/docker/___/vericert
** Claims that are not supported by the artifact
@@ -38,8 +38,8 @@ In addition to that, the Vivado synthesis tool by Xilinx[fn:3] is also commercia
First, the docker image needs to be downloaded and run, which contains the git repository:
#+begin_src shell
-docker pull ymherklotz/vericert:1.0
-docker run -it ymherklotz/vericert:1.0 sh
+docker pull ___/vericert:1.0
+docker run -it ___/vericert:1.0 sh
#+end_src
Then, one just has to go into the directory which contains the git repository (~/vericert~) and open a ~nix-shell~, which will load a shell with all the correct dependencies loaded:
@@ -259,7 +259,7 @@ Where $t$ is the tool being considered.
A tex file is included in the ~/data/data~ directory, which unfortunately can only be compiled outside of the docker file, but will recreate the graphs from the paper using the csv files in the directory. This can be achieved using the following commands:
#+begin_src shell
-docker create ymherklotz/vericert:v1.0 # returns container ID
+docker create ___/vericert:v1.0 # returns container ID
docker cp $container_id:/data/data .
docker rm $container_id
cd data
@@ -308,7 +308,7 @@ docker run -it <hash> sh
The only dependency that is require is nix[fn:7]. Once that is installed, we can clone the Github repository and checkout the ~oopsla21~ branch:
#+begin_src shell
-git clone https://github.com/ymherklotz/vericert
+git clone https://github.com/___/vericert
cd vericert
git checkout oopsla21
#+end_src
diff --git a/scripts/docker/artifact.pdf b/scripts/docker/artifact.pdf
index 05ec4fd..d8b7aab 100644
--- a/scripts/docker/artifact.pdf
+++ b/scripts/docker/artifact.pdf
Binary files differ
diff --git a/scripts/quartus_synth.tcl b/scripts/quartus_synth.tcl
index 6edbf0c..61a78c8 100644
--- a/scripts/quartus_synth.tcl
+++ b/scripts/quartus_synth.tcl
@@ -1,6 +1,6 @@
# PRiME pre-KAPow kernel flow
# Performs pre-KAPow run steps for instrumenting arbitrary Verilog for power monitoring
-# James Davis, 2015
+# ___ Davis, 2015
load_package flow
diff --git a/scripts/synth-ssh-bambu.sh b/scripts/synth-ssh-bambu.sh
deleted file mode 100755
index 5bc1a4d..0000000
--- a/scripts/synth-ssh-bambu.sh
+++ /dev/null
@@ -1,28 +0,0 @@
-#!/usr/bin/env bash
-
-# Assumes that the Verilog is passed on the command line, that the tcl file is in synth.tcl and
-# returns encode_report.xml.
-
-scriptsdir=$(dirname "$(readlink -f "$BASH_SOURCE")")
-
-num=$1
-bench=$2
-output=$3
-machine=ee-beholder${num}.ee.ic.ac.uk
-user=ymh15
-files="$scriptsdir/synth-bambu.tcl $output/$bench/main_top.v"
-log="$output/${bench}_synth.log"
-
-date >$log
-
-temp=$(ssh $user@$machine "mktemp -d")
-
->&2 echo "synthesising $bench $temp"
-rsync $files $user@$machine:$temp/ >>$log 2>&1
-ssh $user@$machine \
- "bash -lc 'cd $temp && vivado -mode batch -source synth-bambu.tcl'" \
- >>$log 2>&1
-rsync $user@$machine:$temp/encode_report.xml $output/${bench}_report.xml >>$log 2>&1
-# ssh $user@$machine "rm -rf '$temp'" >>$log 2>&1
-rm -f main.sv >>$log 2>&1
->&2 echo "done $bench"
diff --git a/scripts/synth-ssh.sh b/scripts/synth-ssh.sh
deleted file mode 100755
index ca255e1..0000000
--- a/scripts/synth-ssh.sh
+++ /dev/null
@@ -1,28 +0,0 @@
-#!/usr/bin/env bash
-
-# Assumes that the Verilog is passed on the command line, that the tcl file is in synth.tcl and
-# returns encode_report.xml.
-
-scriptsdir=$(dirname "$(readlink -f "$BASH_SOURCE")")
-
-num=$1
-bench=$2
-output=$3
-machine=ee-beholder${num}.ee.ic.ac.uk
-user=ymh15
-files="$scriptsdir/synth.tcl $output/$bench.sv"
-log="$output/${bench}_synth.log"
-
-date >$log
-
-temp=$(ssh $user@$machine "mktemp -d")
-
->&2 echo "synthesising $bench $temp"
-rsync $files $user@$machine:$temp/ >>$log 2>&1
-ssh $user@$machine \
- "bash -lc 'cd $temp && cp $(basename $bench).sv main.sv && vivado -mode batch -source synth.tcl'" \
- >>$log 2>&1
-rsync $user@$machine:$temp/encode_report.xml $output/${bench}_report.xml >>$log 2>&1
-# ssh $user@$machine "rm -rf '$temp'" >>$log 2>&1
-rm -f main.sv >>$log 2>&1
->&2 echo "done $bench"
diff --git a/scripts/synthesis-results.org b/scripts/synthesis-results.org
index 602b2ba..43ca413 100644
--- a/scripts/synthesis-results.org
+++ b/scripts/synthesis-results.org
@@ -24,11 +24,11 @@ Usage: *synthesis-results* [options...] [files...]
* AUTHOR
-Written by Yann Herklotz.
+Written by ___ ___.
* COPYRIGHT
-Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com>
+Copyright (C) 2022 ___ ___ <___@______.com>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
diff --git a/scripts/synthesis-results.scm b/scripts/synthesis-results.scm
index 3760cfb..db73ed7 100755
--- a/scripts/synthesis-results.scm
+++ b/scripts/synthesis-results.scm
@@ -1,7 +1,7 @@
#! /usr/local/bin/csi -ss
;; -*- mode: scheme -*-
;;
-;; Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com>
+;; Copyright (C) 2022 ___ ___ <___@______.com>
;;
;; This program is free software: you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
@@ -61,7 +61,7 @@
(print "Usage: " (program-name) " [options...] [files...]")
(newline)
(print (args:usage opts))
- (print "Report bugs to git at yannherklotz dot com.")))
+ (print "Report bugs to git at ______ dot com.")))
(exit 1))
(define (map-names n)