summaryrefslogtreecommitdiffstats
path: root/algorithm.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-11-20 12:02:19 +0000
committerYann Herklotz <git@yannherklotz.com>2020-11-20 12:02:31 +0000
commit80ccc619b9e046d4b11abdc14470f276dedc9ed6 (patch)
tree3f245490223ee5be10ee566426427f96d08d0f82 /algorithm.tex
parenta601adf9c61c1a4a27891ed268b4dff37887a38a (diff)
downloadoopsla21_fvhls-80ccc619b9e046d4b11abdc14470f276dedc9ed6.tar.gz
oopsla21_fvhls-80ccc619b9e046d4b11abdc14470f276dedc9ed6.zip
Remove dimensional
Diffstat (limited to 'algorithm.tex')
-rw-r--r--algorithm.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/algorithm.tex b/algorithm.tex
index cbdd0f0..3a27591 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -322,7 +322,7 @@ Although we would not claim that \vericert{} is a proper `optimising' HLS compil
\subsubsection{Byte- and word-addressable memories}
-One big difference between C and Verilog is how memory is represented. In hardware, efficient RAMs are not as available as in software, and need to be explicitly implemented by declaring two-dimensional arrays with specific properties. A major limitation is that RAMs often only allow one read and one write per clock cycle. So, to make loads and stores as efficient as possible, the RAM needs to be word-addressable, which means that an entire integer can be loaded or stored in one clock cycle.
+One big difference between C and Verilog is how memory is represented. In hardware, efficient RAMs are not as available as in software, and need to be explicitly implemented by declaring arrays with specific properties. A major limitation is that RAMs often only allow one read and one write per clock cycle. So, to make loads and stores as efficient as possible, the RAM needs to be word-addressable, which means that an entire integer can be loaded or stored in one clock cycle.
However, the memory model that \compcert{} uses for its intermediate languages is byte-addre\-ssa\-ble~\cite{blazy05_formal_verif_memor_model_c}. It therefore has to be proven that the byte-addressable memory behaves in the same way as the word-addressable memory in hardware. Any modifications of the bytes in the \compcert{} memory model also have to be shown to modify the word-addressable memory in the same way. Since only integer loads and stores are currently supported in \vericert{}, it follows that the addresses given to the loads and stores should be multiples of four. If that is the case, then the translation from byte-addressed memory to word-addressed memory can be done by dividing the address by four.
\subsubsection{Implementing the \texttt{Oshrximm} instruction}