diff options
Diffstat (limited to 'chapters/hls.tex')
| -rw-r--r-- | chapters/hls.tex | 34 |
1 files changed, 16 insertions, 18 deletions
diff --git a/chapters/hls.tex b/chapters/hls.tex index 0be3f99..8a75fee 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -484,7 +484,7 @@ making it easier to prove optimisations like proper RAM insertion. \stoptikzpicture \stopplacemarginfigure -\paragraph{Translating memory} Typically, HLS-generated hardware consists of a sea of registers and +\paragraph{Translating memory.} Typically, HLS-generated hardware consists of a sea of registers and RAMs. This memory view is very different from the C memory model, so we perform the following translation from CompCert's abstract memory model to a concrete RAM. Variables that do not have their address taken are kept in registers, which correspond to the registers in 3AC. All @@ -500,17 +500,15 @@ and would instead implement it using many registers. This interface is shown on Verilog code in \in{Figure}{a}[fig:accumulator_c_rtl]. A high-level overview of the architecture and of the RAM interface can be seen in \in{Figure}[fig:accumulator_diagram]. -\paragraph{Translating instructions} - -Most 3AC instructions correspond to hardware constructs. For example, line 2 in -\in{Figure}{d}[fig:accumulator_c_rtl] shows a 32-bit register \type{x5} being initialised to 3, -after which the control flow moves execution to line 3. This initialisation is also encoded in the -Verilog generated from HTL at state 8 in both the control logic and data-path always-blocks, shown -at lines 33 and 16 respectively in \in{Figure}{a}[fig:accumulator_c_rtl]. Simple operator -instructions are translated in a similar way. For example, the add instruction is just translated -to the built-in add operator, similarly for the multiply operator. All 32-bit instructions can be -translated in this way, but some special instructions require extra care. One such instruction is -the \type{Oshrximm} instruction, which is discussed further in +\paragraph{Translating instructions.} Most 3AC instructions correspond to hardware constructs. For +example, line 2 in \in{Figure}{d}[fig:accumulator_c_rtl] shows a 32-bit register \type{x5} being +initialised to 3, after which the control flow moves execution to line 3. This initialisation is +also encoded in the Verilog generated from HTL at state 8 in both the control logic and data-path +always-blocks, shown at lines 33 and 16 respectively in \in{Figure}{a}[fig:accumulator_c_rtl]. +Simple operator instructions are translated in a similar way. For example, the add instruction is +just translated to the built-in add operator, similarly for the multiply operator. All 32-bit +instructions can be translated in this way, but some special instructions require extra care. One +such instruction is the \type{Oshrximm} instruction, which is discussed further in \in{Section}[sec:algorithm:optimisation:oshrximm]. Another is the \type{Oshldimm} instruction, which is a left rotate instruction that has no Verilog equivalent and therefore has to be implemented in terms of other operations and proven to be equivalent. The only 32-bit instructions @@ -983,12 +981,12 @@ in the hardware itself. \stoptikzpicture} \stopplacefigure -This translation is represented in \in{Section}[fig:memory_model_transl]. defines a map from blocks -to maps from memory addresses to memory contents. Each block represents an area in memory; for -example, a block can represent a global variable or a stack for a function. As there are no global -variables, the main stack can be assumed to be block 0, and this is the only block we -translate. Meanwhile, our Verilog semantics defines two finite arrays of optional values, one for -the blocking assignments map $\Gamma_{\rm a}$ and one for the nonblocking assignments map +This translation is represented in \in{Figure}[fig:memory_model_transl]. CompCert's memory model +defines a map from blocks to maps from memory addresses to memory contents. Each block represents an +area in memory; for example, a block can represent a global variable or a stack for a function. As +there are no global variables, the main stack can be assumed to be block 0, and this is the only +block we translate. Meanwhile, our Verilog semantics defines two finite arrays of optional values, +one for the blocking assignments map $\Gamma_{\rm a}$ and one for the nonblocking assignments map $\Delta_{\rm a}$. The optional values are present to ensure correct merging of the two association maps at the end of the clock cycle. The invariant used in the proofs is that block 0 should be equivalent to the merged representation of the $\Gamma_{\rm a}$ and $\Delta_{\rm a}$ maps. |