This matches the style of all the other instructions, which use the decoder mapping for this purpose.

This instruction had a bit of a case of 'boolean blindness' code smell,
where the mul operation was represented as a triple of booleans. This
commit refactors the implemention to use a struct with named fields for
high, signed_rs1, and signed_rs2.

The C_MUL instruction in Zcb also needs to be changed appropriately

The mul_op struct was added in riscv_types

While there do some housekeeping w.r.t the comment about a workaround for
Sail < 0.15.1, as this is no longer needed.

These stub functions are required for building the Riscv.thy file
from the generated lem file.

Furthermore, make sure variables defined by calling opam are
created using :=, so opam is not called each time they are expanded

In general we aren't requiring contributors to implement the correct
Lem/Isabelle/HOL4/Coq stubs for new extensions (this would almost
certainly be way too high a bar) so having these in the default set of
build targets just means that typing 'make' is broken until those of us
who are invested in maintaining those targets can add updates for those
stubs.

Updates the instruction mnemonics for vmandn and vmorn

* replace mnemonics "vmandnot" and "vmornot" with "vmandn" and "vmorn" respectively

* renamed MM_VMORNOT and MM_VMANDNOT to match mnemonics

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.