These guards were missing from one side of each clause.

These changes add the "Svinval" Standard Extension for Fine-Grained
Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv
model.

This extension defines five new instructions: SINVAL.VMA,
SFENCE.W.INVAL, SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA.

HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the
Hypervisor Extension which is yet to be included in the model.

SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending
integration of the coherency model (rmem) with sail.

The specification says that SINVAL.VMA behaves just as SFENCE.VMA,
except there are additional ordering constraints with respect to the
new SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are
nops, we can treat SINVAL.VMA as if it were SFENCE.VMA.

Co-authored-by: Kristin Barber <kristinbarber@google.com>

    These changes add the "Svinval" Standard Extension for Fine-Grained
    Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv model.

    This extension defines five new instructions: SINVAL.VMA, SFENCE.W.INVAL,
    SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA.

    HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the
    Hypervisor Extension which is yet to be included in the model.

    SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending integration
    of the coherency model (rmem) with sail.

    The specification says that SINVAL.VMA behaves just as SFENCE.VMA,
    except there are additional ordering constraints with respect to the new
    SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are nops, we
    can treat SINVAL.VMA as if it were SFENCE.VMA.

The pre-commit check is strict about this, and even checks non code
files.

Signed-off-by: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>

Signed-off-by: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>

Signed-off-by: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>

These two instructions are RV64-only, as noted in the comment, but were missing the check. There are other instructions in this file that did have the check so it was just an ommission.

CSR MCONFIGPTR is defined in RISCV priv spec 1.12 but is missing from the
RISC-V SAIL model. This commit adds the read-only CSR MCONFIGPTR.

Co-authored-by: Dan Smathers <dan.smathers@seagate.com>

This adds an implementation of the Zcb code size extension.

Co-authored-by: Martin Berger <martinberger@users.noreply.github.com>

* Remove the duplicate mapping functions.
* Rename to `size_bytes` for consistency with the other two functions.
* Rename `size_bits` to `size_enc`, otherwise it's quite confusing that `size_bits` is not just `8 * size_bytes`.

Fixes #423

* Move `write_knd_of_flags` into its own function.
* Wrap really long lines
* Move PMP check into `phys_access_check` function. This is needed for two reasons:
  - The CBO extension needs to do explicit access checks.
  - In future it will also check PMAs so the name needs changing.

This has been broken for at least 2 years. This fixes the compilation.

Fixes #351

Old vmem code had much 'cut-and-paste' replication for RV32 (Sv32) and (#408)

RV64 (Sv39, Sv48), and was scattered over several files.

New code unifies them into single set of parameterized functions
that works for RV32/RV64 and Sv32/Sv39/Sv48 (and is ready for Sv57).

Deleted old files:
    riscv_vmem_rv32.sail    riscv_vmem_rv64.sail
    riscv_vmem_sv32.sail    riscv_vmem_sv39.sail    riscv_vmem_sv48.sail
    riscv_pte.sail
    riscv_ptw.sail

Current files: all named riscv_vmem_*
    riscv_vmem.sail    (root file for vmem)
    riscv_vmem_common.sail
    riscv_vmem_pte.sail
    riscv_vmem_ptw.sail
    riscv_vmem_tlb.sail
    riscv_vmem_types.sail

Modified top-level Makefile accordingly.

Added documentation on new vmem code: doc/notes_Virtual_Memory.adoc

Fixes #294

Use `PRIu64` for printing `uint64_t`s to prevent compiler warnings.

This is the newer, less confusing (and documented!) syntax. Fixes #425.

The restriction was present for `C.SLLI` but was missing for `C.SRLI` and `C.SRAI`.

The format is copied from `C.SLLI`.

Fixes #356

Some less-than/greater-than operators were missing. This adds the full set.

These were missed when those CSRs were implemented.

This script was used to do the modification:

```
from pathlib import Path
import re

RE_LINE = r"/\*={50,150}\*/\n"
RE_MIDDLE = r"/\*.*\*/\n"

NEW_TEXT = """/*=======================================================================================*/
/*  This Sail RISC-V architecture model, comprising all files and                        */
/*  directories except where otherwise noted is subject the BSD                          */
/*  two-clause license in the LICENSE file.                                              */
/*                                                                                       */
/*  SPDX-License-Identifier: BSD-2-Clause                                                */
/*=======================================================================================*/
"""

REPLACEMENT = re.compile(rf"^{RE_LINE}(?:{RE_MIDDLE}){{10,100}}{RE_LINE}")

def main():
    for file in Path("model").glob("**/*.sail"):
        text = file.read_text(encoding="utf-8")
        text = REPLACEMENT.sub(NEW_TEXT, text, 1)
        file.write_text(text, encoding="utf-8")

if __name__ == "__main__":
    main()
```

This implements a lot of missing functionality for PMPs.

* Support 64 PMPs as well as 0 and 16.
* Support setting PMP grain
* Return correct address bits on read (some read as 0 or 1 depending on the grain and match type)
* Unlock PMPs on reset
* Implement pmpcfg WARL legalisation

Co-authored-by: Ben Fletcher <benjamin.fletcher@codasip.com>

And string_of_bits to bits_str. These are the names that Sail uses so it makes sense to use them.

This change includes `generic_equality.sail` and `mapping.sail` from the Sail standard library which defines a lot of things that were defined in `prelude.sail`.

I also removed `reg_deref` which is no longer required.

The `mapping.sail` and `hex_bits.sail` files are in Sail 0.18 which is not yet released, so they have been temporarily copied here.

Bitfields allow [<bitfield> with field = value], like bitvectors,
so use that instead of the old-style `update_field` overloads.

Use newer bitfield syntax, which has been part of Sail for
a while now. Should in theory be more efficient as it removes
a level of indirection for bitfield accesses.

It's also much more friendly to `sail -fmt`, which has no idea
how to handle the old bitfield syntax.

Switch to bitlist representation because the machine words
can't handle the vector code currently

Remove RMEM target from default set of targets in Makefile.
This is only interesting for RMEM maintainers. There's no reason for it
to be generated by default, and it's also broken.

While we are hacking on these files purge the duplicate versions for Sail 0.11+

class is a reserved keyword in lem, so the use of class as a variable
name was causing issues. While ultimately this should be fixed in Sail
this can easily be worked around here.

Fortunately the code in questions was ultimately using a pattern like

let class = f(x);
let y = match class {
  ...
};
y

which can be simplified to

match f(x) {
  ...
}

removing the variable entirely, and making the code simpler so a
win-win overall!

Add a line to CODE_STYLE.md saying that tabs should not be used

Signed-off-by: Alasdair Armstrong <alasdair.armstrong@cl.cam.ac.uk>

Use fixed-length vectors for AES tables

Note that because we have `default Order dec`, Sail vectors
are indexed the same as bitvectors, in decreasing order, hence why
the indexing in sbox_lookup becomes
```
table[255 - unsigned(x)]
```
rather than
```
table[unsigned(x)]
```
The alternative would be to flip all the literals

This removes the warning about `opam config var`. Setting OPAMCLI in
this way is the correct thing to do if we want to continue supporting
opam 2.0.

If we decide to require opam 2.1+ then all `opam var` invocations should
become `opam --cli=2.1 var`, as per the opam CLI versioning spec:

https://github.com/ocaml/opam/wiki/Spec-for-opam-CLI-versioning