diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/riscv.tex | 19 | ||||
| -rw-r--r-- | doc/tutorial.tex | 42 | ||||
| -rw-r--r-- | doc/types.tex | 2 | ||||
| -rw-r--r-- | doc/usage.tex | 25 |
4 files changed, 45 insertions, 43 deletions
diff --git a/doc/riscv.tex b/doc/riscv.tex index 1e50c90c..2ecc69df 100644 --- a/doc/riscv.tex +++ b/doc/riscv.tex @@ -64,7 +64,7 @@ register Xs : vector(32, dec, xlen_t) We also give a function \ll{MEMr} for reading memory, this function just points at a builtin we have defined elsewhere. Note that -functions in sail are annotated with effects. This effect system is +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 @@ -74,13 +74,13 @@ control flow (the escape effect). \sailMEMr \sailfnMEMr -It's common when defining architecture specications to break +It's common when defining architecture specifications 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 +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. @@ -97,13 +97,14 @@ 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 +Now we provide the clauses for the add-immediate \ll{ast} type, as +well as its 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{@} +the instruction. Sail supports vector concatenation 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. +correct way. We use the \ll{EXTS} library function that sign-extends +its argument. \begin{lstlisting} union clause ast = ITYPE : (bits(12), regbits, regbits, iop) @@ -112,7 +113,7 @@ union clause ast = ITYPE : (bits(12), regbits, regbits, iop) \sailfndecodeSomeITYPE \sailfnexecuteITYPE -\noindent Now we do the same thing for the load duble instruction: +\noindent Now we do the same thing for the load-double instruction: \begin{lstlisting} union clause ast = LOAD : (bits(12), regbits, regbits) @@ -123,7 +124,7 @@ union clause ast = LOAD : (bits(12), regbits, regbits) 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 +scattered function will be matched in the order they appear in the file. \sailfndecodeNone diff --git a/doc/tutorial.tex b/doc/tutorial.tex index 34046e2b..d325dc4d 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -63,9 +63,9 @@ can drop it and simply write: \mrbfnmyreplicatebitsthree \subsection{External Bindings} Rather than defining functions within Sail itself, they can be mapped -onto functions definition within the various backend targets supported +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 like much FFI +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 @@ -127,7 +127,7 @@ from bits to other numeric types would be highly undesirable. The \subsection{Vector Type} \label{sec:vec} -Sail has the built-in type vector, which is a polymorphic type for +Sail has the built-in type \ll{vector}, which is a polymorphic type for fixed-length vectors. For example, we could define a vector \ll{v} of three integers as follows: \begin{lstlisting} @@ -219,7 +219,7 @@ notation. So, in the following code: let a = v[0] let b = v[3] \end{lstlisting} -\ll{a} will be \ll{4}, and \ll{b} will be \ll{1} (not that \ll{v} is +\ll{a} will be \ll{4}, and \ll{b} will be \ll{1} (note that \ll{v} is \ll{dec}). By default, Sail will statically check for out of bounds errors, and will raise a type error if it cannot prove that all such vector accesses are valid. @@ -259,7 +259,7 @@ let l : list(int) = [|1, 2, 3|] \end{lstlisting} The cons operator is \ll{::}, so we could equally write: \lstinputlisting{examples/list.sail} -Pattern matching can be used to destructure lists, see Section~\ref{sec:pat} +Pattern matching can be used to destructure lists, see Section~\ref{sec:pat}. \subsection{Other Types} @@ -291,7 +291,7 @@ separated by commas. The cases are checked sequentially from top to bottom, and when the first pattern matches its expression will be evaluated. -\ll{match} in Sail is not currently check for exhaustiveness---after +\ll{match} in Sail is not currently checked for exhaustiveness---after all we could have arbitrary constraints on a numeric variable being matched upon, which would restrict the possible cases in ways that we could not determine with just a simple syntactic check. However, there @@ -392,7 +392,7 @@ bits. In the above example, \ll{b0} and \ll{b1} will have type \ll{bit}. The pattern \ll{bitone} is a bit literal, with \ll{bitzero} being the other bit literal pattern. -Note that because vectors in sail are type-polymorphic, we can also +Note that because vectors in Sail are type-polymorphic, we can also use both vector concatenation patterns and vector patterns to match against non-bit vectors. @@ -538,7 +538,7 @@ as well as sub ranges of a vector: \begin{lstlisting} { v : bits(8) = 0xFF; - v[4 .. 0] = 0x0; // assume default Order dec + v[3 .. 0] = 0x0; // assume default Order dec assert(v == 0xF0) } \end{lstlisting} @@ -625,7 +625,7 @@ registers in expressions. Unlike previous versions of Sail, referencing and de-referencing registers is done explicitly, although we can use an automatic cast to -implictly dereference registers if that semantics is desired for a +implicitly dereference registers if that semantics is desired for a specific specification that makes heavy use of register references, like so: \begin{lstlisting} @@ -736,7 +736,7 @@ generate a \lstinline[mathescape]{_get_$F$} and takes the bitfield as a reference to a register, hence why we use the \ll{->} notation. For pure updates of values of type \ll{cr} a function \lstinline[mathescape]{update_$F$} is also defined. For more -details on getters and setters, see Section~\ref{sec:getset}. A +details on getters and setters, see Section~\ref{sec:lexp}. A singleton bit in a bitfield definition, such as \ll{LT : 7} will be defined as a bitvector of length one, and not as a value of type \ll{bit}, which mirrors the behaviour of ARM's ASL language. @@ -824,7 +824,7 @@ until it finds one that causes the resulting expression to type-check correctly. Multiple \ll{overload} declarations are permitted for the same -identifier, with each overload declaration after the first adding it's +identifier, with each overload declaration after the first adding its list of identifier names to the right of the overload list (so earlier overload declarations take precedence over later ones). As such, we could split every identifier from above syntax example into it's own @@ -859,7 +859,7 @@ This option can be quite useful for testing how overloading has been resolved. Since the overloadings are done in the order they are listed in the source file, it can be important to ensure that this order is correct. A common idiom in the standard library is to have versions of -functions that guarantee more constraints about there output be +functions that guarantee more constraints about their output be overloaded with functions that accept more inputs but guarantee less about their results. For example, we might have two division functions: \begin{lstlisting} @@ -874,12 +874,12 @@ definitions as \begin{lstlisting} overload operator / = {div1, div2} \end{lstlisting} -Then the first will be applied when the constraints on it's inputs can -be resolved, and therefore the guarantees on it's output can be +Then the first will be applied when the constraints on its inputs can +be resolved, and therefore the guarantees on its output can be guaranteed, but the second will be used when this is not the case, and indeed, we will need to manually check for the division by zero case due to the option type. Note that the return type can be very -different between different cases in the overloaded. +different between different cases in the overload. The amount of arguments overloaded functions can have can also vary, so we can use this to define functions with optional arguments, e.g. @@ -900,7 +900,7 @@ ourselves as an explicit argument. \subsection{Sizeof and Constraint} \label{sec:sizeof} -As already mention in Section~\ref{sec:functions}, Sail allows for +As already mentioned in Section~\ref{sec:functions}, Sail allows for arbitrary type variables to be included within expressions. However, we can go slightly further than this, and include both arbitrary (type-level) numeric expressions in code, as well as type @@ -930,8 +930,8 @@ function f(xs, ys) = { } } \end{lstlisting} -Rather than the equivlent test \ll{length(xs) <= length(ys)}. This way -of writing expressions can be succint, and can also make it very +rather than the equivalent test \ll{length(xs) <= length(ys)}. This way +of writing expressions can be succinct, and can also make it very explicit what constraints will be generated during flow typing. However, all the constraint and sizeof definitions must be re-written to produce executable code, which can result in the @@ -991,7 +991,7 @@ mutually recursive scattered function definitions should be avoided. \subsection{Exceptions} \label{sec:exn} -Perhaps suprisingly for a specification language, Sail has exception +Perhaps surprisingly for a specification language, Sail has exception support. This is because exceptions as a language feature do sometimes appear in vendor ISA pseudocode, and such code would be very difficult to translate into Sail if Sail did not itself support exceptions. We @@ -1014,7 +1014,7 @@ be declared even after they are used. By default Sail has almost no built-in types or functions, except for the primitive types described in this Chapter. This is because -different vendor-pseudocode's have varying naming conventions and +different vendor-pseudocodes have varying naming conventions and styles for even the most basic operators, so we aim to provide flexibility and avoid committing to any particular naming convention or set of built-ins. However, each Sail backend typically implements @@ -1029,7 +1029,7 @@ val ZeroExtend = "zero_extend" : $\ldots$ \end{lstlisting} where each backend knows about the \ll{"zero_extend"} external name, but the actual Sail functions are named appropriately for each -vendor's pseudocode. As such each Sail ISA spec tends to have it's own +vendor's pseudocode. As such each Sail ISA spec tends to have its own prelude. However, the \verb+lib+ directory in the Sail repository contains some diff --git a/doc/types.tex b/doc/types.tex index a74cdea9..4d94aef0 100644 --- a/doc/types.tex +++ b/doc/types.tex @@ -167,7 +167,7 @@ follows: unsolved goals. This unification step may generate new existential variables and constraints which are added to $\mathit{Existentials}$ and $\mathit{Constraints}$ as needed. The results of this - unification step are used to resolve the univarsally-quantified type + unification step are used to resolve the universally-quantified type variables in $Q$. If $x_m$ does not contain free type variables in $Q$, then we simply check it against $B_m$. diff --git a/doc/usage.tex b/doc/usage.tex index 3b8eed5f..c37c835a 100644 --- a/doc/usage.tex +++ b/doc/usage.tex @@ -8,19 +8,20 @@ them and provides translated output. To simply typecheck Sail files, one can pass them on the command line with no other options, so for our \riscv\ spec: \begin{verbatim} -sail prelude.sail riscv_types.sail riscv_sys.sail riscv.sail +sail prelude.sail riscv_types.sail riscv_mem.sail riscv_sys.sail riscv_vmem.sail riscv.sail \end{verbatim} The sail files passed on the command line are simply treated as if -they are one large file concatentated together, although the parser +they are one large file concatenated together, although the parser will keep track of locations on a per-file basis for error-reporting. As can be seen, this specification is split into several logical components. \verb+prelude.sail+ defines the initial type environment and builtins, \verb+riscv_types.sail+ gives type -definitions used in the rest of the specification and then -\verb+riscv_sys.sail+ and \verb+riscv.sail+ implement most of the -specification. +definitions used in the rest of the specification, \verb+riscv_mem.sail+ +and \verb+riscv_vmem.sail+ describe the physical and virtual memory +interaction, and then \verb+riscv_sys.sail+ and \verb+riscv.sail+ +implement most of the specification. -For more complex projects, once can use \ll{$include} statments in +For more complex projects, once can use \ll{$include} statements in Sail source, for example: \begin{lstlisting} $include <library.sail> @@ -31,7 +32,7 @@ Here, Sail will look for \verb+library.sail+ in the \verb+$SAIL_DIR/lib+, where \verb+$SAIL_DIR+ is usually the root of the sail repository. It will search for \verb+file.sail+ relative to the location of the file containing the \ll{$include}. The space after -the include is mandatory. Sail also supports \ll{$define}, +the \ll{$include} is mandatory. Sail also supports \ll{$define}, \ll{$ifdef}, and \ll{$ifndef}. These are things that are understood by Sail itself, not a separate preprocessor, and are handled after the AST is parsed~\footnote{This can affect precedence declarations for custom user defined operators---the precedence must be redeclared in the file you are including the operator into.}. @@ -43,7 +44,7 @@ To compile a Sail specification into OCaml, one calls Sail as sail -ocaml FILES \end{verbatim} This will produce a version of the specification translated into -Ocaml, which is placed into a directory called \verb+_sbuild+, similar +OCaml, which is placed into a directory called \verb+_sbuild+, similar to ocamlbuild's \verb+_build+ directory. The generated OCaml is intended to be fairly close to the original Sail source, and currently we do not attempt to do much optimisation on this output. @@ -98,10 +99,10 @@ snapshots are provided for convenience, and are not guaranteed to be up-to-date. In order to open a theory of one of the specifications in Isabelle, -use the -l Sail command-line flag to load the session containing the +use the \verb+-l Sail+ command-line flag to load the session containing the Sail library. Snapshots of the Sail and Lem libraries are in the \verb+lib/sail+ and \verb+lib/lem+ directories, respectively. You can -tell Isabelle where to find them using the -d flag, as in +tell Isabelle where to find them using the \verb+-d+ flag, as in \begin{verbatim} isabelle jedit -l Sail -d lib/lem -d lib/sail riscv/Riscv.thy \end{verbatim} @@ -132,7 +133,7 @@ command. Here we summarize most of the other options available for Sail. Debugging options (usually for debugging Sail itself) are -indicated by starting with the letter d. +indicated by starting with the letter \verb+d+. \begin{itemize} \item {\verb+-v+} Print the Sail version. @@ -142,7 +143,7 @@ indicated by starting with the letter d. \item {\verb+-no_warn+} Turn off warnings. \item {\verb+-enum_casts+} Allow elements of enumerations to be - automatically casted to numbers. + automatically cast to numbers. \item \verb+-memo_z3+ Memoize calls to the Z3 solver. This can greatly improve typechecking times if you are repeatedly typechecking the |