summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-11-21 10:24:27 +0000
committerYann Herklotz <git@yannherklotz.com>2020-11-21 10:24:37 +0000
commit3defca967808a3cd4842ca4e89a948692b3b6363 (patch)
tree11562c050357a45e536073c5ea033b2c014d5862
parentefba8f4e36ecff409eab2d2ed107593d479b754b (diff)
downloadoopsla21_fvhls-3defca967808a3cd4842ca4e89a948692b3b6363.tar.gz
oopsla21_fvhls-3defca967808a3cd4842ca4e89a948692b3b6363.zip
Add abbreviations
-rw-r--r--algorithm.tex2
-rw-r--r--verilog.tex2
2 files changed, 2 insertions, 2 deletions
diff --git a/algorithm.tex b/algorithm.tex
index 3fc7b2f..889528e 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -320,7 +320,7 @@ Finally, we have to translate the HTL code into proper Verilog. % and prove that
The challenge here is to translate our FSMD representation into a Verilog AST. However, as all the instructions in HTL are already expressed as Verilog statements, only the top level data path and control logic maps need to be translated to valid Verilog. We also require declarations for all the variables in the program, as well as declarations of the inputs and outputs to the module, so that the module can be used inside a larger hardware design.
Figure~\ref{fig:accumulator_v} shows the final Verilog output that is generated for our example.
-Although this translation seems quite straightforward, proving that this translation is correct is complex.
+Although this translation seems quite straight\-forward, proving that this translation is correct is complex.
All the implicit assumptions that were made in HTL need to be translated explicitly to Verilog statements and it needs to be shown that these explicit behaviours are equivalent to the assumptions made in the HTL semantics.
We discuss these proofs in upcoming sections.
diff --git a/verilog.tex b/verilog.tex
index 688a472..0caf06c 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -51,7 +51,7 @@ always @(posedge clk) begin
end
\end{minted}
\end{center}
-which modifies one array element using blocking assignment and then a second using nonblocking assignment. If the existing semantics were used to update the array, then during the merge, the entire array \texttt{x} from the nonblocking association map would replace the entire array from the blocking association map. This would replace \texttt{x[0]} with its original value and therefore behave incorrectly. Accordingly, we modified the maps so they record updates on a per-element basis. Our state $\Gamma$ is therefore split up into $\Gamma_{r}$ for instantaneous updates to variables, and $\Gamma_{a}$ for instantaneous updates to arrays; $\Delta$ is split similarly. The merge function then ensures that only the modified indices get updated when $\Gamma_{a}$ is merged with the nonblocking map equivalent $\Delta_{a}$.
+which modifies one array element using blocking assignment and then a second using nonblocking assignment. If the existing semantics were used to update the array, then during the merge, the entire array \texttt{x} from the nonblocking association map would replace the entire array from the blocking association map. This would replace \texttt{x[0]} with its original value and therefore behave incorrectly. Accordingly, we modified the maps so they record updates on a per-el\-em\-ent basis. Our state $\Gamma$ is therefore split up into $\Gamma_{r}$ for instantaneous updates to variables, and $\Gamma_{a}$ for instantaneous updates to arrays; $\Delta$ is split similarly. The merge function then ensures that only the modified indices get updated when $\Gamma_{a}$ is merged with the nonblocking map equivalent $\Delta_{a}$.
\paragraph{Adding declarations} Explicit support for declaring inputs, outputs and internal variables was added to the semantics to make sure that the generated Verilog also contains the correct declarations. This adds some guarantees to the generated Verilog and ensures that it synthesises and simulates correctly.