summaryrefslogtreecommitdiffstats
path: root/algorithm.tex
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 /algorithm.tex
parentefba8f4e36ecff409eab2d2ed107593d479b754b (diff)
downloadoopsla21_fvhls-3defca967808a3cd4842ca4e89a948692b3b6363.tar.gz
oopsla21_fvhls-3defca967808a3cd4842ca4e89a948692b3b6363.zip
Add abbreviations
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 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.