summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-04-11 15:58:09 +0100
committerYann Herklotz <git@yannherklotz.com>2021-04-11 16:55:51 +0100
commitf1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a (patch)
tree096bb355bcbb3b465bd531cc793f7391e2c49d83
parent9c107a5bd8330ca9b5b6bdadf715b2a48dda1489 (diff)
downloadoopsla21_fvhls-f1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a.tar.gz
oopsla21_fvhls-f1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a.zip
Add new results
-rw-r--r--evaluation.tex14
-rw-r--r--main.tex1
-rw-r--r--proof.tex2
-rw-r--r--results/benchmark_results/legup_no_chain.csv27
-rw-r--r--results/benchmark_results/legup_no_opt.csv27
-rw-r--r--results/benchmark_results/legup_no_opt_no_chain.csv27
-rw-r--r--results/benchmark_results/legup_opt.csv27
-rw-r--r--results/benchmark_results/vericert.csv27
-rw-r--r--reviews/pldi.org2
-rw-r--r--verilog.tex2
10 files changed, 153 insertions, 3 deletions
diff --git a/evaluation.tex b/evaluation.tex
index 1e02c84..2e08031 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -26,6 +26,20 @@ We configured Polybench's parameters so that only integer types are used, since
\subsection{RQ1: How fast is \vericert{}-generated hardware?}
\begin{figure}\centering
+ \begin{tikzpicture}
+ \begin{axis}[
+ visualization depends on={value \thisrow{Name} \as \labela},
+ width=1\textwidth,
+ height=0.5\textwidth,
+ ]
+
+ \addplot[] table [x=benchmark,y=cycles,col sep=comma] {results/benchmark_results/vericert.csv};
+
+ \end{axis}
+ \end{tikzpicture}
+\end{figure}
+
+\begin{figure}\centering
\begin{subfigure}[t]{0.48\textwidth}
\definecolor{cyclecountcol}{HTML}{1b9e77}
\begin{tikzpicture}
diff --git a/main.tex b/main.tex
index 97f74a8..672c6a7 100644
--- a/main.tex
+++ b/main.tex
@@ -40,6 +40,7 @@
\usepackage{booktabs}
\usepackage{mathpartir}
\usepackage{pgfplots}
+\usepackage{pgfplotstable}
\usepackage{soul}
\usepackage{subcaption}
\usepackage{tikz}
diff --git a/proof.tex b/proof.tex
index fe76db8..058969a 100644
--- a/proof.tex
+++ b/proof.tex
@@ -63,7 +63,7 @@ In the following lemma, $\yhfunction{spec\_htl}$ is the top-level specification
\subsubsection{From Specification to Simulation}
-To prove that the specification predicate implies the desired forward simulation, we must first define a relation that matches each 3AC state to an equivalent HTL state. This relation also captures the assumptions made about the 3AC code that we receive from \compcert{}.% so that these assumptions can be used to prove the translations correct.
+To prove that the specification predicate implies the desired forward simulation, we must first define a relation that matches each 3AC state to an equivalent HTL state. This relation also captures the assumptions made about the 3AC code that we receive from \compcert{}. % so that these assumptions can be used to prove the translations correct.
These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm. Some of the assumptions that need to be made about the 3AC and HTL code for a pair of states to match are:
\begin{itemize}
diff --git a/results/benchmark_results/legup_no_chain.csv b/results/benchmark_results/legup_no_chain.csv
new file mode 100644
index 0000000..a03e95d
--- /dev/null
+++ b/results/benchmark_results/legup_no_chain.csv
@@ -0,0 +1,27 @@
+benchmark,lut_flip_flop,slice,regs,luts,ramfifo,iopin,dsps,power,delay,cycles
+2mm,0,2294,5426,3784,10,0,18,0.164,9.62,169531
+3mm,8,2558,5711,4373,14,0,21,0.169,9.309,235768
+atas,0,500,1657,1145,8,0,9,0.135,8.623,58278
+bicg,9,834,2566,1737,12,0,9,0.144,8.496,79651
+cholesky,5,1536,4261,2950,8,0,27,0.163,9.413,830753
+covariance,9,1289,3040,2729,6,0,6,0.164,8.814,212548
+doitgen,8,1632,4472,3038,6,0,42,0.200,9.26,46852
+durbin,3,775,2623,1687,6,0,12,0.144,9.13,22640
+fdtd-2d,4,1700,4660,3963,8,0,3,0.174,9.35,431694
+floyd-warshall,5,649,1832,1510,8,0,3,0.132,7.067,2611426
+gemm,1,2044,4693,3260,6,0,12,0.159,8.891,223526
+gemver,7,796,2274,1770,20,0,15,0.164,9.643,109309
+gesummv,5,728,2363,1677,8,0,9,0.145,8.987,68572
+heat-3d,5,1559,4468,3530,4,0,0,0.159,9.808,80759
+jacobi-1d,8,297,1094,548,4,0,0,0.126,6.9399999999999995,11744
+jacobi-2d,4,1378,3598,3081,4,0,3,0.161,8.32,171633
+lu,2,1543,4267,3042,8,0,24,0.155,9.937,941544
+ludcmp,0,2199,6116,4647,14,0,48,0.218,9.857,903989
+mvt,5,1056,3420,2211,12,0,9,0.152,9.133,88668
+nussinov,5,699,2193,1635,10,0,3,0.133,9.474,464517
+seidel-2d,5,1128,3086,2272,4,0,3,0.156,7.714,544769
+symm,5,1104,3490,2448,6,0,12,0.155,8.793,101653
+syr2k,9,966,2818,1991,6,0,12,0.149,9.161,206241
+syrk,6,730,2288,1610,4,0,9,0.141,8.394,162572
+trisolv,8,976,2296,1895,8,0,9,0.157,9.041,46834
+trmm,4,766,2319,1835,4,0,3,0.133,8.822,85592
diff --git a/results/benchmark_results/legup_no_opt.csv b/results/benchmark_results/legup_no_opt.csv
new file mode 100644
index 0000000..8646cfe
--- /dev/null
+++ b/results/benchmark_results/legup_no_opt.csv
@@ -0,0 +1,27 @@
+benchmark,lut_flip_flop,slice,regs,luts,ramfifo,iopin,dsps,power,delay,cycles
+2mm,0,1133,2446,3076,10,0,18,0.183,9.948,113132
+3mm,6,1267,2649,3594,14,0,15,0.189,10.457,166838
+atas,0,991,2051,2209,8,0,6,0.175,9.972,38012
+bicg,2,692,1707,1870,12,0,9,0.157,8.723,45163
+cholesky,5,1159,2618,3080,8,0,21,0.177,9.803,500738
+covariance,7,1210,2212,2788,6,0,6,0.175,9.949,153732
+doitgen,6,690,1569,1934,6,0,9,0.155,9.966,98749
+durbin,8,714,2163,1640,6,0,12,0.147,9.12,15111
+fdtd-2d,4,1551,3031,3662,8,0,3,0.194,11.429,266014
+floyd-warshall,2,516,1408,1487,8,0,3,0.132,9.819,1512364
+gemm,2,825,1779,2310,6,0,12,0.152,9.711,131836
+gemver,4,740,1418,1904,20,0,15,0.204,9.65,68642
+gesummv,3,627,1542,1699,8,0,9,0.162,10.885,37479
+heat-3d,4,907,1793,2676,4,0,0,0.143,12.922,51757
+jacobi-1d,2,823,1656,1520,4,0,0,0.158,7.138,8077
+jacobi-2d,0,1211,2361,2828,4,0,3,0.167,11.157,94138
+lu,8,1139,2504,3148,8,0,15,0.157,10.07,566955
+ludcmp,3,1695,3486,4826,14,0,30,0.226,11.046,553755
+mvt,2,898,2244,2346,12,0,9,0.164,9.335,56928
+nussinov,5,617,1560,1630,10,0,3,0.138,11.23,265980
+seidel-2d,2,981,2023,2222,4,0,3,0.156,8.994,337110
+symm,1,851,2144,2406,6,0,9,0.159,9.838,66181
+syr2k,0,812,1793,2153,6,0,12,0.159,9.967,121098
+syrk,9,649,1444,1772,4,0,9,0.142,9.589,102946
+trisolv,6,914,1779,1922,8,0,9,0.173,9.192,36030
+trmm,4,600,1507,1726,4,0,3,0.136,9.536,56439
diff --git a/results/benchmark_results/legup_no_opt_no_chain.csv b/results/benchmark_results/legup_no_opt_no_chain.csv
new file mode 100644
index 0000000..fa78dc3
--- /dev/null
+++ b/results/benchmark_results/legup_no_opt_no_chain.csv
@@ -0,0 +1,27 @@
+benchmark,lut_flip_flop,slice,regs,luts,ramfifo,iopin,dsps,power,delay,cycles
+2mm,2,1161,3069,3132,10,0,18,0.160,9.345,240573
+3mm,5,1380,3333,3701,14,0,21,0.163,9.265,342207
+atas,4,1040,2415,2238,8,0,6,0.159,7.715,77210
+bicg,5,717,2161,1836,12,0,9,0.145,9.131,99667
+cholesky,1,1190,3591,3065,8,0,24,0.158,9.679,1000414
+covariance,2,1213,2695,2819,6,0,6,0.166,9.37,283863
+doitgen,0,734,1885,1997,6,0,9,0.145,8.881,198592
+durbin,6,889,2561,1670,6,0,12,0.145,9.277,27840
+fdtd-2d,3,1627,4146,3855,8,0,3,0.173,9.657,507806
+floyd-warshall,4,573,1645,1541,8,0,3,0.132,7.609,3121798
+gemm,1,851,2294,2215,6,0,12,0.145,8.756,274546
+gemver,9,714,2037,1883,20,0,15,0.161,9.724,141440
+gesummv,1,673,2014,1641,8,0,9,0.143,9.392,87649
+heat-3d,4,988,2792,2811,4,0,0,0.132,9.514,103513
+jacobi-1d,8,921,2272,1573,4,0,0,0.150,7.109999999999999,15163
+jacobi-2d,8,1322,3285,2940,4,0,3,0.160,9.148,157584
+lu,9,1214,3541,3233,8,0,21,0.155,9.676,1132106
+ludcmp,8,1900,4876,4832,14,0,42,0.191,9.542,1098988
+mvt,3,913,2825,2169,12,0,9,0.147,9.856,118444
+nussinov,8,746,2195,1838,10,0,3,0.133,9.787,559131
+seidel-2d,6,1026,2657,2300,4,0,3,0.151,7.9990000000000006,658070
+symm,6,905,2857,2350,6,0,9,0.149,9.606,130249
+syr2k,2,901,2449,2207,6,0,12,0.152,9.007,255334
+syrk,2,711,1906,1786,4,0,9,0.138,8.321,206415
+trisolv,1,982,2130,1918,8,0,9,0.159,8.52,44772
+trmm,5,652,1880,1767,4,0,3,0.133,8.509,107174
diff --git a/results/benchmark_results/legup_opt.csv b/results/benchmark_results/legup_opt.csv
new file mode 100644
index 0000000..79f48e6
--- /dev/null
+++ b/results/benchmark_results/legup_opt.csv
@@ -0,0 +1,27 @@
+benchmark,lut_flip_flop,slice,regs,luts,ramfifo,iopin,dsps,power,delay,cycles
+2mm,8,1493,3222,3389,10,0,18,0.192,10.776,73932
+3mm,2,1874,3547,4088,14,0,15,0.207,11.123,109367
+atas,3,496,1132,1172,8,0,6,0.143,9.994,27546
+bicg,2,823,1864,1703,12,0,9,0.166,10.054,28751
+cholesky,5,1275,3081,3133,8,0,27,0.178,9.887,416569
+covariance,8,1321,2409,2927,6,0,6,0.181,10.345,110648
+doitgen,4,1358,2867,2629,6,0,42,0.223,11.224,21207
+durbin,8,732,2231,1749,6,0,12,0.151,9.077,12531
+fdtd-2d,3,1686,3143,3965,8,0,3,0.197,12.868,214433
+floyd-warshall,7,561,1284,1538,8,0,3,0.133,10.104,1221958
+gemm,1,1283,2669,2693,6,0,12,0.157,10.058,100926
+gemver,1,693,1455,1706,20,0,15,0.204,9.774,43083
+gesummv,6,675,1706,1668,8,0,9,0.161,11.074,23988
+heat-3d,4,1278,2667,3102,4,0,0,0.162,13.314,41059
+jacobi-1d,5,288,777,558,4,0,0,0.138,7.96,5894
+jacobi-2d,4,1356,2580,3064,4,0,3,0.169,10.99,111877
+lu,4,1257,3055,3147,8,0,21,0.166,10.507,471964
+ludcmp,5,1902,4443,4477,14,0,39,0.233,10.603,455393
+mvt,0,899,2538,2072,12,0,6,0.162,9.656,34082
+nussinov,5,657,1517,1675,10,0,3,0.145,11.265,216632
+seidel-2d,8,1215,2466,2327,4,0,3,0.166,9.723,240970
+symm,9,957,2349,2518,6,0,12,0.171,12.449,49023
+syr2k,7,902,1885,2161,6,0,12,0.163,10.633,86683
+syrk,3,670,1555,1711,4,0,9,0.147,10.101,71981
+trisolv,3,979,1906,1883,8,0,9,0.170,9.67,35798
+trmm,3,703,1767,1880,4,0,3,0.142,10.363,45382
diff --git a/results/benchmark_results/vericert.csv b/results/benchmark_results/vericert.csv
new file mode 100644
index 0000000..a02d2a3
--- /dev/null
+++ b/results/benchmark_results/vericert.csv
@@ -0,0 +1,27 @@
+benchmark,lut_flip_flop,slice,regs,luts,ramfifo,iopin,dsps,power,delay,cycles
+2mm,2,1764,4952,3541,4,0,24,0.152,4.59,467612
+3mm,9,1940,5046,3834,8,0,21,0.156,4.56,604582
+atas,8,599,1603,1254,4,0,6,0.128,4.539,101618
+bicg,0,930,2628,2012,4,0,9,0.138,4.692,130790
+cholesky,0,1898,5322,3192,8,0,12,0.141,4.877,2575070
+covariance,5,557,1705,1157,4,0,6,0.135,4.271,340794
+doitgen,1,1167,3365,2038,4,0,6,0.136,4.305,386782
+durbin,4,737,2215,1666,1,0,12,0.139,9.702,23832
+fdtd-2d,8,1517,3984,2682,4,0,9,0.142,4.467,958412
+floyd-warshall,8,894,2897,2311,8,0,3,0.140,4.473,5414366
+gemm,9,1110,3169,2474,4,0,18,0.149,4.609,406774
+gemver,6,1121,3116,2046,4,0,21,0.141,4.684,193048
+gesummv,5,991,3017,2174,4,0,15,0.142,4.719,116556
+heat-3d,5,1458,4929,3282,4,0,3,0.132,4.734,592770
+jacobi-1d,5,454,1345,699,1,0,0,0.128,4.248,19996
+jacobi-2d,3,891,2669,2053,4,0,6,0.139,4.378,397200
+lu,6,1755,5039,3049,8,0,9,0.136,4.817,2893146
+ludcmp,6,2584,6796,4299,8,0,15,0.138,4.695,2641694
+mvt,6,1704,4209,2798,4,0,9,0.147,4.686,148874
+nussinov,0,981,2680,2361,8,0,0,0.127,4.467,956490
+seidel-2d,5,728,2544,1439,4,0,3,0.129,4.386,942338
+symm,7,1562,3981,3070,4,0,21,0.147,4.608,279832
+syr2k,1,1369,3804,2548,8,0,18,0.145,4.543,525908
+syrk,0,899,2772,1930,4,0,12,0.134,4.502,338286
+trisolv,1,474,1481,778,4,0,3,0.127,4.541,36050
+trmm,1,889,2729,2007,2,0,6,0.130,4.384,165828
diff --git a/reviews/pldi.org b/reviews/pldi.org
index 2f14d3e..5522a4a 100644
--- a/reviews/pldi.org
+++ b/reviews/pldi.org
@@ -25,7 +25,7 @@ topics"
:PROPERTIES:
:CUSTOM_ID: paper-summary
:END:
-"High-level synthesis" (HSL) is a term of art for compiling C programs
+"High-level synthesis" (HLS) is a term of art for compiling C programs
to hardware designs. This paper presents the first mechanized proof of
soundness for an HLS compiler. The implementation and proof are carried
out in Coq and build on CompCert, targeting Verilog. Evaluation shows
diff --git a/verilog.tex b/verilog.tex
index c9eff1c..d0dd74c 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -57,7 +57,7 @@ which modifies one array element using blocking assignment and then a second usi
\paragraph{Removing support for external inputs to modules} Support for receiving external inputs was removed from the semantics for simplicity, as these are not needed for an HLS target. The main module in Verilog models the main function in C, and since the inputs to a C function shouldn't change during its execution, there is no need for external inputs for Verilog modules.
-\paragraph{Simplifying representation of bitvectors} Finally, we use 32-bit integers to represent bitvectors rather of arrays of Booleans. This is because \vericert{} (currently) only supports types represented by 32 bits.
+\paragraph{Simplifying representation of bitvectors} Finally, we use 32-bit integers to represent bitvectors rather than arrays of Booleans. This is because \vericert{} (currently) only supports types represented by 32 bits.
\subsection{Integrating the Verilog Semantics into \compcert{}'s Model}
\label{sec:verilog:integrating}