diff options
| -rw-r--r-- | algorithm.tex | 4 | ||||
| -rw-r--r-- | proof.tex | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/algorithm.tex b/algorithm.tex index 1191c93..78b8a0a 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -215,7 +215,7 @@ Figure~\ref{fig:accumulator_diagram} shows the resulting FSMD architecture. The \begin{tikzpicture} \fill[control,fill opacity=1] (6.5,0) rectangle (12,5); \fill[data,fill opacity=1] (0,0) rectangle (5.5,5); - \node at (1,4.7) {\footnotesize Data Path}; + \node at (1,4.7) {\footnotesize Data-path}; \node at (7.5,4.7) {\footnotesize Control Logic}; \fill[white,rounded corners=10pt] (7,0.5) rectangle (11.5,2.2); @@ -317,7 +317,7 @@ In addition to that, equality between \emph{unsigned} variables are actually not \subsubsection{Translating HTL to Verilog} Finally, we have to translate the HTL code into proper Verilog. % and prove that it behaves the same as the 3AC according to the Verilog semantics. -The challenge here is to translate our FSMD representation into a Verilog AST. However, as all the instructions in HTL are already expressed as Verilog statements, only the top level data path and control logic maps need to be translated to valid Verilog. We also require declarations for all the variables in the program, as well as declarations of the inputs and outputs to the module, so that the module can be used inside a larger hardware design. +The challenge here is to translate our FSMD representation into a Verilog AST. However, as all the instructions in HTL are already expressed as Verilog statements, only the top level data-path and control logic maps need to be translated to valid Verilog. We also require declarations for all the variables in the program, as well as declarations of the inputs and outputs to the module, so that the module can be used inside a larger hardware design. Figure~\ref{fig:accumulator_v} shows the final Verilog output that is generated for our example. Although this translation seems quite straight\-forward, proving that this translation is correct is complex. @@ -36,7 +36,7 @@ We prove this lemma by first establishing a specification of the translation fun \subsubsection{From Implementation to Specification}\label{sec:proof:3ac_htl:specification} %To simplify the proof, instead of using the translation algorithm as an assumption, as was done in Lemma~\ref{lemma:htl}, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness. For example, for the translation from 3AC to HTL, -The specification for the translation of 3AC instructions into HTL data path and control logic can be defined by the following predicate: +The specification for the translation of 3AC instructions into HTL data-path and control logic can be defined by the following predicate: \begin{equation*} \yhfunction{spec\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control} \end{equation*} |