diff options
| -rw-r--r-- | algorithm.tex | 2 | ||||
| -rw-r--r-- | conclusion.tex | 2 | ||||
| -rw-r--r-- | references.bib | 24 |
3 files changed, 25 insertions, 3 deletions
diff --git a/algorithm.tex b/algorithm.tex index 2aff9bb..7158fbb 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -133,7 +133,7 @@ endmodule to [out=60,in=130] ($(s2.east) + (0.3,0.7)$) to [out=310,in=10] (s2); \end{tikzpicture} \end{subfigure} - \caption{A simple state machine implemented in Verilog, with its diagrammatic representation on the right, where the x's stand for don't cares and each transition is labelled with the values for the \texttt{rst}, \texttt{y} and output \texttt{z}.}% + \caption{A simple state machine implemented in Verilog, with its diagrammatic representation on the right. The x's stand for don't cares and each transition is labelled with the values of the inputs \texttt{rst} and \texttt{y} and output \texttt{z}.}% \label{fig:tutorial:state_machine} \end{figure} diff --git a/conclusion.tex b/conclusion.tex index 6d98ffc..b7daf71 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -19,7 +19,7 @@ Beyond this, we plan to implement scheduling and loop pipelining, since this all Other optimisations include resource sharing to reduce the circuit area, and using tailored hardware operators that use hard IP blocks on chip and can be pipelined. % this could include multi-cycle operations and pipelining optimisations so that division and multiplication operators also become more efficient. -Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output that \vericert{} provides is a strong one, the semantics for the source and target languages are both well-established, and Coq is a mature and thoroughly tested system. However, \vericert{} cannot guarantee to provide an output for every valid input -- for instance, as remarked in Section~\ref{sec:proof:htl_verilog}, \vericert{} will error out if given a program with more than about four million instructions! -- but our evaluation indicates that it does not seem to error out too frequently. And of course, \vericert{} cannot guarantee that the final hardware produced will be correct, because the Verilog it generates must pass through a series of unverified tools along the way. This concern may be allayed in the future thanks to recent work by~\citet{10.1145/3437992.3439916} to produce a verified logic synthesis tool. +Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output that \vericert{} provides is a strong one, the semantics for the source and target languages are both well-established, and Coq is a mature and thoroughly tested system. However, \vericert{} cannot guarantee to provide an output for every valid input -- for instance, as remarked in Section~\ref{sec:proof:htl_verilog}, \vericert{} will error out if given a program with more than about four million instructions! -- but our evaluation indicates that it does not seem to error out too frequently. And of course, \vericert{} cannot guarantee that the final hardware produced will be correct, because the Verilog it generates must pass through a series of unverified tools along the way. That concern may be allayed in the future thanks to recent work by~\citet{10.1145/3437992.3439916} to produce a verified logic synthesis tool. %%% Local Variables: diff --git a/references.bib b/references.bib index c73c488..0065756 100644 --- a/references.bib +++ b/references.bib @@ -712,7 +712,29 @@ year = {2020}, doi = "10.1007/978-3-642-28869-2_20" } -@article{zhao12_formal_llvm_inter_repres_verif_progr_trans, +@inproceedings{zhao12_formal_llvm_inter_repres_verif_progr_trans, + author = {Jianzhou Zhao and + Santosh Nagarakatte and + Milo M. K. Martin and + Steve Zdancewic}, + editor = {John Field and + Michael Hicks}, + title = {Formalizing the {LLVM} intermediate representation for verified program + transformations}, + booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles + of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania, + USA, January 22-28, 2012}, + pages = {427--440}, + publisher = {{ACM}}, + year = {2012}, + url = {https://doi.org/10.1145/2103656.2103709}, + doi = {10.1145/2103656.2103709}, + timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, + biburl = {https://dblp.org/rec/conf/popl/ZhaoNMZ12.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, Steve}, title = {Formalizing the {LLVM} Intermediate Representation for Verified Program |