From a65bdc9ee527e66cf07dd0c4dea21ad342b141b6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 16 Apr 2021 20:26:34 +0100 Subject: Add changes --- verilog.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'verilog.tex') diff --git a/verilog.tex b/verilog.tex index 368fd8d..8f03de3 100644 --- a/verilog.tex +++ b/verilog.tex @@ -62,7 +62,7 @@ The main execution of the module $\downarrow_{\text{module}}$ is split into $\do \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. -\paragraph{Removing support for external inputs to modules} Support for receiving external inputs was removed from the semantics for simplicity, as these are not needed for an HLS target. The main module in Verilog models the main function in C, and since the inputs to a C function shouldn't change during its execution, there is no need for external inputs for Verilog modules. +\paragraph{Removing support for external inputs to modules} Support for receiving external inputs was removed from the semantics for simplicity, as these are not needed for an HLS target. The main module in Verilog models the main function in C, and since the inputs to a C function should not change during its execution, there is no need for external inputs for Verilog modules. \paragraph{Simplifying representation of bitvectors} Finally, we use 32-bit integers to represent bitvectors rather than arrays of Booleans. This is because \vericert{} (currently) only supports types represented by 32 bits. -- cgit