diff options
| -rw-r--r-- | algorithm.tex | 5 | ||||
| -rw-r--r-- | evaluation.tex | 7 | ||||
| -rw-r--r-- | introduction.tex | 5 | ||||
| -rw-r--r-- | main.tex | 5 | ||||
| -rw-r--r-- | proof.tex | 5 | ||||
| -rw-r--r-- | related.tex | 5 | ||||
| -rw-r--r-- | verilog.tex | 5 |
7 files changed, 36 insertions, 1 deletions
diff --git a/algorithm.tex b/algorithm.tex index 8488edf..45d3a42 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -68,3 +68,8 @@ RTL is first translated to an intermediate language called hardware transfer lan \end{align*} \subsection{HLS Algorithm} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/evaluation.tex b/evaluation.tex index 9103942..17e2e36 100644 --- a/evaluation.tex +++ b/evaluation.tex @@ -29,4 +29,9 @@ mips & 18482 & 78.43 & 10617 & 7690 & 0 \\\hline \caption{CHstone programs synthesised in CoqUp} \end{table} -The difference in cycle counts shows the degree of parallelism that LegUp's scheduling and memory system can offer. However, their Verilog generation is not guaranteed to be correct. Although the runtime LegUp outputs are tested to be correct for these programs, this does not provide any confidence on the correctness of Verilog generation of any other programs. Our Coq proof mechanisation guarantees that generated Verilog is correct for any input program that uses the subset of CompCert instructions that we have proven to be correct.
\ No newline at end of file +The difference in cycle counts shows the degree of parallelism that LegUp's scheduling and memory system can offer. However, their Verilog generation is not guaranteed to be correct. Although the runtime LegUp outputs are tested to be correct for these programs, this does not provide any confidence on the correctness of Verilog generation of any other programs. Our Coq proof mechanisation guarantees that generated Verilog is correct for any input program that uses the subset of CompCert instructions that we have proven to be correct. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/introduction.tex b/introduction.tex index 5c8bcac..dfd447d 100644 --- a/introduction.tex +++ b/introduction.tex @@ -45,3 +45,8 @@ CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherkl \NR{Is both the translator and verifier written in Coq?} \NR{A tool-flow diagram here will be useful. I thought you had one previously?} \NR{Do you think we have a very simple example of a program where wrong Verilog is generated in VHLS or LegUp, but not in CoqUp?} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: @@ -213,3 +213,8 @@ Text of appendix \ldots \end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: @@ -1,3 +1,8 @@ \section{Proof} \subsection{Coq Mechanisation} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/related.tex b/related.tex index 335aa8d..9deb788 100644 --- a/related.tex +++ b/related.tex @@ -13,3 +13,8 @@ to logical and implementation errors''. They did, however, find two bugs in SPAR \YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool. And yes thank you, will definitely cite that paper. There seem to be similar early proofs of high-level synthesis like \citet{hwang91_formal_approac_to_sched_probl} or \citet{grass94_high}. There are also the Occam papers that I need to mention too, like \citet{page91_compil_occam}, \citet{jifeng93_towar}, \citet{perna11_correc_hardw_synth} and \citet{perna12_mechan_wire_wise_verif_handel_c_synth}.} \JW{Well it's a good job there's no page limit on bibliographies these days then! I'll keep an eye out for more papers we could cite when I get a free moment. (No need to cite \emph{everything} of course.)} \YH{Yes that's true, there are too many to cite! And great thank you, that would help a lot, I have quite a few papers I still want to cite, but have to think about where they will fit in.} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/verilog.tex b/verilog.tex index dca4d65..cf4baa4 100644 --- a/verilog.tex +++ b/verilog.tex @@ -86,3 +86,8 @@ based on what they evaluate to. For case I think that would end up being a three \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}})} \end{equation} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: |