Add more documentation and clean up benchmarks

12 files changed, 139 insertions, 158 deletions

diff --git a/benchmarks/polybench-syn/common.mk b/benchmarks/polybench-syn/common.mk
new file mode 100644
index 0000000..6508855
--- /dev/null
+++ b/benchmarks/polybench-syn/common.mk
@@ -0,0 +1,26 @@
+VERICERT ?= vericert
+VERICERT_OPTS ?= -DSYNTHESIS
+
+IVERILOG ?= iverilog
+IVERILOG_OPTS ?=
+
+%.v: %.c
+	$(VERICERT) $(VERICERT_OPTS) $< -o $@
+
+%.iver: %.v
+	$(IVERILOG) $(IVERILOG_OPTS) $< -o $@
+
+%.gcc: %.c
+	$(CC) $(CFLAGS) $< -o $@
+
+%: %.iver %.gcc
+	cp $< $@
+
+clean:
+	rm -f *.iver
+	rm -f *.v
+	rm -f *.gcc
+
+.PRECIOUS: %.v
+.PHONY: all clean
+.SUFFIXES:
diff --git a/benchmarks/polybench-syn/data-mining/Makefile b/benchmarks/polybench-syn/data-mining/Makefile
new file mode 100644
index 0000000..cbe138d
--- /dev/null
+++ b/benchmarks/polybench-syn/data-mining/Makefile
@@ -0,0 +1,3 @@
+all: covariance
+
+include ../common.mk
diff --git a/benchmarks/polybench-syn/linear-algebra/blas/Makefile b/benchmarks/polybench-syn/linear-algebra/blas/Makefile
new file mode 100644
index 0000000..5c6d300
--- /dev/null
+++ b/benchmarks/polybench-syn/linear-algebra/blas/Makefile
@@ -0,0 +1,3 @@
+all: gemm gemver gesummv symm syr2k syrk trmm
+
+include ../common.mk
diff --git a/benchmarks/polybench-syn/linear-algebra/blas/trmm.preproc.c b/benchmarks/polybench-syn/linear-algebra/blas/trmm.preproc.c
deleted file mode 100644
index 9b8edfe..0000000
--- a/benchmarks/polybench-syn/linear-algebra/blas/trmm.preproc.c
+++ /dev/null
@@ -1,144 +0,0 @@
-/**
- * This version is stamped on May 10, 2016
- *
- * Contact:
- *   Louis-Noel Pouchet <pouchet.ohio-state.edu>
- *   Tomofumi Yuki <tomofumi.yuki.fr>
- *
- * Web address: http://polybench.sourceforge.net
- */
-/* trmm.c: this file is part of PolyBench/C */
-
-#include <stdio.h>
-#include <unistd.h>
-#include <string.h>
-#include <math.h>
-
-/* Include polybench common header. */
-#include<polybench.h>
-# 1 "trmm.c"
-# 1 "<built-in>" 1
-# 1 "<built-in>" 3
-# 362 "<built-in>" 3
-# 1 "<command line>" 1
-# 1 "<built-in>" 2
-# 1 "trmm.c" 2
-# 1 "utilities/polybench.h" 1
-# 30 "utilities/polybench.h"
-# 1 "/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/stdlib.h" 1 3 4
-# 31 "utilities/polybench.h" 2
-# 231 "utilities/polybench.h"
-extern void* polybench_alloc_data(unsigned long long int n, int elt_size);
-extern void polybench_free_data(void* ptr);
-
-
-
-
-extern void polybench_flush_cache();
-extern void polybench_prepare_instruments();
-# 2 "trmm.c" 2
-
-
-# 1 "./linear-algebra/blas/trmm/trmm.h" 1
-# 5 "trmm.c" 2
-
-
-
-static
-void init_array(int m, int n,
-  int *alpha,
-  int A[ 20 + 0][20 + 0],
-  int B[ 20 + 0][30 + 0])
-{
-  int i, j;
-
-  *alpha = 1.5;
-  for (i = 0; i < m; i++) {
-    for (j = 0; j < i; j++) {
-      A[i][j] = (int)((i+j) % m)/m;
-    }
-    A[i][i] = 1.0;
-    for (j = 0; j < n; j++) {
-      B[i][j] = (int)((n+(i-j)) % n)/n;
-    }
- }
-
-}
-
-
-
-
-static
-void print_array(int m, int n,
-   int B[ 20 + 0][30 + 0])
-{
-  int i, j;
-
-  fprintf(stderr, "==BEGIN DUMP_ARRAYS==\n");
-  fprintf(stderr, "begin dump: %s", "B");
-  for (i = 0; i < m; i++)
-    for (j = 0; j < n; j++) {
- if ((i * m + j) % 20 == 0) fprintf (stderr, "\n");
- fprintf (stderr, "%d ", B[i][j]);
-    }
-  fprintf(stderr, "\nend   dump: %s\n", "B");
-  fprintf(stderr, "==END   DUMP_ARRAYS==\n");
-}
-
-
-
-
-static
-void kernel_trmm(int m, int n,
-   int alpha,
-   int A[ 20 + 0][20 + 0],
-   int B[ 20 + 0][30 + 0])
-{
-  int i, j, k;
-# 68 "trmm.c"
-#pragma scop
- for (i = 0; i < m; i++)
-     for (j = 0; j < n; j++) {
-        for (k = i+1; k < m; k++)
-           B[i][j] += A[k][i] * B[k][j];
-        B[i][j] = alpha * B[i][j];
-     }
-#pragma endscop
-
-}
-
-
-int main(int argc, char** argv)
-{
-
-  int m = 20;
-  int n = 30;
-
-
-  int alpha;
-  int (*A)[20 + 0][20 + 0]; A = (int(*)[20 + 0][20 + 0])polybench_alloc_data ((20 + 0) * (20 + 0), sizeof(int));;
-  int (*B)[20 + 0][30 + 0]; B = (int(*)[20 + 0][30 + 0])polybench_alloc_data ((20 + 0) * (30 + 0), sizeof(int));;
-
-
-  init_array (m, n, &alpha, *A, *B);
-
-
-                             ;
-
-
-  kernel_trmm (m, n, alpha, *A, *B);
-
-
-                            ;
-                             ;
-
-
-
-  if (argc > 42 && ! strcmp(argv[0], "")) print_array(m, n, *B);
-
-
-  free((void*)A);;
-  free((void*)B);;
-
-  return 0;
-}
diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/Makefile b/benchmarks/polybench-syn/linear-algebra/kernels/Makefile
new file mode 100644
index 0000000..ff59d0f
--- /dev/null
+++ b/benchmarks/polybench-syn/linear-algebra/kernels/Makefile
@@ -0,0 +1,3 @@
+all: 2mm 3mm atas bicg doitgen mvt
+
+include ../common.mk
diff --git a/benchmarks/polybench-syn/linear-algebra/solvers/Makefile b/benchmarks/polybench-syn/linear-algebra/solvers/Makefile
new file mode 100644
index 0000000..d466d15
--- /dev/null
+++ b/benchmarks/polybench-syn/linear-algebra/solvers/Makefile
@@ -0,0 +1,3 @@
+all: cholesky durbin lu ludcmp trisolv
+
+include ../common.mk
diff --git a/benchmarks/polybench-syn/medley/Makefile b/benchmarks/polybench-syn/medley/Makefile
new file mode 100644
index 0000000..a64c56d
--- /dev/null
+++ b/benchmarks/polybench-syn/medley/Makefile
@@ -0,0 +1,3 @@
+all: floyd-warshall nussinov
+
+include ../common.mk
diff --git a/benchmarks/polybench-syn/stencils/Makefile b/benchmarks/polybench-syn/stencils/Makefile
new file mode 100644
index 0000000..cf23dc6
--- /dev/null
+++ b/benchmarks/polybench-syn/stencils/Makefile
@@ -0,0 +1,6 @@
+all: adi fdtd-2d heat-3d jacobi-1d jacobi-2d seidel-2d
+
+include ../common.mk
+
+adi.v: adi.c
+	$(VERICERT) $(VERICERT_OPTS) -O0 -finline $< -o $@
diff --git a/benchmarks/polybench-syn/stencils/adi.c b/benchmarks/polybench-syn/stencils/adi.c
index ec2bf2a..2f4aca3 100644
--- a/benchmarks/polybench-syn/stencils/adi.c
+++ b/benchmarks/polybench-syn/stencils/adi.c
@@ -15,28 +15,23 @@
 #include <stdio.h>
 #endif 
 
-#define plus(i) i = i + ONE
-
 static
-void init_array (int n,
-   int u[ 20 + 0][20 + 0])
+void init_array (int n, int u[ 20 + 0][20 + 0])
 {
   int i, j;
 
   for (i = 0; i < n; i++)
     for (j = 0; j < n; j++)
-      {
- u[i][j] = divider((int)(i + n-j) ,n);
-      }
+    {
+      u[i][j] = divider((int)(i + n-j), n);
+    }
 }
 
 
 
 
 static
-int print_array(int n,
-   int u[ 20 + 0][20 + 0])
-
+int print_array(int n, int u[ 20 + 0][20 + 0])
 {
   int i, j;
   int res = 0;
@@ -53,10 +48,10 @@ int print_array(int n,
 }
 static
 void kernel_adi(int tsteps, int n,
-  int u[ 20 + 0][20 + 0],
-  int v[ 20 + 0][20 + 0],
-  int p[ 20 + 0][20 + 0],
-  int q[ 20 + 0][20 + 0])
+                int u[ 20 + 0][20 + 0],
+                int v[ 20 + 0][20 + 0],
+                int p[ 20 + 0][20 + 0],
+                int q[ 20 + 0][20 + 0])
 {
   int t, i, j;
   int B1, B2;
diff --git a/scripts/docker/Dockerfile b/scripts/docker/Dockerfile
index 3e9d4ff..9612938 100644
--- a/scripts/docker/Dockerfile
+++ b/scripts/docker/Dockerfile
@@ -2,3 +2,12 @@ FROM nixos/nix
 
 RUN nix-channel --add https://nixos.org/channels/nixpkgs-unstable nixpkgs
 RUN nix-channel --update
+
+RUN nix-env -i yosys git tmux vim gcc iverilog
+
+RUN git clone --recursive https://github.com/ymherklotz/vericert
+
+WORKDIR /vericert
+RUN git checkout -b oopsla21
+RUN nix-shell --run "make -j7"
+RUN nix-shell --run "make install"
diff --git a/scripts/docker/artifact.org b/scripts/docker/artifact.org
new file mode 100644
index 0000000..0f9ca8b
--- /dev/null
+++ b/scripts/docker/artifact.org
@@ -0,0 +1,74 @@
+#+title: Vericert OOPSLA 2021 Artifact
+#+options: toc:nil num:nil author:nil date:nil
+#+latex_class: scrartcl
+
+This artifact should support the claims made in the paper "Formal Verification of High-Level Synthesis".  In the paper, our tool Vericert was referred to as using the temporary name "HLSCert". The claims that can be verified by the paper are the following:
+
+- The mechanised proof of correctness of the translation from C into Verilog is provided and can be checked and rerun.
+- All 27 PolyBench benchmarks can be recompiled using Vericert.
+- The cycle counts of Vericert on the benchmarks can be checked and compared against LegUp 4.0.
+- If Vivado is downloaded separately, then the whole performance section can be checked, including all the graphs that appear in the paper.
+
+** Claims that are not supported by the artifact
+
+Unfortunately, we could not include our version of LegUp 4.0 in the artifact due to license restrictions.  In addition to that, LegUp was recently bought by Microchip and renamed to SmartHLS[fn:1], which means that it also cannot be freely downloaded anymore either, and the original open source version of LegUp 4.0 is not available anymore due to server issues in Toronto[fn:2].  We have tried contacting the authors of LegUp in Toronto, but have not heard back yet on if our version of LegUp can be shared in the artifact.
+
+Instead, we have included the net lists that LegUp generated from the benchmarks in the artifact, with all the optimisation levels that were tried, however, it does mean that these cannot be verified again and that other optimisation options cannot be tried.
+
+In addition to that, the Vivado synthesis tool by Xilinx[fn:3] is also commercial (but free to download), and therefore cannot be bundled into the artifact either.  This synthesis tool was used to get accurate timing information about how the design would run on an FPGA, and also give the area that the design would take up on the FPGA.  To be able to reproduce these results, it would therefore need Vivado to be set up so that the scripts can run.
+
+* Kick the tyres
+
+First, the docker image needs to be downloaded and run, which contains the git repository:
+
+#+begin_src shell
+docker pull ymherklotz/vericert
+docker run -it ymherklotz/vericert sh
+#+end_src
+
+Then, one just has to go into the directory which contains the git repository and open a ~nix-shell~, which will load a shell with all the correct dependencies loaded:
+
+#+begin_src shell
+cd /vericert
+nix-shell
+#+end_src
+
+Then, any commands can be run in this shell to run ~vericert~, which has already been compiled and can be found in the ~/vericert/bin~ directory.  For a quick test that it is working, a few very simple examples in the ~/vericert/test~ directory can be run using:
+
+#+begin_src shell
+make test
+#+end_src
+
+If this finishes without errors, it means that Vericert is working correctly.
+
+* Detailed Artifact Description
+
+This section describes the detailed instructions to get the results for the different sections of the paper, first describing the structure of the proof and how to execute Vericert manually, to finally running Vericert on the benchmarks and get the cycle counts for the Vericert designs as well as the precompiled LegUp designs.
+
+** How to manually compile using Vericert
+
+To compile arbitrary C files, the following command can be used:
+
+#+begin_src shell
+vericert main.c -o main.v
+#+end_src
+
+Which will generate a Verilog file with a corresponding test bench.  The Verilog file can then be simulated by using the Icarus Verilog simulator:
+
+#+begin_src shell
+iverilog main.v -o main
+./main
+#+end_src
+
+This should print out the return value from the main function in addition to the number of cycles that it took to execute the hardware design.
+
+** Getting cycle counts for Vericert
+
+There are two benchmark sets for which the results are given in the paper.
+To get the cycle counts for Vericert from the benchmarks
+
+* Footnotes
+
+[fn:3] https://www.xilinx.com/support/download.html
+[fn:2] https://legup.eecg.utoronto.ca
+[fn:1] https://www.microsemi.com/product-directory/fpga-design-tools/5590-hls#software-download
diff --git a/scripts/docker/artifact.pdf b/scripts/docker/artifact.pdf
new file mode 100644
index 0000000..6571f97
--- /dev/null
+++ b/scripts/docker/artifact.pdf