1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
\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.
\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
\begin{subfigure}[b]{0.5\linewidth}
\inputminted{c}{data/accumulator.c}
\caption{Accumulator C code.}\label{fig:accumulator_c}
\end{subfigure}%
\begin{subfigure}[b]{0.5\linewidth}
\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}
\end{figure}
\begin{figure}
\centering
\begin{subfigure}[b]{0.5\linewidth}
\inputminted[fontsize=\tiny]{systemverilog}{data/accumulator1.v}
\caption{Accumulator HTL code.}\label{fig:accumulator_v_1}
\end{subfigure}%
\begin{subfigure}[b]{0.5\linewidth}
\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}
\end{figure}
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.
% + TODO Clarify connection between CFG and FSMD
% + TODO Explain how memory is mapped
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% TeX-command-extra-options: "-shell-escape"
%%% End:
|
