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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
#+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 by using the following inside of the ~/vericert~ directory:
#+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.
** Directory structure of Vericert
** 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:
- ~/vericert/benchmarks
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
|
