Age | Commit message (Collapse) | Author | Files | Lines |
|
These stub functions are required for building the Riscv.thy file
from the generated lem file.
|
|
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>
|
|
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+
|
|
This PR adds the following:
General Framework and Configurations:
* Introduced the V extension's general framework and configuration setting instructions.
* Updated model/riscv_insts_vext_vset.sail and effect matching functions in riscv_vlen.sail.
* Addressed code formatting issues and made revisions post the Nov 22 meeting.
* Co-authored by Nicolas Brunie and Jessica Clarke.
Vector Load/Store Instructions:
* Integrated vector load and store instructions.
* Enhanced the implementation of SEW, LMUL, VLEN and removed real numbers from the code.
* Updated vstart settings and removed unnecessary assert statements.
* Rectified bugs in vleff instructions and overhauled coding styles.
* Incorporated guards for vector encdec clauses and optimized memory access post vector load/store failures.
Vector Integer/Fixed-Point Instructions:
* Added vector integer/fixed-point arithmetic and mask instructions.
* Improved vector EEW and EMUL checking functions and introduced illegal instruction check functions.
* Fine-tuned code formatting for vector instruction checks.
Vector Floating-Point Instructions:
* Rolled out vector floating-point instructions and updated their conversion counterparts.
* Refreshed copyright headers specific to the vector extension code.
Vector Reduction and Mask Instructions:
* Integrated vector mask and reduction instructions.
* Addressed register overlap checks for vector mask instructions.
Miscellaneous Enhancements and Fixes:
* Updated vector CSR vtype.vill settings and judgements.
* Systematized patterns for vector illegal instruction checks.
* Rectified issues in vector load/store and reduction operations.
* Purged redundant elements from the V extension code and vector floating-point functions.
* Cleaned up softfloat makefiles and renamed EXTZ and EXTS within the V extension code.
* Addressed a clang-format check issue and NaN boxing anomalies. Provided annotations for pending RVV configurations.
* Initialized default VLEN value and set vlenb CSR.
* Set constraints for vector variable initialization and added mstatus.VS settings specific to the vector extension.
|
|
This is a much clearer name because the option allows code to enable FIOM, it doesn't enable FIOM itself.
|
|
This implements the m/senvcfg(h) CSRs. This CSR is used to enable/disable extensions and behaviours for lower privilege modes. Currently the only implemented bit is FIOM which affects how fences work.
It also affects how atomic memory accesses work in non-cacheable regions, but the model does not currently support PMAs so that can't easily be implemented.
|
|
This strips trailing whitespace and fixes line endings. I had to add the
*.dump files to the exclude list to avoid excessive changes, but
ideally these would not be part of the repository since they can just be
generated by running objdump manually.
|
|
|
|
|
|
|
|
This commit adds the following:
- infrastructure for Zfa (e.g., existence macro)
- support for the following instructions:
+ FLI.[HSD]
+ FMINM.[HSD] and FMAXM.[HSD]
+ FROUND.[HSD] and FROUNDNX.[HSD]
+ FMVH.X.D and FMVP.D.X
+ FLEQ.[HSD] and FLTQ.[HSD]
+ FCVTMOD.W.D
Note the following implementation details:
FMINM and FMAXM provide similar functionality to FMIN and FMAX,
differing only in their NaN-handling:
* FMIN/FMAX return a canonical NaN only if both operands are a NaN
* FMINM/FMAXM return a canonical Nan if any operand is a NaN
Consequently, the implementation is identical to FMIN/FMAX with only
the NaN-related tests changed.
FROUND instruction rounds a floating-point number in floating-point
register rs1 and writes that integer, represented as a floating-point
number to floating-point register rd while:
* Zero and infinite inputs are copied to rd unmodified.
* NaN inputs cause the invalid operation exception flag to be set.
FROUNDNX instruction is defined similarly, but also sets the inexact
exception flag if the input differs from the rounded result and is not
NaN.
FMVH.X.D instruction is available for RV32 only and moves bits 63:32
of floating-point register rs1 into integer register rd.
FMVP.D.X instruction is available for RV32 only and moves a
double-precision number from a pair of integer registers into a
floating-point register. Integer registers rs1 and rs2 supply bits
31:0 and 63:32, respectively.
FLEQ and FLTQ instructions are defined like the FLE and FLT
instructions, except that quiet NaN inputs do not cause the invalid
operation exception flag to be set.
The FCVTMOD.W.D instruction is defined similarly to the FCVT.W.D
instruction, with the following differences:
* FCVTMOD.W.D always rounds towards zero.
* Bits 31:0 are taken from the rounded, unbounded two's complement
result, then sign-extended to XLEN bits and written to integer
register rd.
* Positive infinity, negative infinity and NaN are converted to zero.
Signed-off-by: Charalampos Mitrodimas <charalampos.mitrodimas@vrull.eu>
Signed-off-by: Philipp Tomsich <philipp.tomsich@vrull.eu>
|
|
This can now be found in the Sail repository.
Includes an update to sail-riscv.install
|
|
|
|
|
|
NB: Smstateen support is missing in the model so enabling the Zfinx
extension provides an architectural covert channel via FCSR if
privileged software is not aware of Zfinx's existence.
Co-authored-by: Jessica Clarke <jrtc27@jrtc27.com>
Co-authored-by: Ibrahim Abu Kharmeh <abukharmeh@gmail.com>
|
|
This reverts commit c5e62ea4b3d481fcd491b22b317cc319b089f05d.
|
|
* Adds Zfinx enable flag
* Hardwire misa.{f,d} and mstats.FS to 0
* Moving nan boxing functions to fdext_reg
* Swaps register names for floating point instructions
Adds new mapping to swap register names, and use it in all assembly clauses
* Disable Floating point loads, stores and moves
* Add X_or_F_s and X_or_F_d functions, and use them to access all registers for floating points
Changes register accessed for floating point instructions and modify nan boxing functions for zfinx
* Formatting
Remove couple of misplaced whitespace, unnecessary parens
* Fix inconsistent indentation in insts_dext file
* Fix spacing in fdext_regs
* Remove redundant comparasion with true/ false
* Constistant tuples spacing and removes couple of unnecessary parens.
* Consistent functions declaration & calls spacing and removes couple of unnecessary parens.
* Consistent spacing and removes couple of unnecessary comparasion with true/false
* Make spacing consistent
* Remove checks from execution stage
* Add checks to encdec stage
|
|
Merged scalar-crypto pull request #99 of 1.0.0-rc2 spec work from Ben Marshall. See https://github.com/riscv/sail-riscv/pull/99.
|
|
|
|
|
|
|
|
|
|
corner-cases in hand-rolled helpers.
|
|
|
|
|
|
|
|
Matches recent changes to Sail
|
|
|
|
|
|
|
|
For Lem, bypass the Sail implementation of {read,write}_ram and map to
atomic primitives directly.
We might want to make these functions primitive for other backends as well.
|
|
|
|
Move updated 0.11 lem files from Shaked's commit into their own directory
Remove the 0.7.1 lem directory that performed a similar purpose during the prompt monad changes
Re-add model changes from Shaked's commit with a feature flag
|
|
Move this commit to new_barriers branch until we can update C/SMT/etc
and make a new release of Sail for backwards compatability with the
opam package
This reverts commit 273ec8b0715b39844101c8081114f2697f291312.
|
|
|
|
- unify AccessType and ReadType since they were essentially redundant,
making it easier to implement PMP checks for ReadWrite/atomic accesses.
- add command line options to enable PMP in the platform
- also fix the matching for the case when all entries are off
|
|
|
|
|
|
(requires recent changes to the Coq library)
|
|
|
|
Map to a function that does not actuaylly output anything, in order to
not confuse rmem.
|
|
|
|
|
|
|
|
Works around change to write_mem function signature in monad embedding
|
|
|
|
Also copy ROOT file into the same directory
|
|
|
|
. move prover files into a single support directory
. generated_models -> generated_definitions
. reset vector -> c_emulator
|