diff options
| -rw-r--r-- | algorithm.tex | 33 | ||||
| -rw-r--r-- | introduction.tex | 2 | ||||
| -rw-r--r-- | main.tex | 2 | ||||
| -rw-r--r-- | verilog.tex | 16 |
4 files changed, 25 insertions, 28 deletions
diff --git a/algorithm.tex b/algorithm.tex index c275a03..e43e804 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -52,24 +52,21 @@ int main() { \begin{subfigure}[b]{0.6\linewidth} \begin{minted}[fontsize=\footnotesize]{c} main() { - 19: x9 = 1 - 18: int32[stack(0)] = x9 - 17: x8 = 2 - 16: int32[stack(4)] = x8 - 15: x7 = 3 - 14: int32[stack(8)] = x7 - 13: x3 = 0 - 12: x2 = 1 - 11: x1 = 0 - 10: nop - 9: if (x1 <s 3) goto 8 else goto 3 - 8: x6 = stack(0) (int) - 7: x5 = int32[x6 + x1 * 4 + 0] - 6: x3 = x3 + x5 + 0 (int) - 5: x1 = x1 + x2 + 0 (int) - 4: goto 9 - 3: x4 = x3 goto 1 - 2: x4 = 0 + 16: x9 = 1 + 15: int32[stack(0)] = x9 + 14: x8 = 2 + 13: int32[stack(4)] = x8 + 12: x7 = 3 + 11: int32[stack(8)] = x7 + 10: x3 = 0 + 9: nop + 8: x1 = 0 + 7: x6 = stack(0) (int) + 6: x5 = int32[x6 + x1 * 4 + 0] + 5: x3 = x3 + x5 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x4 = x3 1: return x4 } \end{minted} diff --git a/introduction.tex b/introduction.tex index c72f788..2ac9eba 100644 --- a/introduction.tex +++ b/introduction.tex @@ -18,7 +18,7 @@ However, the fact that the behaviour is preserved after HLS cannot be guaranteed %% Current work in formal verification of HLS %%\NR{This is a good paragraph, but we need to relate it more to this work and why this work is different.} %%\NR{Focus on more high-level of "why this work is interesting"? Two key points we want to get across to the reader is that in existing works: validation is neccessary every time a new program is compiled and the verifying algorithm is not verified.} -%%\NR{Also define words like validation, verifying algorithm (can you use the word ``verifier'',mechanisation} +%%\NR{Also define words like validation, verifying algorithm (can you use the word ``verifier'',mechanisation)} %%\NR{Having said that, keep the text for related work section.}\YH{Added into related works.} To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness. This can either be done by simulation with a large test bench, however, to be sure that the hardware does indeed behave in the same way as the C code, it may be necessary to prove that they are equivalent. \JW{I think that point could be strengthened by emphasising that simulation with a test-bench only provides guarantees that are as good as the test-bench! That is, if the test-bench does not cover all possible inputs then bugs may remain.} Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and has been successfully applied to many HLS optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}. However, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof. In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially. \JW{Does this link back to Mentor's Catapult-C, which you mentioned earlier? Does Catapult-C attempt to do translation validation as part of its HLS process? And if so, can you make the point that this effort is largely ineffective because once the design is a reasonable size, the translation validation usually fails anyway?} A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code. In addition to that, it would allow for the implementation of translation validated optimisation passes which are also proven correct mechanically, thereby greatly improving the reliability of these passes. @@ -74,7 +74,7 @@ \begin{document} %% Title information -\title[Formally Verified HLS]{Formally Verified High-Level Synthesis} %% [Short Title] is optional; +\title[Formally Verified HLS]{Formally Verified High-Level Synthesis} %% when present, will be used in %% header instead of Full Title. %\titlenote{with title note} %% \titlenote is optional; diff --git a/verilog.tex b/verilog.tex index 67f2f4e..f40baf5 100644 --- a/verilog.tex +++ b/verilog.tex @@ -2,20 +2,20 @@ Verilog is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into more basic logic which describes how different gates connect to each other, called a netlist. This representation can then be put onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASPIC) to implement the design that was described in Verilog. The Verilog standard is quite large though, and not all Verilog features are needed to be able to describe hardware. Many Verilog features are only useful for simulation and do not affect the actual hardware itself, which means that these features do not have to be modelled in the semantics. In addition to that, as the HLS algorithm dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed. Only supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated. -The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which were used to create a formal translation from HOL logic into a Verilog circuit. These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. The main syntax for the Verilog subset is the following: \JW{This verilog syntax looks weird to me. I didn't think there was a `then' keyword, for instance. Perhaps you're aiming more at some sort of abstracted syntax of Verilog? What does the semicolon on its own mean? Some sort of skip statement? The case statement looks weird too -- how do you get multiple cases in a single switch statement, and where is the default case? }\YH{I think I have fixed most cases, yes the single semicolon is a skip statement, should I make that more obvious by naming it? } \JW{It still looks a bit funny to me -- a bit of a halfway-house between `proper' Verilog syntax and `abstract' Verilog syntax. E.g. the way `begin...end' blocks contain exactly two statements, or the way that you get an erroneous double semicolon by combining the `begin...end' rule with the `e=e;' rule. People who are very familiar with C-like syntax will know that this isn't quite right... but then again, it doesn't really matter whether you handle the full syntax, because you only have to pretty-print a subset of it. So, why not stick here with a slightly abstracted Verilog syntax? It would make the operational semantics easier to read, for instance. Basically like you had it before, but explicitly labelled as a simplified syntax, so readers don't get confused!} +The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which were used to create a formal translation from HOL logic into a Verilog circuit. These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. The main syntax for the Verilog subset is the following: \JW{This verilog syntax looks weird to me. I didn't think there was a `then' keyword, for instance. Perhaps you're aiming more at some sort of abstracted syntax of Verilog? What does the semicolon on its own mean? Some sort of skip statement? The case statement looks weird too -- how do you get multiple cases in a single switch statement, and where is the default case? }\YH{I think I have fixed most cases, yes the single semicolon is a skip statement, should I make that more obvious by naming it? } \JW{It still looks a bit funny to me -- a bit of a halfway-house between `proper' Verilog syntax and `abstract' Verilog syntax. E.g. the way `begin...end' blocks contain exactly two statements, or the way that you get an erroneous double semicolon by combining the `begin...end' rule with the `e=e;' rule. People who are very familiar with C-like syntax will know that this isn't quite right... but then again, it doesn't really matter whether you handle the full syntax, because you only have to pretty-print a subset of it. So, why not stick here with a slightly abstracted Verilog syntax? It would make the operational semantics easier to read, for instance. Basically like you had it before, but explicitly labelled as a simplified syntax, so readers don't get confused!}\YH{Yeah, the syntax is a bit funny, mostly because this is actually how it is also encoded in Coq. The main weird rule is the Seq rule, basically because it actually doesn't have a semicolon in between and no begin and end block, but it looks a bit strange to just put two $s$ next to each other. We therefore don't really have begin and end blocks, and basically glue them to each statement instead, so in our semantics, the if statement actually looks like: if $e$ begin $s$ end else begin $s$ end, but it gets very verbose for case statements. I got rid of the sequence for now, so maybe this is better, but this is nearly exactly how we actually encode it.} \begin{align*} v\quad ::=&\; \mathit{sz} \yhkeyword{'d} n\\ \textit{op}\quad ::=&\; \yhkeyword{+ } | \yhkeywordsp{- } | \yhkeywordsp{* } \cdots \\ e\quad ::=&\; v\;\; |\;\; x\;\; |\;\; e \yhkeyword{[} e \yhkeyword{]}\;\; |\;\; e\ \mathit{op}\ e\;\; |\;\; \yhkeyword{!} e\;\; |\;\; \yhkeyword{\textasciitilde} e\;\; |\;\; e \yhkeywordsp{? } e \yhkeywordsp{: } e\\ - s\quad ::=&\; \yhkeyword{begin } s \yhkeyword{; } s \yhkeywordsp{end } |\ \epsilon\\[-2pt] + s\quad ::=&\; s s |\ \epsilon\\[-2pt] |&\; \yhkeyword{if } e\ s \yhkeywordsp{else } s\\[-2pt] |&\; \yhkeyword{case (} e \yhkeyword{) } e : s\ \{\ e : s\ \}\ [\ \yhkeyword{default} : \textit{def}\ ] \yhkeywordsp{endcase}\\[-2pt] |&\; e = e \yhkeyword{;}\\[-2pt] |&\; e \Leftarrow e \yhkeyword{;}\\ d\quad ::=&\; \yhkeyword{[n-1:0] } r\ |\ \yhkeyword{[n-1:0] } r \yhkeywordsp{[m-1:0]}\\ m\quad ::=&\; \yhkeyword{reg } d \yhkeyword{;}\ |\ \yhkeyword{input wire } d \yhkeyword{;}\ |\ \yhkeyword{output reg } d \yhkeyword{;}\\ -|&\; \yhkeywordsp{always @(posedge clk) begin } s \yhkeywordsp{end}\\ +|&\; \yhkeywordsp{always @(posedge clk) } s \\ m \text{ list}\quad ::=&\; \{ m \} \end{align*} @@ -49,17 +49,17 @@ The two main evaluation functions are then \textit{erun}, which takes in the cur % \inferrule[CondTrue]{\textit{erun}\ \Gamma_{0}\ c\ v_{c} \\ \yhfunction{valToB}\ v_{c} = \yhconstant{true} \\ \textit{srun}\ \sigma_{0}\ \textit{st}\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{if } c\ \textit{st} \yhkeywordsp{else } \textit{sf})\ \sigma_{1}}\\ % - \inferrule[CondFalse]{\textit{erun}\ \Gamma_{0}\ c\ v_{c} \\ \yhfunction{valToB}\ v_{c} = \yhconstant{false} \\ \textit{srun}\ \sigma_{0}\ \textit{sf}\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{if } c\ \textit{st} \yhkeywordsp{else } \textit{sf})\ \sigma_{1}}\\ + \inferrule[CondFalse]{\textit{erun}\ \Gamma_{0}\ c\ v_{\rm c} \\ \yhfunction{valToB}\ v_{\rm c} = \yhconstant{false} \\ \textit{srun}\ \sigma_{0}\ \textit{sf}\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{if } c\ \textit{st} \yhkeywordsp{else } \textit{sf})\ \sigma_{1}}\\ % - \inferrule[CaseNoMatch]{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case}\ e\ cs\ \textit{def})\ \sigma_{1} \\ \textit{erun}\ \Gamma_{0}\ me\ mve \\ \textit{erun}\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case (} e \yhkeyword{) } (me : sc) :: cs) \yhkeywordsp{default} : \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\ + \inferrule[CaseNoMatch]{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case}\ e\ cs\ \textit{def})\ \sigma_{1} \\ \textit{erun}\ \Gamma_{0}\ me\ mve \\ \textit{erun}\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case (} e \yhkeyword{) } ((me : sc) :: cs) \yhkeywordsp{default} : \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\ % - \inferrule[CaseMatch]{\textit{srun}\ \sigma_{0}\ sc\ \sigma_{1} \\ \textit{erun}\ \Gamma_{0}\ e\ ve \\ \textit{erun}\ \Gamma_{0}\ me\ mve \\ mve = ve}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case (} e \yhkeyword{) } (me : sc) :: cs) \yhkeywordsp{default} : \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\ + \inferrule[CaseMatch]{\textit{srun}\ \sigma_{0}\ sc\ \sigma_{1} \\ \textit{erun}\ \Gamma_{0}\ e\ ve \\ \textit{erun}\ \Gamma_{0}\ me\ mve \\ mve = ve}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case (} e \yhkeyword{) } ((me : sc) :: cs) \yhkeywordsp{default} : \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\ % \inferrule[CaseDefault]{\textit{srun}\ \sigma_{0}\ s\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case (} e \yhkeyword{) } [] \yhkeywordsp{default} : (\yhkeyword{Some}\ s) \yhkeywordsp{endcase})\ \sigma_{1}}\\ % - \inferrule[Blocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\ \Gamma_{r}\ \Gamma_{a}\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\ (\Gamma_{r},\Gamma_{a},\Delta_{r},\Delta_{a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{r} [n \mapsto v_{\textit{rhs}}], \Gamma_{a}, \Delta_{r}, \Delta_{a})}\\ + \inferrule[Blocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\ \Gamma_{\rm r}\ \Gamma_{\rm a}\ \textit{rhs}\ v_{\rm rhs}}{\textit{srun}\ (\Gamma_{\rm r},\Gamma_{\rm a},\Delta_{\rm r},\Delta_{\rm a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{\rm r} [n \mapsto v_{\rm rhs}], \Gamma_{\rm a}, \Delta_{\rm r}, \Delta_{\rm a})}\\ % - \inferrule[Nonblocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\ (\Gamma_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{r}, \Gamma_{a}, \Delta_{r} [n \mapsto v_{\textit{rhs}}], \Delta_{a})} + \inferrule[Nonblocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\ (\Gamma_{\rm r}, \Gamma_{\rm a}, \Delta_{\rm r}, \Delta_{a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{\rm r}, \Gamma_{\rm a}, \Delta_{\rm r} [n \mapsto v_{\rm rhs}], \Delta_{\rm a})} % % \inferrule[Blocking Array]{\yhkeyword{name}\ \textit{lhs} = \yhkeyword{OK}\ n \\ \textit{erun}\ \Gamma_{r}\ \Gamma_{a}\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\ (\Gamma_{r},\Gamma_{a},\Delta_{r},\Delta_{a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Gamma_{a}, \Delta_{r}, \Delta_{a})}\\ % |