diff options
| -rw-r--r-- | algorithm.tex | 2 | ||||
| -rw-r--r-- | proof.tex | 37 | ||||
| -rw-r--r-- | verilog.tex | 8 |
3 files changed, 19 insertions, 28 deletions
diff --git a/algorithm.tex b/algorithm.tex index d52a647..e43d65d 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -10,7 +10,7 @@ This section covers the main architecture of the HLS tool, and the way in which First of all, the choice of C for the input language of \vericert{} is because it is the most widely supported language for HLS, and most major HLS tools also use it as an input. As a lot of existing code is also written in C for HLS, supporting C as an input language compared to a custom domain-specific language means that \vericert{} is more practical. \JW{Can we mention one or two alternatives that we considered?} \paragraph{Choice of target language} -Next, Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language, which can be synthesised into logic gates which can be placed onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC). Verilog was chosen as the output language for \vericert{} because it is one of the most popular hardware description languages and there already exist a few formal semantics for it that could be used as a target~\cite{loow19_verif_compil_verif_proces,meredith10_veril}. \JW{Can we mention one or two alternatives that we considered? Bluespec or Chisel or one of Adam Chlipala's languages, perhaps?} +Next, Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language, which can be synthesised into logic gates which can be either placed onto a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC). Verilog was chosen as the output language for \vericert{} because it is one of the most popular hardware description languages and there already exist a few formal semantics for it that could be used as a target~\cite{loow19_verif_compil_verif_proces,meredith10_veril}. \JW{Can we mention one or two alternatives that we considered? Bluespec or Chisel or one of Adam Chlipala's languages, perhaps?} \paragraph{Choice of implementation language} The framework that was chosen for the frontend was \compcert{}, as it is a mature framework for simulation proofs about intermediate languages, in addition to already providing a validated parser~\cite{jourdan12_valid_lr_parser} from C into the internal representation of Clight. Other frameworks were also considered, such as Vellvm~\cite{zhao12_formal_llvm_inter_repres_verif_progr_trans}, as LLVM IR in particular is often used by HLS tools anyways, however, these would require more work to support a higher level language such as C as input, or even providing a parser for LLVM IR.\@ @@ -2,20 +2,29 @@ This section describes the main correctness theorem that was proven and the main ideas behind the proofs. -The main correctness theorem states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has correct observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$. The following theorem describes this property. +The main correctness theorem states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has correct observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$. The following backwards simulation theorem describes this property. \begin{equation*} - \forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land C \Downarrow B \implies V \Downarrow_{s} B. + \forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B. \end{equation*} -However, this forward simulation might still allow for wrong behaviour of the target code in cases where there are multiple possible behaviours in the target language. This means that there may be cases where it executes correctly, however, there may also be other behaviours that are also valid. However, if the target language is deterministic, meaning there is only one possible behaviour for all possible states, then this implies that the backwards simulation also holds. +To prove this top-level theorem, a forward simulation has to be done between each intermediate language, which implies that the forward simulation between the C and Verilog also holds. To then prove the backward simulation, it suffices to show that the Verilog semantics are deterministic, which implies that there is only one possible behaviour for the Verilog output, and that it therefore also has to imply that $C$ has the same behaviour. + +\subsection{Model} + +%\JW{I think some of the following material belongs in a later section. In the current section, I think we should aim at the casual reader who is interested in understanding things like the overall structure of the tool, which IR language you branch off from, and what the key ideas/difficulties involved are. I think intimidating inference rules with loads of new symbols should be saved for a later section -- the kind of section that really is only going to be read by people who are actually interested in reproducing or building upon your work. So things like `One thing to note is that the comparison is signed ... by default all operators in Verilog are unsigned ... so we force the operators to be signed' very much belong in the current section; you just don't need a scary inference rule first.} + +The translation can be described by a relational specification, which can be described by the following relation, where \textit{fin}, \textit{rtrn}, $\sigma$ and \textit{stk} are the registers for the finished signal, return value, current state and stack respectively, $i$ is the 3AC instruction being translated, and \textit{data} and \textit{control} are the data-flow and control logic map respectively. \begin{equation*} - \forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B. + \yhfunction{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control} \end{equation*} -To prove this statement, we therefore have to prove that the Verilog semantics are deterministic and that the forward simulation between the C and the Verilog holds as well. -\JW{Hm, I'm a little confused. Which theorem is the actual `correctness' theorem? Looks like we could combine the two theorems into something like \[\forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \implies (V \Downarrow_{s} B ~\text{iff}~ C \Downarrow B)\] Is that the theorem you actually want?} +\noindent An example of a rule describing the translation of an operation is the following: + +\begin{equation*} + \inferrule[Iop]{\yhfunction{tr\_op } \textit{op }\ \vec{a} = \yhconstant{OK } e}{\yhfunction{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ (\yhconstant{Iop } \textit{op }\ \vec{a}\ d\ n)\ (d \Leftarrow e)\ (\sigma \Leftarrow n)} +\end{equation*} \subsection{Forward Simulation} @@ -51,22 +60,6 @@ Firstly, as the input representation is a map, all the keys of the map will be u However, the proof of uniqueness of the keys only works if the translation function is \emph{injective}, meaning that the function will result in distinct outputs for all possible inputs. Otherwise, the proof of uniqueness of the keys for the input would not translate to a uniqueness of possible case expression matches in the output. However, in our case the translation function is actually not injective, even though it might at first seem like it, because the state is stored as an integer, whereas the map is addressable by any positive number. This means that if the positive number is greater than the maximum value that can be stored in the integer, the overflow would result in the wrong states being accessed. To make the function injective, we therefore have to prove that the input positive number is never greater than $2^{32}-1$ so that the uniqueness property also holds for the output. -\subsection{Model} - -%\JW{I think some of the following material belongs in a later section. In the current section, I think we should aim at the casual reader who is interested in understanding things like the overall structure of the tool, which IR language you branch off from, and what the key ideas/difficulties involved are. I think intimidating inference rules with loads of new symbols should be saved for a later section -- the kind of section that really is only going to be read by people who are actually interested in reproducing or building upon your work. So things like `One thing to note is that the comparison is signed ... by default all operators in Verilog are unsigned ... so we force the operators to be signed' very much belong in the current section; you just don't need a scary inference rule first.} - -The translation can be described by a relational specification, which can be described by the following relation, where \textit{fin}, \textit{rtrn}, $\sigma$ and \textit{stk} are the registers for the finished signal, return value, current state and stack respectively, $i$ is the 3AC instruction being translated, and \textit{data} and \textit{control} are the data-flow and control logic map respectively. - -\begin{equation*} - \yhfunction{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control} -\end{equation*} - -\noindent An example of a rule describing the translation of an operation is the following: - -\begin{equation*} - \inferrule[Iop]{\yhfunction{tr\_op } \textit{op }\ \vec{a} = \yhconstant{OK } e}{\yhfunction{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ (\yhconstant{Iop } \textit{op }\ \vec{a}\ d\ n)\ (d \Leftarrow e)\ (\sigma \Leftarrow n)} -\end{equation*} - \subsection{Deterministic Semantics} Finally, to prove the backward simulation given the forward simulation, it has to be shown that if we generate hardware with a specific behaviour, that it is the only possible program with that behaviour. This only has to be performed for the final intermediate language, which is Verilog, so that the backward simulation holds for the whole chain from Clight to Verilog. diff --git a/verilog.tex b/verilog.tex index 3db85fc..0eef44e 100644 --- a/verilog.tex +++ b/verilog.tex @@ -1,12 +1,10 @@ \section{Verilog}\label{sec:verilog} -This section describes the Verilog semantics that were chosen for the target language, including the changes that were made to the semantics to be a better fit as an HLS target. +This section describes the Verilog semantics that were chosen for the target language, including the changes that were made to the semantics to be a better fit as an HLS target. The Verilog standard is quite large~\cite{06_ieee_stand_veril_hardw_descr_languag,05_ieee_stand_veril_regis_trans_level_synth}, however, the syntax and semantics can be reduced to a small subset that \vericert{} needs to target. -The Verilog standard is quite large, and not all Verilog features are needed to be able to describe hardware. Many Features are only useful for simulation and do not affect the hardware itself. We can therefore restrict the Verilog semantics to the synthesisable subset of Verilog~\cite{05_ieee_stand_veril_regis_trans_level_synth}. In addition to that, HLS 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. 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 and synthesised by existing tools and how it is dictated by the standard. +The Verilog semantics is based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. This semantics is quite practical as it is restricted to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. The main features that are not supported by the syntax and semantics are continuous assignment and combinational always blocks. -The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. 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 features that are supported by the syntax and semantics are module items, such as variable declarations and always blocks, statements and expressions. As hardware designs normally describe events that will be executed periodically for an infinite amount of time, the top-level of the semantics can be described using small-step semantics, whereas the execution of one small step is then described using big-step semantics. - -The semantics of Verilog differ from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, instead of describing an algorithm, which is often done sequentially. The main construct in Verilog is the always block, which is construct that contains statements. A module can contain multiple always blocks, which all run in parallel. These always blocks further contain statements such as if-statements or assignments to variables. Each always block also contains a list of events at which it should trigger, which could either contain signals that are assigned to other signals in that always block, or a different signal such as a clock which will trigger the always block periodically, only the latter are actually supported in our target semantics. An example of a rule in the semantics for executing an always block in the semantics shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the always block: +The semantics of Verilog differ from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, instead of describing an algorithm, which is often done sequentially. The main construct in Verilog is the always block, which is construct that contains statements. A module can contain multiple always blocks, which all run in parallel. These always blocks further contain statements such as if-statements or assignments to variables. Each always block also contains a list of events at which it should trigger, which could either contain signals that are assigned to other signals in that always block, or a different signal such as a clock which will trigger the always block periodically, only the latter are actually supported in our target semantics. As hardware designs normally describe events that will be executed periodically for an infinite amount of time, the top-level of the semantics can be described using small-step semantics, whereas the execution of one small step is then described using big-step semantics. An example of a rule in the semantics for executing an always block in the semantics shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the always block: \begin{equation*} \inferrule[Always]{(\Sigma, s)\longrightarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \longrightarrow_{\text{always}} \Sigma'} |