Add more content

1 files changed, 1 insertions, 1 deletions

diff --git a/verilog.tex b/verilog.tex
index b672145..cdcbe10 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -25,7 +25,7 @@ The main addition to the Verilog syntax is the explicit declaration of inputs an
 
 \subsection{Semantics}
 
-An existing operational semantics for Verilog~\cite{loow19_verif_compil_verif_proces} was adapted for the semantics of the language that Vericert eventually targets.  This semantics is a small-step operational semantics at the clock cycle level, as hardware typically does not terminate in any way, however, within each clock cycle the semantics are constructed in a big-step style semantics.  This style of semantics matches the small-step operational semantics of \compcert{}'s register transfer language (RTL) quite well.
+An existing operational semantics for Verilog~\cite{loow19_verif_compil_verif_proces} was adapted for the semantics of the language that Vericert eventually targets.  This semantics is a small-step operational semantics at the clock cycle level, as hardware typically does not terminate in any way, however, within each clock cycle the semantics are constructed in a big-step style semantics.  This style of semantics matches the small-step operational semantics of \compcert{}'s three address code (3AC) quite well.
 
 %~\NR{So the semantics does not support combinational always blocks or assignments?}\YH{Currently not, as they are not needed.}
 %~\NR{Does the semantics also enforce that variables can only be modified within one always block (multiple drivers not allowed)? PL community might think of data races. }\YH{Will add that.}