aboutsummaryrefslogtreecommitdiff
path: root/model
AgeCommit message (Collapse)AuthorFilesLines
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-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-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-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-06-15Run the pre-commit hook on all filesAlex Richardson13-28/+25
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-05-29apply_headers: regenerate copyright headersupdate-copyright-headersPhilipp Tomsich85-73/+1057
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 Tomsich4-6/+882
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 Tomsich3-2/+41
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-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-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 Campbell2-218/+0
This can now be found in the Sail repository. Includes an update to sail-riscv.install
2023-02-14Revert "added 3 new command line switches (plus functionality): ↵Jessica Clarke2-23/+0
-X/--enable-experimental-extensions, --enable-smepmp, --enable-zicond (#219)" (#220) Reverts #219. Merged without code review and with many issues. This reverts commit 43b81eafc660ab584e1684668995957764a5e684.
2023-02-13added 3 new command line switches (plus functionality): ↵Bill McSpadden2-0/+23
-X/--enable-experimental-extensions, --enable-smepmp, --enable-zicond (#219) * added 3 command-line switches: -X/--enable-experimental-extensions, --enable-Smepmp, --enable-Zicond * example commit * fixed some type warnings/errors (between int/bool)
2023-01-25Increase flexibility of the decode hook (and simplify it) (#205)Alexander Richardson3-14/+11
Previously the decoding hook (`ext_post_decode_hook`) allowed models to override the decoded `ast`. However, this is not sufficient if model extension changes interpretation of fields. Additionally, the assembly printing would always print assembly for the "baseline decode" which resulted in incorrect trace output in the sail-cheri-riscv model. With the new hook models can implement ext_decode()/ext_decode_compressed() to return an `ast` and for encodings that are not adjusted fall back to the default `encdec`/`encdec_compressed`.
2023-01-16Fix packw sign-extension (#185)Jan Henrik Weinstock1-1/+1
Signed-off-by: Jan Henrik Weinstock <jan@mwa.re> Signed-off-by: Jan Henrik Weinstock <jan@mwa.re>
2023-01-16Fix xperm4 index calculation (#186)Jan Henrik Weinstock1-2/+2
Signed-off-by: Jan Henrik Weinstock <jan@mwa.re> Signed-off-by: Jan Henrik Weinstock <jan@mwa.re>
2022-11-01riscv_step: Fix -i/--mtval-has-illegal-inst-bits option (#174)cookbook_brJessica Clarke1-0/+2
This option causes handle_illegal to pass instbits as the value to set for xtval, but instbits is never set so it ends up being 0 just as if the option was never enabled. Fix this by initialising instbits during fetch; we could make this conditional on whether the option is enabled but that seems unnecessary and introduces tighter coupling. Note that this option appears to have always been broken; when it was originally added, instbits was only written two in two cases which were both dead code and later removed in eb176111887b. Closes: #173
2022-07-13Add support for Zhinx extension (#153)Bilal Sakhawat3-155/+180
Merged after code review. Thanks everybody for helping.
2022-01-21Add support for Scalar Cryptography Zbkb, Zbkc and Zbkx Extensions (#135)Bilal Sakhawat7-27/+193
2022-01-19Add support for Zfh extension (#129)Bilal Sakhawat7-13/+1150
2022-01-19Add support for Zmmul (#122)Bilal Sakhawat2-2/+4
2021-12-05Support BitManip Zba, Zbb, Zbc and Zbs extensions (#116)Bilal Sakhawat6-0/+569
2021-11-22Implement support for Zfinx (#130)Jessica Clarke7-334/+422
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>
2021-11-17Revert "Initial introduction of zfinx (#75)"Jessica Clarke7-367/+287
This reverts commit c5e62ea4b3d481fcd491b22b317cc319b089f05d.
2021-11-17Initial introduction of zfinx (#75)Ibrahim Abu Kharmeh7-287/+367
* 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
2021-11-10scalar-crypto: aesks1i clarificationsBen Marshall2-16/+20
Trying to make the behavior of aesks1i easier to understand, and more obviously correspond to the specification. - Ensure that the aes_decode_rcon function only accepts valid values, plus add comments. - Re-name operands to aesks1i rcon -> rnum to be in line with the specification - Re-structure the Sail code for clarity based on jrtc27's suggestion.
2021-11-10scalar-crypto: whitespace consistency for SHA* instructionsBen Marshall1-6/+6
Remove weird whitespace " );" -> ");" at end of expressions to be consistent with the rest of the code base. On branch scalar-crypto-tidy Changes to be committed: modified: model/riscv_insts_zkn.sail
2021-11-10scalar-crypto: Consistent whitespace for ==Ben Marshall1-10/+10
Add spaces pre/post used of "==" operator to be consistent with the rest of the code.
2021-11-05Delete riscv_iris.sailMartin Berger1-1244/+0
File is no longer needed, as per this discussion: https://github.com/riscv/sail-riscv/issues/119
2021-10-22Support D extension on RV32 (#108)Jessica Clarke4-104/+88
* 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
2021-10-18scalar-crypto: Initial commit of 1.0.0-rc2 spec work. (#99)Ben Marshall8-1/+956
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.
2021-09-09Merge pull request #103 from PeterRugg/fix-rounding-modesJessica Clarke2-177/+284
Fix crash when fcsr.frm is invalid
2021-08-22Fix incorrect SV48_Vaddr bitfielddylux1-1/+1
2021-08-09Fix crash when fcsr.frm is invalidPeter Rugg2-177/+284
2021-07-29Use headache to apply copyright header at request of Peter Sewell.Robert Norton76-0/+5166
2021-07-16Add an extension point to allow validation of physical memory accesses.Robert Norton3-3/+36
This is required for implementing memory version support for CHERI.
2021-06-29vmem_rvNN: allow shimming underneath effectivePrivilegeNathaniel Wesley Filardo2-6/+12
It's possible that we might want to do page table walks at Privilege levels other than the default value (e.g., under the explicit direction of the instruction stream). Split translateAddr into a thin wrapper of the same name and a new translateAddr_priv that takes the Privilege as an argument.