Tags: rems-project/sail
Tags
Release 0.20 CHANGES: In addition to bug-fixes and smaller improvements, the following changes and improvements have been made to the language: 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. 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. Arguments can now be passed via the `SAIL_FLAGS` environment variable, or via `SAIL_ENCODED_FLAGS`. PR: #1374
Release 0.19
CHANGES:
In addition to numerous bug-fixes and smaller improvements, the
following major changes and improvements have been made to the
language:
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 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 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.
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.
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.
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.
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.
Release 0.18
CHANGES:
This release mostly incorporates many small improvements and fixes
to Sail 0.17.1.
This release introduces a simple module system. See the section of
the manual for details.
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.
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.
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.
Release 0.17 CHANGES: 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. 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. 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. 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.
PreviousNext