| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
Minor style fixes
|
|
csim: Fix C23 compatability warning
|
|
|
|
Remove unused (f)reg_name_abi functions
|
|
The plat_get_16_random_bits was missing its unit argument, which
produces the following warning:
```
generated_definitions/c/riscv_model_RV64.c:28041:34: warning: passing arguments to 'plat_get_16_random_bits' without a prototype is deprecated in all versions of C and is not supported in C2x [-Wdeprecated-non-prototype]
zseed = plat_get_16_random_bits(UNIT);
```
This commit adds the appropriate argument to the function in the C simulator
|
|
|
|
RVWMO support via Sail concurrency interface
|
|
Don't read or write 8 bytes for 4-byte PTEs
|
|
Move haveAtomics() guard for atomic instructions to guard clauses
|
|
Move haveMulDiv() guard to encdec for M extension
|
|
|
|
|
|
|
|
Very minor. Uses an existing type alias.
|
|
Fix the encoding and assembly of `vsetvl` instruction
|
|
|
|
Implicit `var` declarations will eventually be an error. This makes some implicit `var` declarations explicit.
|
|
The existing PMP code could not handle physical addresses above 32 bits on RV32, which are possible since Sv32 has 34-bit physical addresses, and the PMP registers are in units of 4 bytes, so they can encode 34-bit addresses.
This fixes that by delaying the *4 until the comparison where it can be done using `nat` instead of `xlenbits` which it would overflow.
|
|
For Sv32 Page Table Entries are only 4 bytes, but the old code was unconditionally reading and writing 8 bytes.
Fixes #459
|
|
* Remove unnecessary `f` variable
* Remove redundant type delcaration for `fetch`.
* Indentation
|
|
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.
|
|
Sail has for a while now had a flexible way of passing additional information
to either operational or axiomatic concurrency models by instantiating outcomes
(effects) with model-specific types. The set of possible outcomes is defined
in the Sail library, and a subset of these can be instantiated by any model.
As part of adapting the model to this newer concurrency interface, the
riscv_analysis file is no-longer needed, so it has been removed.
|
|
|
|
|
|
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>
|
|
Signed-off-by: Xinlai Wan <xinlai.w@rioslab.org>
|
|
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
|
|
|
