| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
RVWMO support via Sail concurrency interface
|
|
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.
|
|
|
|
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.
|
|
This adds an implementation of the Zcb code size extension.
Co-authored-by: Martin Berger <martinberger@users.noreply.github.com>
|
|
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
|
|
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.
|
|
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+
|
|
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
|
|
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.
|
|
Allows for (e.g.) BSD sed, which uses -i differently.
|
|
|
|
|
|
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 implements the Zicond (conditional integer operations) extension,
as of version 1.0-draft-20230120.
The Zicond extension acts as a building block for branchless sequences
including conditional-arithmetic, conditional-logic and
conditional-select/move.
The following instructions constitute Zicond:
- czero.eqz rd, rs1, rs2 => rd = (rs2 == 0) ? 0 : rs1
- czero.nez rd, rs1, rs2 => rd = (rs2 != 0) ? 0 : rs1
See
https://github.com/riscv/riscv-zicond/releases/download/v1.0-draft-20230120/riscv-zicond_1.0-draft-20230120.pdf
for the proposed specification and usage details.
Co-authored-by: Jessica Clarke <jrtc27@jrtc27.com>
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
|
|
After the last commit -fcommon is no longer required.
This reverts commit ffea7a39c32a210a446379aeda0eabcec4918ed6.
|
|
|
|
|
|
|
|
The order used for wildcard is not deterministic and varies between
systems. Sorting ensures the diffs are easy to inspect going forwards.
|
|
|
|
|
|
Fixes rems-project/sail#152
|
|
* Use bool for floating point comparison result
Using bits_WU (bits(32)) or bits_LU (bits(64)) makes no sense, these are
just boolean values, and having fixed-width types is a pain for
suporting RV32D (since RV32D would need to truncate, but RV128D would
need to extend). Instead represent these as an actual bool to match what
the values really are. This could be done with bits(1) but the value is
logically a boolean (like the built-in integer comparison operators) not
a bit vector of length one so we convert to bool and back for a cleaner
interface.
* Support compiling RV32F with flen == 64
The code conflated flen and xlen; deconflating them and adding suitable
assertions (rather than silently retiring as a no-op that doesn't bump
instret) ensures that it can be compiled for RV32 with flen set to 64.
Whilst here, add the extensions and truncations that would be needed for
RV128F.
Note that there are already suitable guards on the decode clauses to
ensure these instructions are illegal on RV32.
* Support compiling RV32D
This copies various bits of XLEN generality from the F code.
* Support RV32D loads/stores
* Correctly initialise misa.D based on flen not xlen
* Makefile: Enable D extension for RV32
This now works so can be enabled.
* test: Enable RV32D tests
|
|
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.
|
|
|
|
Also tweak Makefile to remove new Coq generated files
|
|
|
|
|
|
macOS build fixes (with added fix for Ubuntu 18.04)
|
|
Add workaround for ubuntu 18.04 lack of pkg-config for libgmp.
|
|
Homebrew on Arm-based Macs installs in /opt/homebrew, and hard-coding
/opt/local was the wrong solution for MacPorts anyway. Instead, use
pkg-config to query the right compiler and linker flags for gmp and
zlib.
|
|
I was building sail-cheri-riscv, so previously only updated that makefile.
|
|
This currently maps their assembly renditions to non-standard instructions to preserve bidirectional mappings.
Fixes #67 and #29.
|
|
|
|
|
|
|
|
|
|
|
|
- make opam package include files required for building rmem
|
|
Fixes #51.
|
|
|
|
accrued into fcsr.
|
|
|
|
|
|
"Recursive make commands should always use the variable MAKE, not the
explicit command name ‘make’"
See:
https://www.gnu.org/software/make/manual/make.html#MAKE-Variable
|
|
|
