1 files changed, 140 insertions, 0 deletions
diff --git a/doc/riscv.tex b/doc/riscv.tex
new file mode 100644
index 00000000..e2aa3025
--- /dev/null
+++ b/doc/riscv.tex
@@ -0,0 +1,140 @@
+\section{A tutorial \riscv\ example}
+\label{sec:riscv}
+
+We introduce the basic features of Sail via a small example from our
+\riscv\ model that includes just two instructions: add immediate and
+load double.
+
+We start with some basic type synonyms. We create a type \ll{xlen_t}
+for bitvectors of length 64, then we define a type \ll{regno}, which
+is a type synonym for the builtin type \ll{atom}. The type
+\ll{atom('n)} is a number which is exactly equal to the type variable
+\ll{atom('n)}. Type variables are syntactically marked with single
+quotes, as in ML. A \emph{constraint} can be attached to this type
+synonym---ensuring that it is only used where we can guarantee that
+its value will be between 0 and 31. Sail supports a rich variety of
+numeric types, including range types, which are statically checked. We
+then define a synonym \ll{regbits} for \ll{bits(5)}. We don't want to
+manually convert between \ll{regbits} and \ll{regno} all the time, so
+we define a function that maps between them and declare it as a
+\emph{cast}, which allows the type-checker to insert it where
+needed. By default, we do not do any automatic casting (except between
+basic numeric types when safe), but to allow idioms in ISA vendor
+description documents we support flexible user defined casts. To ensure
+that the constraint on the \ll{regno} type synonym is satisfied, we
+return an existentially quantified type \ll{\{'n, 0 <= 'n <
+  32. regno('n)\}}.
+
+\sailxlent
+\sailregno
+\sailregbits
+\sailregbitstoregno
+\sailfnregbitstoregno
+
+We now set up some basic architectural state. First creating a
+register of type \ll{xlen_t} for both the program counter \ll{PC}, and
+the next program counter, \ll{nextPC}. We define the general purpose
+registers as a vector of 32 \ll{xlen_t} bitvectors. The \ll{dec}
+keyword isn't important in this example, but Sail supports two
+different numbering schemes for (bit)vectors \ll{inc}, for most
+significant bit is zero, and \ll{dec} for least significant bit is
+zero. We then define a getter and setter for the registers, which
+ensure that the zero register is treated specially (in
+\riscv\ register 0 is always hardcoded to be 0). Finally we overload
+both the read (\ll{rX}) and write (\ll{wX}) functions as simply
+\ll{X}. This allows us to write registers as \ll{X(r) = value} and
+read registers as \ll{value = X(r)}. Sail supports flexible ad-hoc
+overloading, and has an expressive l-value language in assignments,
+with the aim of allowing pseudo-code like definitions.
+
+\begin{lstlisting}
+register PC : xlen_t
+register nextPC : xlen_t
+
+register Xs : vector(32, dec, xlen_t)
+\end{lstlisting}
+
+\sailrX
+\sailfnrX
+\sailfnrXA
+
+\sailwX
+\sailfnwX
+\sailX
+
+We also give a function \ll{MEMr} for reading memory, this function
+just points at a builtin we have defined elsewhere \TODO{Section where
+  we talk about preludes, built-in type environment etc}. Note that functions in sail are
+annotated with effects. This effect system is quite basic, but
+indicates whether or not functions read or write registers (rreg and
+wreg), read and write memory (rmem and wmem), as well as a host of
+other concurrency model related effects. They also indicate whether a
+function throws exceptions or has other non-local control flow (the
+escape effect).
+
+\sailMEMr
+\sailfnMEMr
+
+It's common when defining architecture specications to break
+instruction semantics down into separate functions that handle
+decoding (possibly even in several stages) into custom intermediate
+datatypes and executing the decoded instructions. However it's often
+desirable to group the relevant parts of these functions and datatypes
+together in one place, as they would usually be found in an
+architecture reference manual. To support this sail supports
+\emph{scattered} definitions. First we give types for the execute and
+decode functions, and declare them as scattered functions, as well as
+the \ll{ast} union.
+
+\sailiop
+
+\begin{lstlisting}
+scattered union ast
+
+val decode : bits(32) -> option(ast) effect pure
+scattered function decode
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+scattered function execute
+\end{lstlisting}
+
+Now we provide the clauses for the add immediate \ll{ast} type, as
+well as it's execute and decode clauses. We can define the decode
+function by directly pattern matching on the bitvector representing
+the instruction. Sail supports vector concatentation patterns (\ll{@}
+is the vector concatenation operator), and uses the types provided
+(e.g. \ll{bits(12)} and \ll{regbits}) to destructure the vector in the
+correct way.
+
+\begin{lstlisting}
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+\end{lstlisting}
+
+\sailfndecodeSomeITYPE
+\sailfnexecuteITYPE
+
+\noindent Now we do the same thing for the load duble instruction:
+
+\begin{lstlisting}
+union clause ast = LOAD : (bits(12), regbits, regbits)
+\end{lstlisting}
+
+\sailfndecodeSomeLOAD
+\sailfnexecuteLOAD
+
+Finally we define the fallthrough case for the decode function, and
+end all our scattered definitions. Note that the clauses in a
+scattered function will be executed in the order they appear in the
+file.
+
+\sailfndecodeNone
+
+\begin{lstlisting}
+end ast
+end decode
+end execute
+\end{lstlisting}
+
+The actual code for this example, as well as our more complete
+\riscv\ specification can be found on our github at
+\url{https://github.com/rems-project/sail/blob/sail2/riscv/riscv_duopod.sail}.