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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
\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)\}}.
\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
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}
\sailval{rX}
% TODO: Fix funcl commands
\sailfclrX
\sailfclMMMrX
\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
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, and declare them as scattered functions, as well as
the \ll{ast} union.
\sailtype{iop}
\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 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}
%\sailfndecodeSomeITYPE
%\sailfnexecuteITYPE
\noindent Now we do the same thing for the load-double 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 matched 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
\anonymise{\url{https://github.com/rems-project/sail/blob/sail2/riscv/riscv_duopod.sail}}.
|
