Add verilog introduction

1 files changed, 26 insertions, 0 deletions

diff --git a/algorithm.tex b/algorithm.tex
index c71b54c..c367917 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -85,6 +85,32 @@ We select CompCert's three-address code (3AC)\footnote{This is known as register
 3AC is also attractive because it is the closest intermediate language to LLVM IR, which is used by several existing HLS compilers. %\JP{We already ruled out LLVM as a starting point, so this seems like it needs further qualification.}\YH{Well not because it's not a good starting point, but the ecosystem in Coq isn't as good.  I think it's still OK here to say that being similar to LLVM IR is an advantage?} 
 It has an unlimited number of pseudo-registers, and is represented as a control flow graph (CFG) where each instruction is a node with links to the instructions that can follow it. One difference between LLVM IR and 3AC is that 3AC includes operations that are specific to the chosen target architecture; we chose to target the x86\_32 backend because it generally produces relatively dense 3AC thanks to the availability of complex addressing modes.% reducing cycle counts in the absence of an effective scheduling approach.
 
+\subsection{An introduction to Verilog}
+
+This section will introduce Verilog for readers that may not be familiar with the language, introducing the parts of the language that are used in the output of \vericert{}.  Verilog is a hardware description language (HDL) and is used to design hardware from CPU's which are eventually produced as an integrated circuit, or small application specific hardware accelerators that are placed on an FPGA.  Verilog is a populare language, because it allows for fine-grained control over the hardware, as well as some high-level constructs to simplify the development.  For example, a net list with transfer delay information could be implemented in Verilog, as well as a more abstract state machine which would first have to translated to the net list level.
+
+Verilog behaves quite differently to standard software programming languages due to it having to express the parallel nature of hardware.  The basic construct to achieve this is an always-block, which is a block of assignments that are executed every time some event occurs.  In the case of \vericert{}, this event is either a positive or a negative clock edge.  Each always block triggering at the same event will be executed in parallel.  In addition to that, control-flow can also be expressed in always-blocks using if-statements or case-statements.
+
+A simple state machine can therefore be implemented as follows:
+
+\begin{minted}[linenos,xleftmargin=20pt]{verilog}{verilog}
+module main(input state, input y, input clk, output z);
+  reg x;
+  always @(posedge clk)
+    case (state)
+      1'd0: begin x <= y; end
+      1'd1: begin x <= 1'd0; z <= x; end
+    endcase
+  always @(posedge clk)
+    case (state)
+      1'd0: begin if (y) state <= 1'd1; else state <= 1'd0; end
+      1'd1: begin state <= 1'd0 end
+    endcase
+endmodule
+\end{minted}
+
+At every positive edge of the clock (\texttt{clk}), both the always-blocks will trigger simultaneously.  The first always-block controls the values of the internal state of the register \texttt{x} and the output \texttt{z}, whereas the second always-block controls the next state the state machine should go to.  When the input \texttt{state} is 0, \texttt{x} will be assigned to the input \texttt{y} using nonblocking assignment, denoted by \texttt{<=}.  Nonblocking assignment assigns registers in parallel at the end of the clock cycle, instead of sequentially throughout the always-block. In the second always block, the input \texttt{y} will be checked, and if it's high it will move on to the next state, otherwise it will stay in the current state.  When \texttt{state} is 1, the first always block will reset the value of \texttt{x} and then set \texttt{z} to the original value of \texttt{x}, as nonblocking assignment does not change it's value until the end of the clock cycle.  Finally, the last always block will set the state to be 0 again.
+
 \begin{figure}
   \centering
   \begin{subfigure}[b]{0.3\linewidth}