diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 8 | ||||
| -rw-r--r-- | doc/manual.tex | 19 | ||||
| -rw-r--r-- | doc/riscv.tex | 39 | ||||
| -rw-r--r-- | doc/tutorial.tex | 74 |
4 files changed, 80 insertions, 60 deletions
diff --git a/doc/Makefile b/doc/Makefile index b3802b34..7e9e4f2f 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -54,14 +54,16 @@ endif RISCV=../../sail-riscv +all: manual.pdf + .PHONY: clean -code_riscv.tex: ${RISCV}/prelude.sail ${RISCV}/riscv_duopod.sail - sail -o code_riscv -latex ${RISCV}/prelude.sail ${RISCV}/riscv_duopod.sail +code_riscv.tex: ${RISCV}/model/prelude.sail ${RISCV}/model/riscv_duopod.sail + sail -o code_riscv -latex -latex_full_valspecs ${RISCV}/model/prelude.sail ${RISCV}/model/riscv_duopod.sail cp code_riscv/commands.tex code_riscv.tex code_myreplicatebits.tex: examples/my_replicate_bits.sail - sail -o code_myreplicatebits -latex -latex_prefix mrb examples/my_replicate_bits.sail + sail -o code_myreplicatebits -latex -latex_full_valspecs -latex_prefix mrb examples/my_replicate_bits.sail cp code_myreplicatebits/commands.tex code_myreplicatebits.tex grammar.tex: ../language/sail.ott diff --git a/doc/manual.tex b/doc/manual.tex index d731ecd3..1cab3afa 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -1,5 +1,6 @@ \documentclass[a4paper]{article} +\usepackage{etoolbox} \usepackage[nounderscore]{syntax} \usepackage{amsmath,amssymb} \usepackage[svgnames]{xcolor} @@ -25,7 +26,7 @@ \lstdefinelanguage{sail} { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof, scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct, - foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw}, + foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw,constraint}, keywordstyle={\bf\ttfamily\color{blue}}, morestring=[b]", stringstyle={\ttfamily\color{red}}, @@ -44,6 +45,22 @@ \def\sail{\trivlist \item\relax} \def\endsail{\endtrivlist} +\newcommand{\saildocval}[2]{ +#1 #2 +} +\newcommand{\saildocfcl}[2]{ +#1 #2 +} +\newcommand{\saildoctype}[2]{ +#1 #2 +} +\newcommand{\saildocfn}[2]{ +#1 #2 +} +\newcommand{\saildocoverload}[2]{ +#1 #2 +} + \renewcommand{\ll}[1]{\lstinline{#1}} \newcommand{\riscv}{RISC-V} diff --git a/doc/riscv.tex b/doc/riscv.tex index 299a7bdd..586efdf4 100644 --- a/doc/riscv.tex +++ b/doc/riscv.tex @@ -25,11 +25,11 @@ 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 +\sailtype{xlen_t} +\sailtype{regno} +\sailtype{regbits} +\sailval{regbits_to_regno} +\sailfn{regbits_to_regno} 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 @@ -54,13 +54,14 @@ register nextPC : xlen_t register Xs : vector(32, dec, xlen_t) \end{lstlisting} -\sailrX -\sailfnrX -\sailfnrXA +\sailval{rX} +% TODO: Fix funcl commands +\sailfclrX +\sailfclMMMrX -\sailwX -\sailfnwX -\sailX +\sailval{wX} +\sailfn{wX} +\sailoverloadHHX We also give a function \ll{MEMr} for reading memory, this function just points at a builtin we have defined elsewhere. Note that @@ -71,8 +72,8 @@ 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 +\sailval{MEMr} +\sailfn{MEMr} It's common when defining architecture specifications to break instruction semantics down into separate functions that handle @@ -85,7 +86,7 @@ architecture reference manual. To support this Sail supports decode functions, and declare them as scattered functions, as well as the \ll{ast} union. -\sailiop +\sailtype{iop} \begin{lstlisting} scattered union ast @@ -110,8 +111,8 @@ its argument. union clause ast = ITYPE : (bits(12), regbits, regbits, iop) \end{lstlisting} -\sailfndecodeSomeITYPE -\sailfnexecuteITYPE +%\sailfndecodeSomeITYPE +%\sailfnexecuteITYPE \noindent Now we do the same thing for the load-double instruction: @@ -119,15 +120,15 @@ union clause ast = ITYPE : (bits(12), regbits, regbits, iop) union clause ast = LOAD : (bits(12), regbits, regbits) \end{lstlisting} -\sailfndecodeSomeLOAD -\sailfnexecuteLOAD +%\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 matched in the order they appear in the file. -\sailfndecodeNone +%\sailfndecodeNone \begin{lstlisting} end ast diff --git a/doc/tutorial.tex b/doc/tutorial.tex index 5a362c28..dcac1c13 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -12,14 +12,14 @@ Subsection, we will write our own version of the \ll{replicate_bits} function from the Sail library. This function takes a number $n$ and a bitvector, and copies that bitvector $n$ times. -\mrbmyreplicatebits +\mrbval{my_replicate_bits} \noindent The general syntax for a function type in Sail is as follows: \begin{center} \ll{val} \textit{name} \ll{:} \ll{forall} \textit{type variables} \ll{,} \textit{constraint} \ll{. (} \textit{type$_1$} \ll{,} $\ldots$ \ll{,} \textit{type$_2$} \ll{)} \ll{->} \textit{return type} \end{center} An implementation for the \ll{replicate_bits} function would be -follows \mrbfnmyreplicatebits +follows \mrbfn{my_replicate_bits} The general syntax for a function declaration is: \begin{center} @@ -36,7 +36,7 @@ above function, and eventually return the result \verb|0xAAA|. Typing to be evaluated fully, rather than stepping through the execution. Sail allows type variables to be used directly within expressions, so -the above could be re-written as \mrbfnmyreplicatebitstwo This +the above could be re-written as \mrbfn{my_replicate_bits_two} This notation can be succinct, but should be used with caution. What happens is that Sail will try to re-write the type variables using expressions of the appropriate size that are available within the @@ -48,8 +48,8 @@ however very useful for implementing functions with implicit parameters, e.g. we can implement a zero extension function that implicitly picks up its result length from the calling context as follows: -\mrbextzz -\mrbfnextzz +\mrbval{extz} +\mrbfn{extz} Notice that we annotated the \ll{val} declaration as a \ll{cast}---this means that the type checker is allowed to @@ -58,32 +58,32 @@ check. This is another feature that must be used carefully, because too many implicit casts can quickly result in unreadable code. Sail does not make any distinction between expressions and statements, so since there is only a single line of code within the foreach block, we -can drop it and simply write: \mrbfnmyreplicatebitsthree - -\subsection{External Bindings} - -Rather than defining functions within Sail itself, they can be mapped -onto function definitions within the various backend targets supported -by Sail. This is primarily used to setup the primitive functions -defined in the Sail library. These declarations work much like FFI -bindings in many programming languages---in Sail we provide the -\ll{val} declaration, except rather than giving a function body we -supply a string used to identify the external operator in each -backend. For example, we could link the \ll{<<} operator with the -\verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the -external function has the same name as the sail function, such as -\ll{shiftl = "shiftl"}, then we can use the shorthand syntax -\mrbshiftl - -We can map onto differently-named operations for different targets by -using a JSON-like \ll{key: "value"} notation, for example: -\mrbzeightoperatorzzerozKzKznine We can also omit backends---in which -case those targets will expect a definition written in Sail. Note that -no checking is done to ensure that the definition in the target -matches the type of the Sail function. Finally, the \ll{_} key used -above is a wildcard that will be used for any backend not otherwise -included. If we use the wildcard key, then we cannot omit specific -backends to force them to use a definition in Sail. +can drop it and simply write: \mrbfn{my_replicate_bits_three} + +%\subsection{External Bindings} + +%Rather than defining functions within Sail itself, they can be mapped +%onto function definitions within the various backend targets supported +%by Sail. This is primarily used to setup the primitive functions +%defined in the Sail library. These declarations work much like FFI +%bindings in many programming languages---in Sail we provide the +%\ll{val} declaration, except rather than giving a function body we +%supply a string used to identify the external operator in each +%backend. For example, we could link the \ll{<<} operator with the +%\verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the +%external function has the same name as the sail function, such as +%\ll{shiftl = "shiftl"}, then we can use the shorthand syntax +%\mrbshiftl + +%We can map onto differently-named operations for different targets by +%using a JSON-like \ll{key: "value"} notation, for example: +%\mrbzeightoperatorzzerozKzKznine We can also omit backends---in which +%case those targets will expect a definition written in Sail. Note that +%no checking is done to ensure that the definition in the target +%matches the type of the Sail function. Finally, the \ll{_} key used +%above is a wildcard that will be used for any backend not otherwise +%included. If we use the wildcard key, then we cannot omit specific +%backends to force them to use a definition in Sail. \subsection{Numeric Types} \label{sec:numeric} @@ -265,10 +265,10 @@ Pattern matching can be used to destructure lists, see Section~\ref{sec:pat}. Sail also has a \ll{string} type, and a \ll{real} type. The \ll{real} type is used to model arbitrary real numbers, so floating point -instructions could be specified by saying that they are equivalent to -mapping the floating point inputs to real numbers, performing the -arithmetic operation on the real numbers, and then mapping back to a -floating point value of the appropriate precision. +instructions could be specified by mapping the floating point inputs +to real numbers, performing the arithmetic operation on the real +numbers, and then mapping back to a floating point value of the +appropriate precision. \subsection{Pattern Matching} \label{sec:pat} @@ -473,8 +473,8 @@ If we were to write \end{lstlisting} instead, then \textit{pattern} would only be bound within $\textit{expression}_1$ and not any further expressions. In general -the block-form of let statements terminated with a semicolon should be -preferred within blocks. +the block-form of let statements terminated with a semicolon should +always be preferred within blocks. Variables bound within function arguments, match statement, and let-bindings are always immutable, but Sail also allows mutable |