diff options
Diffstat (limited to 'archive/verilog.tex')
| -rw-r--r-- | archive/verilog.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/archive/verilog.tex b/archive/verilog.tex index 01c4adb..5fc8999 100644 --- a/archive/verilog.tex +++ b/archive/verilog.tex @@ -1,3 +1,7 @@ +Using these constructs it is therefore possible to describe how hardware functions, where always blocks that are triggered by a clock periodically get translated into flip-flops and always blocks triggered by changes in any internal signals are translated into combinational logic. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \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 three address code (3AC) quite well. |