CHANGES:

In addition to bug-fixes and smaller improvements, the following
changes and improvements have been made to the language:

Rocq Semantics

The core stepwise semantics of Sail that are currently used by the
interactive REPL and during optimisation passes like constant-folding
are now implemented in Rocq and extracted to OCaml.

Improved C++ support

New C++ --cpp backend that is a variant of the Sail C backend. It
wraps the generated model in a struct, so when using C++ multiple
instances can be created.
PR: #1437

As part of the above work, Sail always generates a separate header
file for C or C++, meaning the --c-generate-header option is
redundant and deprecated.

The --c-static option has been removed.

Small fixes to the parsing of - and foreach loops. Slightly breaking
as from, to, and downto are now treated as proper keywords and
cannot be used as identifiers.

Other changes

Arguments can now be passed via the SAIL_FLAGS environment variable,
or via SAIL_ENCODED_FLAGS.
PR: #1374

This is a binary release of Sail 0.20 for Linux, for both x86_64 (Intel/AMD) platforms and Aarch64 (Arm). It is built using a Rocky Linux container, so it should work on a wide variety of Linux distributions with more recent glibc versions.

The tarballs can be verified using GitHub artifact attestations with the GitHub CLI client, which should produce output like:

# gh attestation verify sail-Linux-x86_64.tar.gz --owner rems-project
Loaded digest sha256:45e850e28e87f9ee2b4d7cd6c934598bb2071f3cdd5b8bbfcc4d68e26ecab77b for file://sail-Linux-x86_64.tar.gz
Loaded 1 attestation from GitHub API

The following policy criteria will be enforced:
- Predicate type must match:................ https://slsa.dev/provenance/v1
- Source Repository Owner URI must match:... https://github.com/rems-project
- Subject Alternative Name must match regex: (?i)^https://github.com/rems-project/
- OIDC Issuer must match:................... https://token.actions.githubusercontent.com

✓ Verification succeeded!

The following 1 attestation matched the policy criteria

- Attestation #1
  - Build repo:..... rems-project/sail
  - Build workflow:. .github/workflows/release.yml@refs/heads/sail2
  - Signer repo:.... rems-project/sail
  - Signer workflow: .github/workflows/release.yml@refs/heads/sail2

To use the binary release, simply extract the correct tarball for your platform and add the included bin directory to your $PATH variable. By default it should know where to find the included Sail libraries and plugins relative to this directory. We include a pre-compiled version of z3, so no additional dependencies should be required.

If you want to move the binaries you will need to set the $SAIL_DIR environment variable to the included share/sail folder, and the $SAIL_PLUGIN_DIR variable to the share/libsail/plugins folder.

This is a binary release of Sail 0.19.1 for Linux. It is built using a Rocky Linux container, so it should work on a wide variety of Linux distributions with more recent glibc versions.

The tarball can be verified using GitHub artifact attestations with the GitHub CLI client, which should produce output like:

$ gh attestation verify sail.tar.gz --owner rems-project
Loaded digest sha256:7a06f699dc8724b8eae69c31a6d971d3f5b1b3512139c192d41ed4b528abb4b6 for file://sail.tar.gz
Loaded 1 attestation from GitHub API

The following policy criteria will be enforced:
- Predicate type must match:................ https://slsa.dev/provenance/v1
- Source Repository Owner URI must match:... https://github.com/rems-project
- Subject Alternative Name must match regex: (?i)^https://github.com/rems-project/
- OIDC Issuer must match:................... https://token.actions.githubusercontent.com

✓ Verification succeeded!

To use the binary release, simply extract the tarball and add the included bin directory to your $PATH variable, or symlink the included binaries from a directory already in your $PATH. By default it should know where to find the included Sail libraries and plugins relative to this directory.

If you want to move the binaries you will need to set the $SAIL_DIR environment variable to the included share/sail folder, and the $SAIL_PLUGIN_DIR variable to the share/libsail/plugins folder.

CHANGES:

This is primarily a bugfix release for Sail 0.19. It also includes
performance fixes that should significantly reduce the time and memory
usage when generating C code from Sail.

CHANGES:

In addition to numerous bug-fixes and smaller improvements, the
following major changes and improvements have been made to the
language:

Model configuration system

Sail now supports writing configurable ISA models. There is a new
language construct:

config x.y : T

which will interpret a JSON value contained at x.y in a provided
configuration file as the Sail type T. Depending on the Sail backend,
the configuration can be provided statically at build time using the
--config flag, or at runtime for C generated from Sail.

Sail is able to generate a JSON schema which describes the set of
configuration parameters supported by a model, to enable static
checking of configurations.

See the corresponding section of the Sail manual for details.

Abstract types

Abstract types are no longer behind an experimental flag. One can write:

// Declare a top-level abstract numeric type
type xlen : Int

// And then write top-level constraints about it
constraint xlen in {32, 64, 128}

These abstract types are integrated with the configuration system so
the following is supported.

type xlen : Int = config <some key>

Stricter bitvector type indexing

Stricter indexing for bitvector types. Previous versions of Sail
treated bitvector('n) as uninhabited if 'n < 0, but otherwise
permitted such bitvector types in signatures. Now the type
bitvector('n) is only well-formed if 'n >= 0. This is a breaking
change, as some previously permitted definitions are now rejected
without additional constraints. However Sail has a new kind Nat
which allows it to infer these >= 0 constraints when explicit type
variables are omitted, so in a function signature

val foo : forall 'n. bits('n) -> bool

the 'n type variable will be inferred as:

val foo : forall ('n : Nat). bits('n) -> bool

This is enabled with the --strict-bitvector flag. We expect this
behaviour will be the default in future.

Removed support for compressed ELF binaries

As a convenience feature, the Sail C runtime allowed transparently
loading compressed ELF files directly by using gzopen. However, it
is easy to just manually decompress such files before passing them to
the runtime, so we have decided to remove this feature in favour
of fewer build-time dependencies for the Sail C runtime.

Lean backend (HIGHLY EXPERIMENTAL)

This release contains the first version of a new Sail to Lean backend.

It is currently highly experimental, and will likely not compile all
Sail programs.

Sail to SystemVerilog improvements

The Sail to SystemVerilog generation has been improved significantly,
to the point where it is possible (with some hackery) get a working
sail-riscv emulator running in Verilator. Note that we still consider
this backend a work in progress, so expect to run into issues for the
time being.

Sail to C improvements

Several new flags have been implemented:

• The --c-no-mangle flag disables name mangling (except where
  necessary for monomorphisation, or to avoid name-clashes), producing
  much more readable function names.

• The --c-generate-header will cause Sail to generate both a .c
  file and a corresponding .h file, rather than just a .c file.
  There is also a --c-header-include flag which mirrors the
  --c-include flag when this option is used.

Type synonyms are now preserved into C, which makes it possible to
write external bindings that refer to polymorphic types in Sail.

Code generation for the newtype construct has been improved.

This is a binary release of Sail 0.19 for Linux. It is built using a Rocky Linux container, so it should work on a wide variety of Linux distributions with more recent glibc versions.

The tarball can be verified using GitHub artifact attestations with the GitHub CLI client, which should produce output like:

$ gh attestation verify sail.tar.gz --owner rems-project
Loaded digest sha256:0965ccab502312e01f02ada053df2aeca2437d59cb948373397029db740d7c86 for file://sail.tar.gz
Loaded 1 attestation from GitHub API

The following policy criteria will be enforced:
- Predicate type must match:................ https://slsa.dev/provenance/v1
- Source Repository Owner URI must match:... https://github.com/rems-project
- Subject Alternative Name must match regex: (?i)^https://github.com/rems-project/
- OIDC Issuer must match:................... https://token.actions.githubusercontent.com

✓ Verification succeeded!

To use the binary release, simply extract the tarball and add the included bin directory to your $PATH variable, or symlink the included binaries from a directory already in your $PATH. By default it should know where to find the included Sail libraries and plugins relative to this directory.

If you want to move the binaries you will need to set the $SAIL_DIR environment variable to the included share/sail folder, and the $SAIL_PLUGIN_DIR variable to the share/libsail/plugins folder.

This is a binary release of Sail 0.18 for Linux. It is built using a Rocky Linux container, so it should work on a wide variety of Linux distributions with more recent glibc versions.

The tarball can be verified using GitHub artifact attestations with the GitHub CLI client, which should produce output like:

$ gh attestation verify sail.tar.gz --owner rems-project
Loaded digest sha256:4e9086b867c4b15bad2b5e93f1120134d12d76730ddca7d1c222c9079157c0b8 for file:///Users/alasdair/Downloads/sail.tar.gz
Loaded 1 attestation from GitHub API
✓ Verification succeeded!

sha256:4e9086b867c4b15bad2b5e93f1120134d12d76730ddca7d1c222c9079157c0b8 was attested by:
REPO               PREDICATE_TYPE                  WORKFLOW                                             
rems-project/sail  https://slsa.dev/provenance/v1  .github/workflows/release.yml@refs/heads/release-0.18

CHANGES:

This release mostly incorporates many small improvements and fixes
to Sail 0.17.1.

Module System

This release introduces a simple module system. See the section of
the manual for details.

Type level if-then-else

If expressions are now permitted in types, so one can write types such
as

bits(if XLEN == 32 then 15 else 57)

this doesn't add any additional expressiveness, as one could
previously introduce additional type variables and constrain them in
such a way to guarantee the same thing, but being able to use
if-then-else directly is usually more clear.

Improved kind inference

Previously, type synonyms would require annotation with kinds (types
of types), for example:

union option('a : Type) = { Some : 'a, None : unit }

type xlen : Int = 64

Now, type variable kinds are inferred in most places, so the above
could be written as:

union option('a) = { Some : 'a, None : unit }

type xlen = 64

There are still some places where explicit kinds are necessary, such
as for scattered type definitions or abstract types.

Documentation backend

The Sail documentation backend can now produce hyperlinked and syntax
highlighted source code output with the --html option. The
Asciidoctor plugin can now hyperlink between definitions included in
the documentation, and otherwise link into a hyperlinked version of
the source.

CHANGES:

Updated 0.17 release with bugfixes for:

• Issue 362 #362

Additionally includes patches for better ASL to Sail compatibility

CHANGES:

Performance improvements

This release is primarily intended to fix performance issues. Overall
the Sail to C compilation can be almost 10x faster, and consumes
significantly less memory.

Order parameters deprecated

The order parameter on the bitvector and vector types no longer does
anything. The default Order <ord> statement now sets the bitvector
and vector ordering globally. In practice only POWER uses increasing
bit order, and there is never a valid reason to mix them in a
specification. Overall they added significant complexity to the
language for no real gain. Over subsequent releases a warning will be
added before they are eventually removed from the syntax.

String append pattern rework

For a while string append patterns x ^ y have been marked with a
special non-executable effect that forbids them from being used. Now
the implementation has been removed due to the deleterious effect
the generated code has on performance. Such clauses are now eagerly
removed from the syntax tree during rewriting pending a revised
implementation.

SystemVerilog backend (EXPERIMENTAL)

Sail can now produce SystemVerilog output using the -sv flag. Note
that this is not intended to be human readable or produce a
synthesizable design, but is instead intended to be used with
SystemVerilog verification tools like JasperGold.