summaryrefslogtreecommitdiff
path: root/doc/riscv.tex
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-01-21 16:19:20 +0000
committerAlasdair Armstrong2019-01-21 16:19:20 +0000
commitd2d7321afb0112142966c44a8dc4719851f20035 (patch)
tree40c88ba76b765006a3f650d1bcad714c4425997d /doc/riscv.tex
parent3797f0a21c142b37c6ce0728f60b231f2230c4f0 (diff)
Fix some issues with latex generation so manual builds again
since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together)
Diffstat (limited to 'doc/riscv.tex')
-rw-r--r--doc/riscv.tex39
1 files changed, 20 insertions, 19 deletions
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