diff options
| -rw-r--r-- | main.tex | 9 | ||||
| -rw-r--r-- | references.bib | 61 |
2 files changed, 68 insertions, 2 deletions
@@ -190,9 +190,12 @@ %% environment and commands, and keywords command. \maketitle - \section{Introduction} +The current approach to writing energy-efficient and high-throughput applications is to use custom hardware which has been specialised for that application, instead of relying on and optimising for a CPU.\@ This comes at the cost of having to design the customised hardware, which, if using hardware description languages such as Verilog can be tedious and quite error prone. Especially with the size growing over the years, it can become difficult to verify that the hardware design behaves in the expected way, as simulation of hardware description languages can be quite inefficient. Furthermore, the algorithms that are being accelerated in hardware often already have a software implemention, meaning they have to be reimplemented efficiently in a hardware description language which can be time consuming. + + + \section{Background} \subsection{Verilog} @@ -277,11 +280,13 @@ based on what they evaluate to. For case I think that would end up being a three \begin{equation} \label{eq:9} - \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) = (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})} + \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})} \end{equation} \section{Proof} +\section{Coq mechanisation} + \section{Conclusion} %% Acknowledgments diff --git a/references.bib b/references.bib index dc73c13..914d673 100644 --- a/references.bib +++ b/references.bib @@ -14,3 +14,64 @@ numpages = 9, publisher = {ACM}, } + +@inproceedings{lidbury15_many_core_compil_fuzzin, + author = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson, + Alastair F.}, + title = {Many-Core Compiler Fuzzing}, + booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design + and Implementation}, + year = 2015, + pages = {65-76}, + doi = {10.1145/2737924.2737986}, + address = {New York, NY, USA}, + isbn = 9781450334686, + location = {Portland, OR, USA}, + numpages = 12, + publisher = {Association for Computing Machinery}, + series = {PLDI '15}, +} + +@article{takach16_high_level_synth, + author = {A. {Takach}}, + title = {High-Level Synthesis: Status, Trends, and Future + Directions}, + journal = {IEEE Design Test}, + volume = {33}, + number = {3}, + pages = {116-124}, + year = {2016}, + doi = {10.1109/MDAT.2016.2544850}, + url = {https://doi.org/10.1109/MDAT.2016.2544850}, + ISSN = {2168-2364}, + month = {June}, +} + +@inproceedings{liu16_effic_high_level_synth_desig, + author = { {Dong Liu} and B. C. {Schafer}}, + title = {Efficient and reliable High-Level Synthesis Design Space + Explorer for FPGAs}, + booktitle = {2016 26th International Conference on Field Programmable + Logic and Applications (FPL)}, + year = 2016, + pages = {1-8}, + doi = {10.1109/FPL.2016.7577370}, + ISSN = {1946-1488}, + month = {Aug}, +} + +@article{lahti19_are_we_there_yet, + author = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and + T. D. {H{\"a}m{\"a}l{\"a}inen}}, + title = {Are We There Yet? a Study on the State of High-Level + Synthesis}, + journal = {IEEE Transactions on Computer-Aided Design of Integrated + Circuits and Systems}, + volume = {38}, + number = {5}, + pages = {898-911}, + year = {2019}, + doi = {10.1109/TCAD.2018.2834439}, + ISSN = {1937-4151}, + month = {May}, +} |