The Sail instruction-set semantics specification language

For command line arguments, by default Sail accepts arguments of the form ‑long_opt, i.e. leading with a single - and words separated by _. For those who find this departure from standard convention distasteful, you can define the SAIL_NEW_CLI environment variable, and all such options will be formatted as ‑‑long‑opt (short opts like ‑o will remain unchanged). For backwards compatibility reasons, this default is hard to change.

For a list of all options, one can call Sail as sail -help.

To compile Sail into C, the -c option is used, like so:

The translated C is by default printed to stdout, but one can also use the -o option to output to a file, so

will generate a file called out.c. To produce an executable this needs to be compiled and linked with the C files in the $SAIL_DIR/lib directory:

The C output requires the GMP library for arbitrary precision arithmetic, as well as zlib for working with compressed ELF binaries.

There are several Sail options that affect the C output:

To compile Sail into SystemVerilog, the -sv option is used. The -o option provides a prefix that is used on the various generated files.

There are several options for the SystemVerilog output:

The are various other options that control various minutae about the generated SystemVerilog, see sail -help for more details.

Sail supports automatic code formatting similar to tools like go fmt or rustfmt. This is built into Sail itself, and can be used via the -fmt flag. To format a file my_file.sail, we would use the command:

Note that Sail does not attempt to type-check files when formatting them, so in this case we do not necessarily have to pass the other files that my_file.sail would otherwise require to type-check. However, it is perfectly fine to pass multiple files like so:

The one exception is if a file uses a custom infix operator, then the file that declares that operator must be passed before any file that uses it. So if my_file.sail uses an operator declared in operator.sail (otherwise it would not be able to parenthesize infix expressions correctly), we would be required to do:

This will format both files. If we want to avoid formatting operator.sail, we could either use -fmt_skip, like so:

or the -fmt_only option, like so:

Both of these options can be passed multiple times if required.

Formatting configuration is done using a JSON configuration file: as:

which is passed to sail with the -config flag.

The various keys supported under the "fmt" key are as follows:

If this file is not passed on the command line, Sail will check the $SAIL_CONFIG environment variable, and if that is unset it will search for a file named sail_config.json in the current working directory, then recursively backwards through parent directories.

Sail has a GHCi-style interactive interpreter. This can be used by starting Sail with sail -i. Sail will still handle any other command line arguments as per usual. To use Sail files within the interpreter they must be passed on the command line as if they were being compiled normally. One can also pass a list of commands to the interpreter by using the -is flag, as

where <file> contains a list of commands. Once inside the interactive mode, a list of available commands can be accessed by typing :commands, while :help <command> can be used to provide some documentation for each 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.

In Sail, we often define functions in two parts. First we can write the type signature for the function using the val keyword, then define the body of the function using the function keyword. In this Subsection, we will write our own version of the replicate_bits function from the Sail library. This function takes a number n and a bitvector, and creates a new bitvector containing that bitvector copied n times.

This signature shows how Sail can track the length of bitvectors and the value of integer variables in type signatures, using type variables. Type variables are written with a leading 'tick', so 'n and 'm are the type variables in the above signature.

The type bits('m) is a bitvector of length 'm, and int('n) is an integer with the value 'n. The result of this function will therefore be a bitvector of length 'n * 'm. We can also add constraints on these types. Here we require that we are replicating the input bitvector at least once with the 'n >= 1 constraint, and that the input bitvector length is at least one with the 'm >= 1 constraint. Sail will check that all callers of this function are guaranteed to satisfy these constraints.

Sail will also ensure that the output of our function has precisely the length bits('n * 'm) for all possible inputs (hence why the keyword uses the mathematical forall quantifier).

A potential implementation of this function looks like:

Functions may also have implicit parameters, e.g. we can implement a zero extension function that implicitly picks up its result length from the calling context as follows:

Implicit parameters are always integers, and they must appear first before any other parameters in the function type signature. The first argument can then just be omitted when calling the function, like so:

You may have noticed that in the definition of my_replicate_bits above, there was no return keyword. This is because unlike languages such as C and C++, and more similar to languages like OCaml and Rust, everything in Sail is an expression which evaluates to a value. A block in Sail is simply a sequence of expressions surrounded by curly braces { and }, and separated by semicolons. The value returned by a block is the value returned by the last expressions, and likewise the type of a block is determined by it’s final expressions, so { A; B; C }, will evaluate to the value of C after evaluating A and B in order. The expressions other than the final expression in the block must have type unit, which is discussed in the following section. Within blocks we can declare immutable variables using let, and mutable variables using var, for example:

The above block has type int and evaluates to the value 6.

The simplest type in Sail is the unit type unit. It is a type with a single member (). Rather than have functions that takes zero arguments, we have functions that take a single unit argument. Similarly, rather than having functions that return no results, a function with no meaningful return value can return (). The () notation reflects the fact that the unit type can be thought of as an empty tuple (see Tuples).

In Sail unit plays a similar role to void in C and C++, except unlike void it is an ordinary type and can appear anywhere and be used in generic functions.

The wikipedia page for the unit type, goes into further details on the difference between unit and void.

Sail has three basic numeric types, int, nat, and range. The type int which we have already seen above is an arbitrary precision mathematical integer. Likewise, nat is an arbitrary precision natural number. The type range('n, 'm) is an inclusive range between type variables 'n and 'm. For both int and nat we can specify a type variable that constrains elements of the type to be equal to the value of that type variable. In other words, the values of type int('n) are integers equal to 'n. So 5 : int(5) and similarly for any integer constant. These types can often be used interchangeably provided certain constraints are satisfied. For example, int('n) is equivalent to range('n, 'n) and range('n, 'm) can be converted into int('n) when 'n == 'm.

Note that bit isn’t a numeric type (i.e. it’s not range(0, 1)). This is intentional, as otherwise it would be possible to write expressions like (1 : bit) + 5 which would end up being equivalent to 6 : range(5, 6). This kind of implicit casting from bits to other numeric types would be highly undesirable. The bit type itself is a two-element type with members bitzero and bitone.

In addition, we can write a numeric type that only contains a fixed set of integers. The type {32, 64} is a type that can only contain the values 32 and 64.

Bitvector literals in Sail are written as either 0x followed by a sequence of hexadecimal digits or 0b followed by a sequence of binary digits, for example 0x12FE or 0b1010100. The length of a hex literal is always four times the number of digits, and the length of binary string is always the exact number of digits, so 0x12FE has length 16, while 0b1010100 has length 7. To ensure bitvector logic in specifications is precisely specified, we do not allow any kind of implicit widening or truncation as might occur in C. To change the length of a bitvector, explicit zero/sign extension and truncation functions must be used. Underscores can be used in bitvector literals to separate groups of bits (typically in groups of 16), for example:

We can make bitvectors as large as we need:

We can also write bitvectors very verbosely using bitzero and bitone, like:

The @ operator is used to concatenate bitvectors, for example:

For historical reasons the bit type is not equal to bits(1), and while this does simplify naively mapping the bits type into a (very inefficient!) representation like bit list in Isabelle or OCaml, it might be something we reconsider in the future.

Sail allows two different types of bitvector orderings---increasing (inc) and decreasing (dec). These two orderings are shown for the bitvector 0b10110000 below.

For increasing (bit)vectors, the 0 index is the most significant bit and the indexing increases towards the least significant bit. Whereas for decreasing (bit)vectors the least significant bit is 0 indexed, and the indexing decreases from the most significant to the least significant bit. For this reason, increasing indexing is sometimes called `most significant bit is zero' or MSB0, while decreasing indexing is sometimes called `least significant bit is zero' or LSB0. While this vector ordering makes most sense for bitvectors (it is usually called bit-ordering), in Sail it applies to all vectors. A default ordering can be set using

and this should usually be done right at the beginning of a specification. This setting is global, and increasing and decreasing bitvectors can therefore never be mixed within the same specification!

In practice decreasing order is the almost universal standard and only POWER uses increasing order. All currently maintained Sail specifications use decreasing. You may run into issues with increasing bitvectors as the code to support these is effectively never exercised as a result.

Sail has the built-in type vector, which is a polymorphic type for fixed-length vectors. For example, we could define a vector v of three integers as follows:

The first argument of the vector type is a numeric expression representing the length of the vector, and the second is the type of the vector’s elements. As mentioned in the bitvector section, the ordering of bitvectors and vectors is always the same, so:

Note that a generic vector of bits and a bitvector are not the same type, despite us being able to write them using the same syntax. This means you cannot write a function that is polymorphic over both generic vectors and bitvectors). This is because we typically want these types to have very different representations in our various Sail backends, and we don’t want to be forced into a compilation strategy that requires monomorphising such functions.

A (bit)vector can be indexed by using the vector index notation. So, in the following code:

a will be 4, and b will be 1 (we assume default Order dec here). 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.

A vector v can be sliced using the v[n .. m] notation. The indexes are always supplied with the index closest to the MSB being given first, so we would take the bottom 32-bits of a decreasing bitvector v as v[31 .. 0], and the upper 32-bits of an increasing bitvector as v[0 .. 31], i.e. the indexing order for decreasing vectors decreases, and the indexing order for increasing vectors increases.

A vector v can have an index index using [v with index = expression]. Similarly, a sub-range of v can be updated using [v with n .. m = expression] where the order of the indexes is the same as described above for increasing and decreasing vectors.

In addition to vectors, Sail also has list as a built-in type. For example:

The cons operator is ::, so we could equally write:

For those unfamiliar the word, 'cons' is derived from Lisp dialects, and has become standard functional programming jargon for such an operator — see en.wikipedia.org/wiki/Cons for more details.

Sail has tuple types which represent heterogeneous sequences containing values of different types. A tuple type (T1, T2, …​) has values (x1, x2, …​) where x1 : T1, x2 : T2 and so on. A tuple must have 2 or more elements. Some examples of tuples would be:

Note that while the function type (A, B) -> C might look like a function taking a single tuple argument, it is in fact a function taking two arguments. If we wanted to write a function taking a single tuple argument, we would instead write:

which would be called as

Sail has a string type, which is primarily used for error reporting and debugging.

A Sail string is any sequence of ASCII characters between double quotes. Backslash is used to introduce escape sequences, and the following escape sequences are supported:

Multi-line strings can be written by escaping the newline character at the end of a line:

Like most functional languages, Sail supports pattern matching via the match keyword. For example:

The match keyword takes an expression and then branches by comparing the matched value with a pattern. Each case in the match expression takes the form <pattern> => <expression>, separated by commas (a trailing comma is allowed). The cases are checked sequentially from top to bottom, and when the first pattern matches its expression will be evaluated.

The concrete match statement syntax in Sail is inspired by the syntax used in Rust — but programmers coming from languages with no pattern matching features may be unfamiliar with the concept. One can think of the match statement like a super-powered switch statement in C. At its most basic level a match statement can function like a switch statement (except without any fall-through). As in the above example we can use match to compare an expression against a sequence of values like so:

However the pattern in a match statement can also bind variables. In the following example we match on a numeric expression x + y, and if it is equal to 1 we execute the first match arm. However, if that is not the case the value of x + y is bound to a new immutable variable z.

Finally, we can use patterns to destructure values — breaking them apart into their constituent parts. For example if we have a pair expression we can break it apart into the first value in the pair and the second, which can then be used as individual variables:

These features can be combined, so if we had a pattern (first, 3) in the above example, the expression for that pattern would be executed when the second element of the pair is equal to 3, and the first element would be bound to the variable first.

Sail will check match statements for exhaustiveness (meaning that the patterns in the match cover every possible value), and prints a warning if the overall match statement is not exhaustive. There are some limitations on the exhaustiveness checker which we will discuss further below.

The match statement isn’t the only place we can use patterns. We can also use patterns in function arguments and with let, for example:

In the previous section we saw as patterns, which allowed us bind additional variables for subpatterns. However, as patterns can also be used to bind type variables. For example:

You can think of the as int('n) as matching on the return type of the get_current_xlen rather than the value, and binding it’s length to a new type variable 'n, which we can subsequently use in types later in our function. Note that even though we only know if xlen will be 32 or 64 at runtime after the call to get_current_xlen, Sail is still able to statically check all our bitvector accesses.

If a type only contains a single type variable (as int('n) does), then we allow omitting the type name and just using a variable as the type pattern, for example the following would be equivalent to the first line of example above:

If we want to give the variable xlen and the type variable 'n the same name, we could go further and simplify to:

Here we can use xlen within the function as both a regular variable xlen and as a type variable 'xlen.

Bindings made using let are always immutable, but Sail also allows mutable variables. Mutable variables are created by using the var keyword within a block.

Like let-bound variables, mutable variables are lexically scoped, so they only exist within the block that declared them.

Technically, unless the -strict_var option is used Sail also allows mutable variables to be implicitly declared, like so:

This functions identically, just without the keyword. We consider this deprecated and strongly encourage the use of the var keyword going forwards.

The assignment operator is the equality symbol, as in C and other programming languages. Sail supports a rich language of l-value forms, which can appear on the left of an assignment. These will be described in the next section.

One important thing to note is that Sail always infers the most specific type it can for variables, and in the presence of integer types with constraints, these types can be very specific. This is not a problem for immutable bindings, but can cause issues for mutable variables when explicit types are omitted. The following will not typecheck:

The reason is that Sail (correctly) infers that x has the type 'the integer equal to 3', and therefore refuses to allow us to assign 2 to it (as it well should), because two is not equal to three. To avoid this we must give an annotation with a less specific type like int.

It is common in ISA specifications to assign to complex l-values, e.g. to a subvector or named field of a bitvector register, or to an l-value computed with some auxiliary function, e.g. to select the appropriate register for the current execution model.

Sail has l-values that allow writing to individual elements of a (bit)vector:

As well as sub-ranges of a (bit)vector:

We also have vector concatenation l-values, which work much like vector concatenation patterns

For structs we can write to an individual struct field as

We can also do multiple assignment using tuples, for example:

Finally, we allow functions to appear in l-values. This is a very simple way to declare setter functions that look like custom l-values, for example:

This feature is commonly used when setting registers or memory that have some additional semantics when they are read or written. We commonly use the ad-hoc overloading feature to declare what appear to be getter/setter pairs, so for the above example we could implement a read_memory function and a write_memory function and overload them both as memory to allow us to write memory using memory(addr) = data and read memory as data = memory(addr), for example:

The following example creates a bitfield type called cr_type and a register CR of that type. The underlying bitvector type (in this case bits(8)) must be specified as part of the bitfield declaration.

If the bitvector is decreasing then indexes for the fields must also be in decreasing order, and vice-versa for an increasing vector. The field definitions can be overlapping and do not need to be contiguous.

A bitfield generates a type that is simply a struct wrapper around the underlying bitvector, with a single field called bits containing that bitvector. For the above example, this will be:

This representation is guaranteed, so it is expected that Sail code will use the bits field to access the underlying bits of the bitfield as needed. The following function shows how the bits contained in a bitfield can be accessed:

Similarly, bitfields can be updated much like regular vectors just using the field names rather than numeric indices:

Older versions of Sail did not guarantee the underlying representation of the bitfield (because it tried to do clever things to optimise them). This meant that bitfields had to be accessed using getter and setter functions, like so:

The method like accessor syntax was (overly sweet) syntactic sugar for getter and setter functions following a specific naming convention that was generated by the bitfield. These functions are still generated for backwards compatibility, but we would advise against using them.

Valid operators in Sail are sequences of the following non alpha-numeric characters: !%&*+-./:<>=@^|#. Additionally, any such sequence may be suffixed by an underscore followed by any valid identifier, so <=_u or even <=_unsigned are valid operator names. Operators may be left, right, or non-associative, and there are 10 different precedence levels, ranging from 0 to 9, with 9 binding the tightest. To declare the precedence of an operator, we use a fixity declaration like:

For left or right associative operators, we’d use the keywords infixl or infixr respectively. An operator can be used anywhere a normal identifier could be used via the operator keyword. As such, the <=_u operator can be defined as:

Sail has a flexible overloading mechanism using the overload keyword. For example:

It takes an identifier name, and a list of other identifier names to overload that name with. When the overloaded name is seen in a Sail definition, the type-checker will try each of the overloads (that are in scope) in order from left to right until it finds one that causes the resulting expression to type-check correctly.

Multiple overload declarations are permitted for the same 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 example into its own line like so:

Note that if an overload is defined in module B using identifiers provided by another module A, then a module C that requires only B will not see any of the identifiers from A, unless it also requires A. See the section on modules for details. Note that this means an overload cannot be used to 're-export' definitions provided by another module.

As an example for how overloaded functions can be used, consider the following example, where we define a function print_int and a function print_string for printing integers and strings respectively. We overload print as either print_int or print_string, so we can print either number such as 4, or strings like "Hello, World!" in the following main function definition.

We can see that the overloading has had the desired effect by dumping the type-checked AST to stdout using the following command sail -ddump_tc_ast examples/overload.sail. This will print the following, which shows how the overloading has been resolved

This option can sometimes be quite useful for observing how overloading has been resolved. Since the overloadings are done in the order they are defined, 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 their output be overloaded with functions that accept more inputs but guarantee less about their results. For example, we might have two division functions:

The first guarantees that if the first argument is greater than or equal to zero, and the second argument is greater than zero, then the result will be greater than or equal to zero. If we overload these definitions as

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. Notice that the return type can be different between different cases in the overload.

Mappings are a feature of Sail that allow concise expression of bidirectional relationships between values that are common in ISA specifications: for example, bit-representations of an enum type, or the encoding-decoding of instructions.

They are defined similarly to functions, with a val keyword to specify the type and a definition, using a bidirectional arrow <-> rather than a function arrow ->, and a separate mapping definition.

As a shorthand, you can also specify a mapping and its type simultaneously:

Mappings are used simply by calling them as if they were functions: type inference will determine in which direction the mapping is applied. (This gives rise to the restriction that the types on either side of a mapping must be different.)

Sometimes, because the subset of Sail allowed in bidirectional mapping clauses is quite restrictive, it can be useful to specify the forwards and backwards part of a mapping separately:

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 constraints. For example, if we have a function that takes two bitvectors as arguments, then there are several ways we could compute the sum of their lengths.

Note that the second line is equivalent to

There is also the constraint keyword, which takes a type-level constraint and allows it to be used as a boolean expression, so we could write:

rather than the equivalent test 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 generated theorem prover output diverging (in appearance) somewhat from the source input. In general, it is probably best to use sizeof and constraint sparingly on type variables.

One common use for sizeof however, is to lower type-level integers down to the value level, for example:

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 (they are a feature in Arm’s ASL language), and such code would be very difficult to translate into Sail if Sail did not itself support exceptions. In practice Sail language-level exceptions end up being quite a nice tool for implementing processor exceptions in ISA specifications.

For exceptions we have two language features: throw statements and try--catch blocks. The throw keyword takes a value of type exception as an argument, which can be any user defined type with that name. There is no built-in exception type, so to use exceptions one must be set up on a per-project basis. Usually the exception type will be a union, often a scattered union, which allows for the exceptions to be declared throughout the specification as they would be in OCaml, for example:

In a Sail specification, sometimes it is desirable to collect together the definitions relating to each machine instruction (or group thereof), e.g.~grouping the clauses of an AST type with the associated clauses of decode and execute functions, as in the A tutorial RISC-V style example section. Sail permits this with syntactic sugar for `scattered' definitions. Functions, mappings, unions, and enums can be scattered.

One begins a scattered definition by declaring the name and kind (either function or union) of the scattered definition, e.g.

This is then followed by clauses for either, which can be freely interleaved with other definitions. It is common to define both a scattered type (either union or enum), with a scattered function that operates on newly defined clauses of that type, as is shown below:

Finally the scattered definitions are ended with the end keyword, like so:

Technically the end keyword is not required, but it is good practice to include it as it informs Sail that the clauses are now complete, which forbids new clauses and means subsequent pattern completeness checks no longer have to require extra wildcards to account for new clauses being added.

Semantically, scattered definitions for types appear at the start of their definition (note however, that this does not mean that a module that requires just the start scattered union definition can access any constructors of a union defined in modules it does not require). Scattered definitions for functions and mappings appear at the end. A scattered function definition can be recursive, but mutually recursive scattered function definitions should be avoided.

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-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 specific external names, so for a PowerPC ISA description one might have:

while for ARM, to mimic ASL, one would have

where each backend knows about the "zero_extend" external name, but the actual Sail functions are named appropriately for each vendor’s pseudocode. As such each ISA spec written in Sail tends to have its own prelude.

Sail provides support for organizing large specifications into modules. Modules provide an access control mechanism, meaning a Sail definition in one module cannot access or use definitions provided by another module unless it explicitly requires the other module.

The module structure of a Sail project/specification is specified in a separate .sail_project file.

For a simple example, let’s assume we have two Sail files amod.sail and bmod.sail:

We can use the following .sail_project file:

This file defines two modules A and B, with module A containing the file amod.sail and module B containing the file bmod.sail. Module B requires module A, so it can use the alfa function defined in A. What would happen if we removed the requires line? We would get the following error:

This error tells us that alfa is not in scope, but Sail knows it exists as it has already checked module A, so it points us at the definition and suggests how we could resolve the error by adding the requires line we just removed.

When using a .sail_project file we do not have to pass all the files on the command line, so we can invoke Sail simply as

and it will know where to find amod.sail and bmod.sail relative to the location of the project file.

A module can have more than one Sail file. These files are processed sequentially in the order they are listed. This is exactly like what happens when we pass multiple Sail files on the command line without a .sail_project file to define the module structure. A module can therefore be thought of as a sequence of Sail files that is treated as a single logical unit. As an example, we could add a third module to our above file, which is comprised of three Sail files and depends on A and B.

Note that comments and trailing commas are allowed, and we could optionally delimit the lists using [ and ], like so:

If we wanted to we could define C in a separate file, rather than adding it to our previous file, and pass multiple project files to Sail like so:

These will be treated together as a single large project file. A use case might be if you were defining an out-of-tree extension Xfoo for sail-riscv, you could do something like:

and the modules you define in Xfoo.sail_project can require modules from riscv.sail_project, and also vice-versa, although it makes less sense in this example.

The -list_files option can be used to list all the files within a project file, which allows them to be used in a Makefile prerequisite. As an example, to build the module examples in this very manual, we use the rule below to generate documentation indexes (which our Asciidoctor plugin consumes) for every .sail file within a project file.

We can use variables in our project files to control either file inclusion within a module or to control whether a module requires another or not. A variable can even contain a sequence of modules, that can then be used in a require statement, as shown in the following example:

Modules can be marked as either optional or default. Default modules are those that form the base part of a specification, whereas optional modules are intended to implement extensions which may or may not be present. Default modules cannot require optional modules.