1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
\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 by including two files from the main sail-riscv
development:
\begin{lstlisting}
$include "prelude.sail"
$include "riscv_xlen64.sail"
\end{lstlisting}
The prelude sets up basic definitions we will use, it can vary on a
per-architecture basis to account for stylistic differences in ISA
specifications. \texttt{riscv\_xlen64.sail} introduces some type
synonyms. It creates a integer type xlen, which is 64. Sail supports
definitions which are generic over both regular types, and integers
(think const generics in C++, but more expressive). We also create a
type \ll{xlenbits} for bitvectors of length \ll{xlen}.
\sailtype{xlen}
\sailtype{xlen_bytes}
\sailtype{xlenbits}
For the purpose of this example, we also introduce a type synonym for
bitvectors of length 5, which represent registers.
\sailtype{regbits}
We now set up some basic architectural state. First creating a
register of type \ll{xlenbits} 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{xlenbits} 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 : xlenbits
register nextPC : xlenbits
register Xs : vector(32, dec, xlenbits)
\end{lstlisting}
\sailval{rX}
\sailfn{rX}
\sailval{wX}
\sailfn{wX}
\sailoverloadXXX
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
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).
\sailval{MEMr}
\sailfn{MEMr}
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
\emph{scattered} definitions. First we give types for the execute and
decode functions, as well as the \ll{ast} union.
\sailtype{iop}
\begin{lstlisting}
scattered union ast
val decode : bits(32) -> option(ast) effect pure
val execute : ast -> unit effect {rmem, rreg, wreg}
\end{lstlisting}
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 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. We use the \ll{EXTS} library function that sign-extends
its argument.
\begin{lstlisting}
union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
\end{lstlisting}
\sailfclITYPEdecode
\sailfclITYPEexecute
\noindent Now we do the same thing for the load-double instruction:
\begin{lstlisting}
union clause ast = LOAD : (bits(12), regbits, regbits)
\end{lstlisting}
\sailfclLOADdecode
\sailfclLOADexecute
Finally we define the fallthrough case for the decode function. Note
that the clauses in a scattered function will be matched in the order
they appear in the file. The actual code for this example, as well as
our more complete \riscv\ specification can be found on our github at
\anonymise{\url{https://github.com/rems-project/sail-riscv/blob/master/model/riscv_duopod.sail}}.
|
