Fix the small test bench for Vericert

7 files changed, 67 insertions, 137 deletions

diff --git a/benchmarks/README.md b/benchmarks/README.md
index 59edf78..c10f357 100644
--- a/benchmarks/README.md
+++ b/benchmarks/README.md
@@ -1,14 +1,11 @@
-Hi,
+# Benchmarks
 
-I have collected a set of benchmarks that you may be interested in. The main idea is to run the existing HLS benchmarks to see if they work - they can only test correctness for a single set of input by a customised test bench.
+The main idea is to run the existing HLS benchmarks to see if they work - they can only test correctness for a single set of input by a customised test bench.
 
-* jacob_2d: a benchmark from Polybench
-* sobel: a benchmark from LegUp HLS
-* getTanh: a benchmark from DASS
-* fft: a benchmark from MachSuite
-* KMeans: a benchmark from Felix's work
+- jacob_2d: a benchmark from Polybench
+- sobel: a benchmark from LegUp HLS
+- getTanh: a benchmark from DASS
+- fft: a benchmark from MachSuite
+- KMeans: a benchmark from Felix's work
 
-Note all the benchmark set above (links included in the source code) should be all synthesisable in your case, so you may be show coverage instead of a single benchmark.
-
-Best,
-Jianyi
+Note all the benchmark set above (links included in the source code) should be all synthesisable, so you may be able to show coverage instead of a single benchmark.
diff --git a/benchmarks/polybench-syn-div/exec.csv b/benchmarks/polybench-syn-div/exec.csv
index 8d1f5da..e28109b 100644
--- a/benchmarks/polybench-syn-div/exec.csv
+++ b/benchmarks/polybench-syn-div/exec.csv
@@ -5,3 +5,23 @@ jacobi-1d,19622
 seidel-2d,664780
 jacobi-2d,344072
 nussinov,954402
+floyd-warshall,5373798
+3mm,536114
+2mm,404478
+doitgen,351988
+bicg,53916
+mvt,70204
+atas,58424
+syrk,271816
+gemver,117394
+symm,240172
+gesummv,37700
+gemm,328104
+trmm,144688
+syr2k,436520
+cholesky,2535686
+trisolv,25192
+lu,2853646
+ludcmp,2601382
+durbin,22974
+covariance,288392
diff --git a/ip/altera.v b/ip/altera.v
new file mode 100644
index 0000000..3839cbe
--- /dev/null
+++ b/ip/altera.v
@@ -0,0 +1,2 @@
+module ALTERA_MF_MEMORY_INITIALIZATION;
+endmodule
diff --git a/scripts/docker/Dockerfile b/scripts/docker/Dockerfile
index 9612938..169971c 100644
--- a/scripts/docker/Dockerfile
+++ b/scripts/docker/Dockerfile
@@ -5,9 +5,14 @@ RUN nix-channel --update
 
 RUN nix-env -i yosys git tmux vim gcc iverilog
 
+ADD legup_polybench_syn.tar.gz /data/legup-polybench-syn
+ADD legup_polybench_syn_div.tar.gz /data/legup-polybench-syn-div
+
 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"
+
+RUN echo "export PATH=/vericert/bin:$PATH" >>/root/.bashrc
diff --git a/scripts/docker/artifact.org b/scripts/docker/artifact.org
index d6029f8..5ef1735 100644
--- a/scripts/docker/artifact.org
+++ b/scripts/docker/artifact.org
@@ -45,6 +45,10 @@ If this finishes without errors, it means that Vericert is working correctly.
 
 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.
 
+** Directory structure of Vericert
+
+
+
 ** How to manually compile using Vericert
 
 To compile arbitrary C files, the following command can be used:
@@ -70,8 +74,28 @@ There are two benchmark sets for which the results are given in the paper:
 
 To get the cycle counts for Vericert from the benchmarks
 
+** Getting the cycle counts for LegUp
+
+** Rebuilding the Docker image
+
+The docker image can be completely rebuilt from scratch as well, by using the Dockerfile that is located in the Vericert repository at ~/vericert/scripts/docker/Dockerfile~, which also contains this document.
+
+To rebuild the docker image, one first needs to download the legup results for the benchmarks without divider[fn:4] and with divider[fn:5], and the tar files should be placed in the same directory as the ~Dockerfile~.  Then, in the ~docker~ directory, the following will build the docker image, which might take around 20 minutes:
+
+#+begin_src shell
+docker build .
+#+end_src
+
+Then, using the hash it can be run in the same way as the docker container that was linked to this artifact:
+
+#+begin_src shell
+docker run -it <hash> sh
+#+end_src
+
 * Footnotes
 
+[fn:5] https://imperialcollegelondon.box.com/s/94clcbjowla3987opf3icjz087ozoi1o
+[fn:4] https://imperialcollegelondon.box.com/s/ril1utuk2n88fhoq3375oxiqcgw42b8a
 [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/test/array.c b/test/array.c
index 680acdf..a50cda4 100644
--- a/test/array.c
+++ b/test/array.c
@@ -1,128 +1,9 @@
-/* durbin.c: this file is part of PolyBench/C */
+int main() {
+    int a[10] = {0};
 
-#ifndef SYNTHESIS
-#include <stdio.h>
-#endif
-
-unsigned int divider(unsigned int x, unsigned int y)
-{
-    unsigned int r0, q0, y0, y1;
-
-    r0 = x;
-    q0 = 0;
-    y0 = y;
-    y1 = y;
-    do
-    {
-        y1 = 2 * y1;
-    } while (y1 <= x);
-    do
-    {
-        y1 = y1 / 2;
-        q0 = 2 * q0;
-        if (r0 >= y1)
-        {
-            r0 = r0 - y1;
-            q0 = q0 + 1;
-        }
-    } while ((int)y1 != (int)y0);
-    return q0;
-}
-
-int sdivider(int N, int D) {
-    if (D < 0) {
-        if (N < 0)
-            return divider(-N, -D);
-        else
-            return -divider(N, -D);
-    } else {
-        if (N < 0)
-            return -divider(-N, D);
-        else
-            return divider(N, D);
-    }
-}
-
-#define plus(i) i = i + ONE
-/* Include polybench common header. */
-static
-void init_array (int n,
-                 int r[ 40 + 0])
-{
-    int ONE = 1;
-    int i;
-
-    for (i = 0; i < n; plus(i))
-    {
-        r[i] = (n+ONE-i);
+    for (int i = 1; i < 10; i++) {
+        a[i] = a[i-1] + i;
     }
-}
-
-
-
-static
-int print_array(int n,
-                int y[ 40 + 0])
-
-{
-    int ONE = 1;
-    int i;
-    int res = 0;
-
-    for (i = 0; i < n; plus(i)) {
-        res  ^= y[i];
-    }
-
-#ifndef SYNTHESIS
-    printf("finished: %u\n", res);
-#endif
-
-    return res;
-}
-
-static
-void kernel_durbin(int n,
-                   int r[ 40 + 0],
-                   int y[ 40 + 0])
-{
-    int z[40];
-    int alpha;
-    int beta;
-    int sum;
-
-    int ONE = 1;
-    int i,k;
-    y[0] = -r[0];
-    beta = 1;
-    alpha = -r[0];
-
-    for (k = 1; k < n; plus(k)) {
-        beta = (ONE-alpha*alpha)*beta;
-        sum = 0;
-        for (i=0; i<k; plus(i)) {
-            sum += r[k-i-ONE]*y[i];
-        }
-        alpha = - sdivider(r[k] + sum, beta);
-
-        for (i=0; i<k; plus(i)) {
-            z[i] = y[i] + alpha*y[k-i-ONE];
-        }
-        for (i=0; i<k; plus(i)) {
-            y[i] = z[i];
-        }
-        y[k] = alpha;
-    }
-}
-
-
-int main()
-{
-    int n = 40;
-    int r[40 + 0];
-    int y[40 + 0];
-
-    init_array (n, r);
-    kernel_durbin (n, r, y);
 
-    return print_array(n, y);
+    return a[9];
 }
diff --git a/test/test_all.sh b/test/test_all.sh
index 6b67d27..2d78890 100755
--- a/test/test_all.sh
+++ b/test/test_all.sh
@@ -21,6 +21,7 @@ test_command() {
 
 test_command iverilog
 test_command gcc
+test_command vericert
 
 echo "--------------------------------------------------"
 
@@ -30,13 +31,13 @@ for cfile in $test_dir/*.c; do
     gcc -o $outbase.gcc $cfile >/dev/null 2>&1
     $outbase.gcc
     expected=$?
-    ./bin/vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1
+    vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1
     if [[ ! -f $outbase.v ]]; then
         echo "ERROR"
         continue
     fi
     iverilog -o $outbase.iverilog $outbase.v
-    actual=$($outbase.iverilog | sed -E -e 's/[^0-9]+([0-9]+)/\1/')
+    actual=$($outbase.iverilog | tail -n1 | sed -E -e 's/[^0-9]+([0-9]+)/\1/')
     if [[ $expected = $actual ]]; then
         echo "OK"
     else