diff options
| -rw-r--r-- | main.tex | 2 | ||||
| -rw-r--r-- | proof.tex | 51 | ||||
| -rw-r--r-- | verilog.tex | 6 |
3 files changed, 37 insertions, 22 deletions
@@ -54,7 +54,7 @@ \ANONYMOUStrue \newif\ifCOMMENTS -\COMMENTSfalse +\COMMENTStrue \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi} \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}} \newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}} @@ -4,9 +4,13 @@ Now that the Verilog semantics have been adapted to the CompCert model, we are i The main correctness theorem is the exact same correctness theorem as stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil} which 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$, where behaviour can either be convergent, divergent or ``going wrong'' and is associated with a trace $t$ of any external function calls. The following backwards simulation theorem describes this property, where $\Downarrow_{s}$ and $\Downarrow$ stand for simulation and execution 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. -\end{equation*} +\begin{theorem} + Assuming that the translation from $C$ to Verilog $V$ succeeds, then if $V$ has behaviour $B$, $C$ should have the same behaviour $B$. + + \begin{equation*} + \forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B. + \end{equation*} +\end{theorem} To prove this top-level theorem, we first have to build a specification of the translation algorith, with the properties that are needed to prove the simulation correct, which is described in Section~\ref{sec:proof:specification}. Next, a forward simulation has to be proven between the semantics of 3AC and HTL, and then between HTL and Verilog, which then implies that the forward simulation holds between C and Verilog. Then, to 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. @@ -79,21 +83,24 @@ This \texttt{match\_states} predicate that is used to match the states of the 3A Using the \texttt{match\_states}, we can then define the forward simulation for the translation, shown as a simulation diagram below, where the 3AC state can be represented by $(R,M,\textit{pc})$, $R$ being the map of values for all current registers, $M$ being the current state of memory and \textit{pc} being the current program counter. The state of HTL can also be represented by $\Gamma$, which can be split into $\Gamma_{r}$ for the current state of all registers in the module, and $\Gamma_{a}$, for the state of all arrays in the Verilog module, which represents the stack. Finally, $\mathcal{I}$ stands for the other invariants that need to hold in the \texttt{match\_states} predicate: -\begin{center} - \begin{tikzpicture} - \begin{scope} - \node[circle] (s1) at (0,1.5) {$R, M, \textit{pc}$}; - \node[circle] (r1) at (6.5,1.5) {$\Gamma_{r}, \Gamma_{a}$}; - \node[circle] (s2) at (0,0) {$R', M', \textit{pc}'$}; - \node[circle] (r2) at (6.5,0) {$\Gamma_{r}', \Gamma_{a}'$}; - \node at (6.8,0.75) {+}; - \draw (s1) -- node[above] {$\mathcal{I} \land R \le \Gamma_{r} \land M \le \Gamma_{a} \land \textit{pc} = \Gamma_{r}!\sigma$} ++ (r1); - \draw[-{Latex}] ($(s1.south) + (0,0.4)$) -- ($(s2.north) - (0,0.4)$); - \draw[-{Latex},dashed] ($(r1.south) + (0,0.2)$) -- ($(r2.north) - (0,0.2)$); - \draw[dashed] (s2) -- node[above] {$\mathcal{I} \land R' \le \Gamma_{r}' \land M' \le \Gamma_{a}' \land \textit{pc}' = \Gamma_{r}'!\sigma$} ++ (r2); - \end{scope} - \end{tikzpicture} -\end{center} +\begin{theorem} + Given the 3AC state $(R,M,\textit{pc})$ and the matching HTL state $(\Gamma_{r}, \Gamma_{a})$, assuming one step in the 3AC semantics produces state $(R',M',\textit{pc}')$, there exists one or more steps in the HTL semantics that result in matching states $(\Gamma_{r}', \Gamma_{a}')$. + \begin{center} + \begin{tikzpicture} + \begin{scope} + \node[circle] (s1) at (0,1.5) {$R, M, \textit{pc}$}; + \node[circle] (r1) at (6.5,1.5) {$\Gamma_{r}, \Gamma_{a}$}; + \node[circle] (s2) at (0,0) {$R', M', \textit{pc}'$}; + \node[circle] (r2) at (6.5,0) {$\Gamma_{r}', \Gamma_{a}'$}; + \node at (6.8,0.75) {+}; + \draw (s1) -- node[above] {$\mathcal{I} \land R \le \Gamma_{r} \land M \le \Gamma_{a} \land \textit{pc} = \Gamma_{r}!\sigma$} ++ (r1); + \draw[-{Latex}] ($(s1.south) + (0,0.4)$) -- ($(s2.north) - (0,0.4)$); + \draw[-{Latex},dashed] ($(r1.south) + (0,0.2)$) -- ($(r2.north) - (0,0.2)$); + \draw[dashed] (s2) -- node[above] {$\mathcal{I} \land R' \le \Gamma_{r}' \land M' \le \Gamma_{a}' \land \textit{pc}' = \Gamma_{r}'!\sigma$} ++ (r2); + \end{scope} + \end{tikzpicture} + \end{center} +\end{theorem} \noindent where $\le$ means ``less defined'', meaning all locations in $R$ or $M$ need to be equal to $\Gamma_{r}$ and $\Gamma_{a}$ except in the cases where the values in memory are undefined. The \texttt{match\_states} predicate can be shortened to the statement that $R$ needs to be ``less defined'' than $\Gamma_{r}$, $M$ needs to be ``less defined'' than $\Gamma_{a}$ and finally the program counter \textit{pc} needs to equal to the current value of the state register $\sigma$. @@ -109,6 +116,14 @@ Another problem with the representation of the state as an actual register is th 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. +\begin{theorem} + Semantics are deterministic if it can be shown that two behaviours $B_{1}$ and $B_{2}$ for the same program implies that the behaviours are the same. + + \begin{equation*} + C \Downarrow B_{1} \land C \Downarrow B_{2} \implies B_{1} = B_{2}. + \end{equation*} +\end{theorem} + The Verilog semantics that are used are deterministic, as the order of operation of all the constructs is defined, and there is therefore only one way to evaluate the module and only one possible behaviour. This was proven correct for the small-step semantics shown in Figure~\ref{fig:inferrence_module}. %\subsection{Coq Mechanisation} diff --git a/verilog.tex b/verilog.tex index 708ed1f..5768a43 100644 --- a/verilog.tex +++ b/verilog.tex @@ -77,7 +77,7 @@ In addition to adding support for two-dimensional arrays, support for receiving \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \textit{pc }\ \Gamma :: \textit{sf}) \longrightarrow \yhconstant{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma [ \textit{st} \mapsto \textit{pc}, r \mapsto i ])\ \epsilon} \end{gather*} \end{minipage} - \caption{Inferrence rules for modules}% + \caption{Top-level small-step semantics for Verilog modules in \compcert{}'s computational framework.}% \label{fig:inferrence_module} \end{figure*} @@ -101,10 +101,10 @@ However, as Verilog behaves quite differently to software programming languages, \item[stack] The function stack can be modelled as a RAM using a two-dimensional array in the module, denoted as \textit{stk}. \end{description} -Figure~\ref{fig:inferrence_module}\NR{This ref points to Figure 14 instead of Figure 5!} shows the inference rules that convert from one state to another. The first rule \textsc{Step} is the normal rule of execution. Assuming that the module is not being reset, and that the finish state has not been reached yet and that the current and next state are $v$ and $v'$, and finally that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Module} rule, we can then define one step in the \texttt{State}.\NR{No module rule in Fig. 5?} The \textsc{Finish} rule is the rule that returns the final value of running the module and is applied when the \textit{fin} register is set. The return value is then taken from the \textit{ret} register. +Figure~\ref{fig:inferrence_module} shows the inference rules that convert from one state to another. The first rule \textsc{Step} is the normal rule of execution. Assuming that the module is not being reset, and that the finish state has not been reached yet and that the current and next state are $v$ and $v'$, and finally that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Step} rule, we can then define one step in the \texttt{State}. The \textsc{Finish} rule is the rule that returns the final value of running the module and is applied when the \textit{fin} register is set. The return value is then taken from the \textit{ret} register. -The first thing to note about the \textsc{Call} rule is that there is no step from \texttt{State} to \texttt{Callstate}, as function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main. The same can be said about the \textsc{Return} state rule, which will only be matched for the final return value from the main function, as there is no rule that allocates another stack frame \textit{sf} except for the initial call to main. Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}\NR{Wrong figure again}, an initial state and final state need to be defined. +The first thing to note about the \textsc{Call} rule is that there is no step from \texttt{State} to \texttt{Callstate}, as function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main. The same can be said about the \textsc{Return} state rule, which will only be matched for the final return value from the main function, as there is no rule that allocates another stack frame \textit{sf} except for the initial call to main. Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}, an initial state and final state need to be defined. \begin{align*} \texttt{initial:}\quad &\forall P,\ \yhconstant{Callstate } []\ P.\texttt{main } []\\ |