From a5d43e7a09d71ae95e7cf6badb8ec3ddbe68362a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 20 Nov 2020 12:01:22 +0000 Subject: Fix algorithm --- algorithm.tex | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'algorithm.tex') diff --git a/algorithm.tex b/algorithm.tex index 4ea9f98..cbdd0f0 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -294,7 +294,8 @@ module main(reset, clk, finish, return_val); 32'd5: state <= 32'd4; 32'd4: state <= 32'd3; 32'd3: state <= - ({$signed(reg_1) < $signed(32'd3)} + ({$signed(reg_1) + < $signed(32'd3)} ? 32'd7 : 32'd2); 32'd2: state <= 32'd1; 32'd1: ; @@ -322,7 +323,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. -However, the memory model that \compcert{} uses for its intermediate languages is byte-addressable~\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. +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} -- cgit