diff options
| -rw-r--r-- | archive/verilog.tex | 4 | ||||
| -rw-r--r-- | references.bib | 24 | ||||
| -rw-r--r-- | verilog.tex | 16 |
3 files changed, 29 insertions, 15 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. diff --git a/references.bib b/references.bib index cd232b5..29bd581 100644 --- a/references.bib +++ b/references.bib @@ -512,19 +512,21 @@ booktitle = "Formal Methods and Software Engineering", year = 2005, pages = "280--299", - abstract = "This paper presents a formal verification with the Coq proof - assistant of a memory model for C-like imperative - languages. This model defines the memory layout and the - operations that manage the memory. The model has been - specified at two levels of abstraction and implemented as part - of an ongoing certification in Coq of a moderately-optimising - C compiler. Many properties of the memory have been verified - in the specification. They facilitate the definition of - precise formal semantics of C pointers. A certified OCaml code - implementing the memory model has been automatically extracted - from the specifications.", address = "Berlin, Heidelberg", editor = "Lau, Kung-Kiu and Banach, Richard", isbn = "978-3-540-32250-4", publisher = "Springer Berlin Heidelberg" } + +@inproceedings{slind08_brief_overv_hol4, + author = "Slind, Konrad and Norrish, Michael", + title = "A Brief Overview of HOL4", + booktitle = "Theorem Proving in Higher Order Logics", + year = 2008, + pages = "28--32", + address = "Berlin, Heidelberg", + editor = "Mohamed, Otmane Ait and Mu{\~{n}}oz, C{\'e}sar and Tahar, Sofi{\`e}ne", + isbn = "978-3-540-71067-7", + keywords = {theorem proving;HOL}, + publisher = "Springer Berlin Heidelberg", +} diff --git a/verilog.tex b/verilog.tex index e2a716b..9d6372c 100644 --- a/verilog.tex +++ b/verilog.tex @@ -1,14 +1,22 @@ \section{Verilog}\label{sec:verilog} -\JW{I'm not sure the Verilog syntax figure adds enough value to be worthy of inclusion in the body -- perhaps it could be demoted to an appendix. Instead, I think it would be interesting to see a bit more about how the semantics works. Not the whole gamut of inference rules or anything, but a little bit about how the rules work and what the appropriate notion of state is.} +%\JW{I'm not sure the Verilog syntax figure adds enough value to be worthy of inclusion in the body -- perhaps it could be demoted to an appendix. Instead, I think it would be interesting to see a bit more about how the semantics works. Not the whole gamut of inference rules or anything, but a little bit about how the rules work and what the appropriate notion of state is.} This section describes the Verilog semantics that were chosen for the target language, including the changes that were made to the semantics to be a better fit as an HLS target. -Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. The Verilog standard is quite large though, and not all Verilog features are needed to be able to describe hardware. Many Verilog features are only useful for simulation and do not affect the actual hardware itself, we can therefore restrict the Verilog semantics to the synthesisable subset of Verilog~\cite{05_ieee_stand_veril_regis_trans_level_synth}. In addition to that, HLS dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed. Supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated and synthesised by existing tools and how it is dictated by the standard. +Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. The Verilog standard is quite large, and not all Verilog features are needed to be able to describe hardware. Many Features are only useful for simulation and do not affect the hardware itself. We can therefore restrict the Verilog semantics to the synthesisable subset of Verilog~\cite{05_ieee_stand_veril_regis_trans_level_synth}. In addition to that, HLS dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed. Supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated and synthesised by existing tools and how it is dictated by the standard. -The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. An abstraction of the Verilog syntax that is generated is shown in Figure~\ref{fig:verilog_syntax}. The main features that are supported by the syntax and semantics are module items, such as variable declarations and always blocks, statements and expressions. +The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. The main features that are supported by the syntax and semantics are module items, such as variable declarations and always blocks, statements and expressions. As hardware designs normally describe events that will be executed periodically for an infinite amount of time, the top-level of the semantics can be described using small-step semantics, whereas the execution of one small step is then described using big-step semantics. -The semantics of Verilog differ from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, instead of describing an algorithm, which is often done sequentially. The main construct in Verilog is the always block, which is construct that contains statements. A module can contain multiple always blocks, which all run in parallel. Each always block also contains a list of events at which it should trigger, which could either contain signals that are assigned to other signals in that always block, or a different signal such as a clock which will trigger the always b lock periodically. Two types of assignments are also supported in always blocks: nonblocking and blocking assignment. Nonblocking assignment modifies the signal at the end of the timestep, and atomically, meaning a swap operation can be implement without a temporary variable. Blocking assignment, on the other hand, assigns the variable directly in the always block for later signals to pick up. 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. +The semantics of Verilog differ from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, instead of describing an algorithm, which is often done sequentially. The main construct in Verilog is the always block, which is construct that contains statements. A module can contain multiple always blocks, which all run in parallel. These always blocks further contain statements such as if-statements or assignments to variables. Each always block also contains a list of events at which it should trigger, which could either contain signals that are assigned to other signals in that always block, or a different signal such as a clock which will trigger the always block periodically, only the latter are actually supported in our target semantics. An example of a rule in the semantics for executing an always block in the semantics shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the always block: + +\begin{align*} + \inferrule[Always]{(\Sigma, s)\longrightarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \longrightarrow_{\text{always}} \Sigma'} +\end{align*} + +\noindent which shows that assuming the statement $s$ in the always block runs with state $\Sigma$ and produces the new state $\Sigma'$, the always block will result in the same final state. As only clocked always blocks are supported, and one step in the semantics correspond to one clock cycle, it means that this rule is run once per clock cycle which is what it is defined to do. + +Two types of assignments are supported in always blocks: nonblocking and blocking assignment. Nonblocking assignment modifies the signal at the end of the timestep and atomically. Blocking assignment, on the other hand, assigns the variable directly in the always block for later signals to pick up. To model both these assignments, the state $\Sigma$ can be split When targeting a hardware description language such as Verilog, it is important to be consistent between simulating the hardware and the behaviour of the synthesised result on actual hardware. In the target Verilog semantics, only clocked always blocks are supported as these ensure that there are not mismatches between simulation and synthesis, as combinational always blocks that trigger on any change of an internal signal may behave differently in simulation or synthesis based on the order of operations. This limitation in the semantics therefore helps keep the Verilog correct and consistent. In addition to that, only nonblocking assignment is used in signals that are used in multiple always blocks, which stops any race conditions from occurring as all the signal updates happen deterministically. Finally, a specific order of evaluation for the always blocks is chosen, and because of the limitations listed before, choosing an order is guaranteed to have the same behaviour as executing the always blocks in any order. |