From fe75887a8858f82c71ca617c6d3f0c2db5af6cc2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 15 Nov 2020 20:12:52 +0000 Subject: More changes to Verilog section --- archive/verilog.tex | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'archive') 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. -- cgit