From 3defca967808a3cd4842ca4e89a948692b3b6363 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 21 Nov 2020 10:24:27 +0000 Subject: Add abbreviations --- algorithm.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'algorithm.tex') 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. -- cgit