From b4f5506f21bf98dc36e78a809a797413fe79e8b9 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 13 Sep 2021 00:20:52 +0100
Subject: a HLS -> an HLS

---
 verilog.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'verilog.tex')

diff --git a/verilog.tex b/verilog.tex
index 11087b0..d7980f0 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -37,7 +37,7 @@ where $\Gamma$ is the initial state of all the variables, $\epsilon$ is the empt
 
 \subsection{Changes to the Semantics}
 
-Five changes were made to the semantics proposed by \citet{loow19_proof_trans_veril_devel_hol} to make it suitable as a HLS target.
+Five changes were made to the semantics proposed by \citet{loow19_proof_trans_veril_devel_hol} to make it suitable as an HLS target.
 
 \paragraph{Adding array support}
 The main change is the addition of support for arrays, which are needed to model RAM in Verilog.  RAM is needed to model the stack in C efficiently, without having to declare a variable for each possible stack location. % In the original semantics, RAMs (as well as inputs and outputs to the module) could be modelled using a function from variable names (strings) to values, which could be modified accordingly to model inputs to the module.  This is quite an abstract description of memory and can also be expressed as an array of bitvectors instead, which is the path we took. This requires the addition of array operators to the semantics and correct reasoning of loads and stores to the array in different \alwaysblock{}s simultaneously.  
-- 
cgit 

