| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
Remove apply_header target and etc directory, as it is no longer used
|
|
#464 updated which targets are produced by just running make. This brings the README file up to date with those changes.
|
|
These OCaml files can be read only, in which case copying them for a second build fails. To work around this use the `-f` flag which ignores the read-only-ness.
|
|
`mstatus.MPP` legal values are User (`0b00`) (if U-mode implemented), Supervisor (`0b01`) (if S-mode implemented) and Machine (`0b11`). Encoding `0b10` is illegal.
|
|
These are sub-extensions for AMO and LR/SC support. Currently hard-coded to be the same as overall atomic support.
Specification: https://github.com/ved-rivos/riscv-zaamo-zalrsc
|
|
This uses the `CC` variable (which defaults to `cc`) so that compilation
works when using Clang. This also allows the compiler to be overridden
via `CC=foo make`.
|
|
This is optional according to the spec - you can check afterwards. However
1. it seems extremely unlikely that any real designs will do that for atomics, which (ignoring Zam which the model doesn't support yet), always have to be aligned, and
2. the LR and SC instructions already check before address translation, so this wasn't even consistent.
Ideally in future this would be configurable.
|
|
Remove unnecessary matches for loads/stores
|
|
Simplify the load/store code by removing the unnecessary matches on the access size. I have not done it for float loads/stores because that requires a separate change to make the float code generic over size.
This also simplifies the AMO operation by not extending and truncating the values so many times, and removing the use of to_bits.
|
|
Change ext_data_get_addr to use bytes for width
|
|
Instead of `word_width` which can only be up to 8 bytes, just use bytes. This allows larger accesses (the limit is increased to 4096), e.g. for `cbo.zero`.
|
|
This uses the Make job server so that multiple threads can be used for LTO, which speeds up the build.
|
|
fix disassembly problems
|
|
Remove duplicate type declarations for mem_read
|
|
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.
|
|
These used to be different because they had different effects annotations, but those have since been removed and now they are the same.
|
|
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
|
|
These immediates are sign extended and usually interpreted as signed, so it's less confusing to use signed numbers. This also matches SPIKE's disassembly.
|
|
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.
|
