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-mangleflag disables name mangling (except where
necessary for monomorphisation, or to avoid name-clashes), producing
much more readable function names. -
The
--c-generate-headerwill cause Sail to generate both a.c
file and a corresponding.hfile, rather than just a.cfile.
There is also a--c-header-includeflag which mirrors the
--c-includeflag 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.