From e40fa69ac8bf0a3b38edc63bdf33e4e879c42b9b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 2 Nov 2020 10:25:52 +0000 Subject: Add macros for vericert and compcert --- algorithm.tex | 78 ++++++++++++++++++++++++++++++----------------------------- 1 file changed, 40 insertions(+), 38 deletions(-) (limited to 'algorithm.tex') diff --git a/algorithm.tex b/algorithm.tex index 425e1b0..684975c 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -1,17 +1,40 @@ -\section{Adding an HLS back end to CompCert} +\section{Adding an HLS back end to \compcert{}} -This section covers the main architecture of the HLS tool, and the way in which the backend was added to CompCert. This section will also cover an example of converting a simple C program into hardware, expressed in the Verilog language. +This section covers the main architecture of the HLS tool, and the way in which the backend was added to \compcert{}. This section will also cover an example of converting a simple C program into hardware, expressed in the Verilog language. + +\begin{figure} + \centering + \resizebox{0.47\textwidth}{!}{ + \begin{tikzpicture} + [language/.style={fill=white,rounded corners=2pt}] + \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5); + \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5); + \node[language] at (0,0) (clight) {Clight}; + \node[language] at (2,0) (cminor) {C\#minor}; + \node[language] at (4,0) (rtl) {3AC}; + \node[language] at (6,0) (ltl) {LTL}; + \node[language] at (8,0) (ppc) {PPC}; + \node[language] at (4,-2) (dfgstmd) {HTL}; + \node[language] at (7,-2) (verilog) {Verilog}; + \node at (0,1) {\compcert{}}; + \node at (0,-2) {Vericert}; + \draw[->] (clight) -- (cminor); + \draw[->,dashed] (cminor) -- (rtl); + \draw[->] (rtl) -- (ltl); + \draw[->,dashed] (ltl) -- (ppc); + \draw[->] (rtl) -- (dfgstmd); + \draw[->] (dfgstmd) -- (verilog); + \end{tikzpicture}} + \caption{Verilog backend to Compcert, branching off at the three address code (3AC), at which point the three address code is transformed into a state machine. Finally, it is transformed to a hardware description of the state machine in Verilog.}% + \label{fig:rtlbranch} +\end{figure} + +The main work flow of \vericert{} is shown in Figure~\ref{fig:rtlbranch}, which shows the parts of the translation that are performed in \compcert{}, and which have been added with \vericert{}. % - Explain main differences between translating C to software and to hardware. % + This can be done by going through the simple example. -\begin{figure*} - \centering - \includegraphics[scale=0.3,trim={10cm 10cm 7cm 7cm},clip=true]{data/accumulator_fsmd2.pdf} - \caption{Accumulator hardware diagram.}\label{fig:accumulator_diagram} -\end{figure*} - \begin{figure} \centering \begin{subfigure}[b]{0.5\linewidth} @@ -22,7 +45,7 @@ This section covers the main architecture of the HLS tool, and the way in which \inputminted[fontsize=\footnotesize]{c}{data/accumulator.rtl} \caption{Accumulator RTL code.}\label{fig:accumulator_rtl} \end{subfigure} - \caption{Accumulator example using CompCert to translate from C to three address code (3AC).}\label{fig:accumulator_c_rtl} + \caption{Accumulator example using \compcert{} to translate from C to three address code (3AC).}\label{fig:accumulator_c_rtl} \end{figure} \begin{figure} @@ -35,42 +58,21 @@ This section covers the main architecture of the HLS tool, and the way in which \inputminted[fontsize=\tiny]{systemverilog}{data/accumulator2.v} \caption{Accumulator Verilog code.}\label{fig:accumulator_v_2} \end{subfigure} - \caption{Accumulator example using CompCert to translate from HTL to Verilog.\YH{I feel like these examples take up too much space, but don't really know of a different way to show off a complete example without the long code.} \JW{Ok, what about drawing the FSMD in some sort of pictorial way? I think you tried drawing it as a schematic previously, but that was too big and clumsy. What about drawing the FSMD as a state machine, with sixteen states and labelled edges between them? Or might that be too abstract?}}\label{fig:accumulator_v} + \caption{Accumulator example using \compcert{} to translate from HTL to Verilog.\YH{I feel like these examples take up too much space, but don't really know of a different way to show off a complete example without the long code.} \JW{Ok, what about drawing the FSMD in some sort of pictorial way? I think you tried drawing it as a schematic previously, but that was too big and clumsy. What about drawing the FSMD as a state machine, with sixteen states and labelled edges between them? Or might that be too abstract?}}\label{fig:accumulator_v} \end{figure} -Taking a simple accumulator program shown in Figure~\ref{fig:accumulator_c}, we can describe the main translation that is performed in Vericert to go from the behaviour description into a hardware design. +Taking the simple accumulator program shown in Figure~\ref{fig:accumulator_c}, we can describe the main translation that is performed in Vericert to go from the behaviour description into a hardware design. + +\begin{figure*} + \centering + \includegraphics[scale=0.3,trim={10cm 10cm 7cm 7cm},clip=true]{data/accumulator_fsmd2.pdf} + \caption{Accumulator hardware diagram.}\label{fig:accumulator_diagram} +\end{figure*} % + TODO Explain the main mapping in a short simple way % - Explain why we chose 3AC (RTL) as the branching off point. -\begin{figure} - \centering - \resizebox{0.47\textwidth}{!}{ - \begin{tikzpicture} - [language/.style={fill=white,rounded corners=2pt}] - \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5); - \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5); - \node[language] at (0,0) (clight) {Clight}; - \node[language] at (2,0) (cminor) {C\#minor}; - \node[language] at (4,0) (rtl) {3AC}; - \node[language] at (6,0) (ltl) {LTL}; - \node[language] at (8,0) (ppc) {PPC}; - \node[language] at (4,-2) (dfgstmd) {HTL}; - \node[language] at (7,-2) (verilog) {Verilog}; - \node at (0,1) {CompCert}; - \node at (0,-2) {Vericert}; - \draw[->] (clight) -- (cminor); - \draw[->,dashed] (cminor) -- (rtl); - \draw[->] (rtl) -- (ltl); - \draw[->,dashed] (ltl) -- (ppc); - \draw[->] (rtl) -- (dfgstmd); - \draw[->] (dfgstmd) -- (verilog); - \end{tikzpicture}} - \caption{Verilog backend branching off at the 3AC stage in CompCert.}% - \label{fig:rtlbranch} -\end{figure} - % + TODO Clarify connection between CFG and FSMD % + TODO Explain how memory is mapped -- cgit