From a68d9b19756801fb1633edd17aec2ac9c22d8444 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 8 Sep 2021 18:55:41 +0100 Subject: Some initial changes towards the final submission --- verilog.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'verilog.tex') diff --git a/verilog.tex b/verilog.tex index 1a1ac2f..c0eced8 100644 --- a/verilog.tex +++ b/verilog.tex @@ -63,7 +63,7 @@ The main execution of the module $\downarrow_{\text{module}}$ is split into $\do \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. +\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. \subsection{Integrating the Verilog Semantics into \compcert{}'s Model} \label{sec:verilog:integrating} -- cgit