aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)AuthorFilesLines
2023-10-17RISC-V Vector Extension Supportvector-devXinlai Wan28-11/+8547
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.
2023-10-11Rename enable-fiom to enable-writable-fiomTim Hutt11-46/+46
This is a much clearer name because the option allows code to enable FIOM, it doesn't enable FIOM itself.
2023-10-11Implement menvcfgTim Hutt14-0/+104
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.
2023-10-10Fix lem build errorAlasdair1-1/+1
The speculate_conditional should be marked monadic. It would seem like the various _reservation functions should be also, but it seems like perhaps they are not implemented in lem right now.
2023-10-10Fix fmaxm.d definitionPaul A. Clarke1-1/+1
Likely a cut-and-paste error, the definition for fmaxm.d uses the fmaxm.s mnemonic, which is already used earlier in the same file.
2023-09-26Per section 3.1.1 of the Privileged Spec (Machine ISA Register misa): F/D ↵ahadali50001-3/+3
both should be disabled if F=0
2023-09-20Allow loading more than one ELF binaryAlex Richardson1-12/+21
This makes it easier to use a separate M-mode bootloader and kernel payload (e.g. OpenSBI fw_jump). It also makes it easier to test booting systems such as FreeBSD without bundling the kernel with the bootloader.
2023-09-20Refactor process_args to return the argv index instead of the valueAlex Richardson1-3/+8
This makes it possible for a follow-up commit to add logic that allows loading more than one ELF file (e.g. M-mode firmware and S-mode kernel).
2023-09-20Report the faulting virtual address in tvalAlex Richardson2-6/+6
In some cases we were reporting the translated value instead, but the privileged spec text requires the virtual address: ``` If mtval is written with a nonzero value when a breakpoint, address-misaligned, access-fault, or page-fault exception occurs on an instruction fetch, load, or store, then mtval will contain the faulting virtual address. ```
2023-09-12Remove effectsTim Hutt32-189/+189
Since Sail 0.15 (released Nov 2022), effects have had no effect. They now generate a deprecation warning. This commit removes all the effect annotations from the model, thus fixing the compiler warnings.
2023-09-12Remove non-existent function from overloadAlasdair1-2/+2
2023-09-12Remove redundant type annotations on w_pte & add explicit `var`.Tim Hutt3-5/+5
These are given on the previous line already. Sail does not let you change the type of a variable like Rust does. The `var` ensures this definitely refers to a local rather than global variable.
2023-09-12Fix some stray tabsTim Hutt2-4/+4
2023-09-12Add z3_problems to .gitignoreTim Hutt1-0/+1
This file seems to be created on every build.
2023-09-12Remove redundant _ match caseTim Hutt1-1/+0
2023-09-12Remove duplicate xor_vecTim Hutt1-2/+0
This is already provided by Sail.
2023-08-28If C cannot be disabled, all changes to misa must be suppressedahadali50001-15/+12
2023-08-28Avoid unnecessary empty lines when instruction tracing is onAlex Richardson1-2/+0
These empty lines don't add to the readability of the trace and in fact when trace redirection is enabled they result in lots of empty lines being printed to stderr which makes it impossible to read the OS boot messages.
2023-08-28Fix --help output for options without a short flagAlex Richardson1-1/+5
Previously --help printed the following: ``` -V --no-trace -� --trace-output -l --inst-limit ``` With the new change it is: ``` -V --no-trace --trace-output -l --inst-limit ```
2023-08-28csim: Allow redirecting trace output to a file using command line flagAlex Richardson3-29/+52
This is useful when booting an operating system with tracing enabled as it allows showing the printed messages on the terminal and storing the trace log to a separate file. All categorized trace messages are now redirected to the --trace-output file when passed. If this option is not gived, the current behaviour of using stdout is retained. Example usage: `./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb --trace-output /dev/stderr os-boot/linux-rv64-64mb.bbl --trace-output /tmp/linux.log`
2023-08-01Rename EXTZ and EXTSAlasdair42-256/+256
Rename EXTZ to zero_extend and EXTS to sign_extend. Two main reasons for doing this - it means that the source more closely follows the descriptions in the documentation with more readable names, and EXTS and EXTZ are visually very close to each other with just the S and Z. They are also following an odd convention where they are ALLCAPS rather than snake_case like other functions in the spec. I think this convention comes from early Power specs in Sail, which influenced Sail MIPS and CHERI-MIPS, but I don't think it's a very good convention we should be keeping in sail-riscv
2023-07-04Adjust Makefile to only use posix options for sedBrian Campbell1-4/+10
Allows for (e.g.) BSD sed, which uses -i differently.
2023-06-27Add Sail documentation target to MakefileAlasdair1-0/+6
2023-06-19Add clang-format to the pre-commit hooksAlex Richardson1-0/+5
This formats the code with clang-format 15 since the pre-commit hook for clang-format 16 would require a newer version of pre-commit.
2023-06-19Update pre-commit-hooks versionAlex Richardson1-1/+2
The template that I used when adding it uses hooks from 2020. Update this to the latest version and add a minimum pre-commit version check to ensure we get sensible error messages rather than obscure failures. The minimum chosen here is 2.10 as that is the version shipping with Debian 11 and most other distributions have newer versions. If needed a newer version can always be installed using pip.
2023-06-15Run the pre-commit checks as part of CIAlex Richardson1-4/+6
Do this before installing sail or building the model to avoid wasting CI time if these basic checks are failing.
2023-06-15Run the pre-commit hook on all filesAlex Richardson28-115/+115
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.
2023-06-15Add a basic pre-commit hook and update CONTRIBUTING.mdAlex Richardson2-0/+16
Recommend installation of this basic pre-commit hook that ensures that all files are free of trailing whitespace and have a final newline. It also checks that no large files are added and that YAML files are valid.
2023-06-15Add a clang-format configuration and reformat C code (#261)Alexander Richardson11-236/+413
* Add a clang-format configuration and reformat C code From my testing it turns out the built-in WebKit style is the closest to the current style. I added a few config options to further reduce the diff and I think the current output looks reasonable. In the future it would be good to add a CI and pre-commit check to enforce that all C code is consistently formatted to reduce the need for reviewers to look for formatting issues. * Fix formatting of commented-out reservation debug code Use an empty-by-default macro instead of commented-out fprintf calls. This way clang-format can format the calls sensibly and it's easier to enable the debug prints. * Improve formatting of fprintf call in set_config_print() Clang-format does not like long string literals, so split this manually to format the call sensibly. * Fix formatting of function pointer typedef Clang-format gets this wrong `*` is part of the typedef. * Improve formatting of getopt_long call * Fix odd fprintf continuation by splitting long string literal
2023-06-12CODE_STYLE: Explicitly ban strings for non-textJessica Clarke1-0/+2
Apparently this needs stating and isn't obvious. Signed-off-by: Jessica Clarke <jrtc27@jrtc27.com>
2023-05-31Fix build for Coq 8.17Michael Sammler1-1/+1
2023-05-31Add opam packaging for the Coq outputBrian Campbell2-0/+46
2023-05-31Coq updates for Sail 0.15Brian Campbell2-15/+1
2023-05-29apply_headers: regenerate copyright headersupdate-copyright-headersPhilipp Tomsich91-79/+1075
2023-05-29LICENCE: add VRULL and myself as contributorsPhilipp Tomsich1-0/+2
2023-05-29LICENSE: update copyright yearsPhilipp Tomsich1-1/+1
2023-05-29coding style: fix style issues from merge of PR #257Philipp Tomsich2-8/+10
PR #257 was aggressively merged before all coding-style issues had been commented on. This addresses the issues that came up (except the drive-by whitespace cleanup that was contained in PR #257 and would require a force-push) in review.
2023-05-29Add Zfa extension support (excl. quad-precision)Philipp Tomsich9-6/+1067
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>
2023-05-29Fix minstret off-by-one when mcountinhibit is setTim Hutt4-12/+18
This fixes a small bug in `mcounthinhibit`. In the current code if you set `mcountinhibit=1` then it inhibits the count of that CSR write, whereas the spec says that it should only apply to future instructions: > Any CSR write takes effect after the writing instruction has otherwise completed. - From the priviledged spec, section 3.1.10 Hardware Performance Monitor.
2023-05-29Changed the pmp initial misconfiguration check so that if the low and high ↵Muhammad Bilal Sakhawat1-1/+1
range limit are the same then no pmp match
2023-05-29Add support for the Zicond extensionPhilipp Tomsich4-2/+43
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>
2023-05-29RVFI: only report write data if the write succeedsAlex Richardson1-13/+17
Only reporting the address (without data) on failures matches QEMU. This also drops the call to rvfi_write from phys_mem_write since that would result in (harmless) duplicate trace value updates.
2023-04-10Check for mstatus.FS when performing half-precision loads/storesAlex Richardson1-3/+2
Half-precision loads/stores should not be allowed if mstatus.FS is set to 0 to match single/double-precision ones.
2023-04-04fixed an issue with the -g switch which requires an argument. missing colon ↵William McSpaddden1-1/+1
in string arg to getopt_long()
2023-03-14Add a new recipe to run the Sail tests manually via GH Actions (#229)billmcspadden-riscvRafael Sene1-1/+1
Signed-off-by: Rafael Sene <rafael@riscv.org>
2023-03-14Use not() instead of ~() for boolean negation (#210)Alexander Richardson18-51/+53
This may be more readable and also matches the sail-cheri-riscv model. For now this keeps ~ overloaded to accept bool, but in the future we may want to consider removing it (which is what I did to find all uses modified in this patch)
2023-03-14Move ILLEGAL/C_ILLEGAL ast declaration to riscv_insts_begin.sail (#223)Alexander Richardson2-4/+9
This is useful for the sail-cheri-riscv model, where we would like to reuse C_ILLEGAL, but can't right now since it is current defined too late. It is needed for https://github.com/CTSRD-CHERI/sail-cheri-riscv/pull/69
2023-03-07Bump CI to Ubuntu 22.04 (#228)Jessica Clarke1-3/+1
Ubuntu 18.04 is being sunset.
2023-03-06Add wildcard cases to matches to suppress Sail warnings. (#197)Robert Norton16-85/+127
Sail tries to check for pattern match completeness and issues warnings but this often gives false positives: see discussion at https://github.com/rems-project/sail/issues/191 . To suppress these we add a wildcard case that raises an internal error. There is effectively no behaviour change as these would previously have resulted in a match error at runtime and they should be unreachable anyway. At the same time we change the DOUBLE case in memory access paths to allow for xlen > 64. Following discussion on the PR I also changed internal_error to take a file and line number as an argument to aid with debugging. Fixes: https://github.com/riscv/sail-riscv/issues/194
2023-02-23Remove duopodBrian Campbell5-244/+1
This can now be found in the Sail repository. Includes an update to sail-riscv.install