aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_insts_base.sail
AgeCommit message (Collapse)AuthorFilesLines
2024-01-31Update bitfield syntaxAlasdair1-3/+3
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.
2023-11-29Fix Store-Conditional assembly operand order and add parensPaul A. Clarke1-2/+2
The operand order for Store-Conditional assembly has the second and third operands reversed. The RISC-V Instruction Set Manual states: > ``` > SC.W conditionally writes a word in rs2 to the address in rs1 [...] > If the SC.W succeeds, the instruction writes the word in rs2 to memory, > and it writes zero to rd. If the SC.W fails, the instruction does not > write to memory, and it writes a nonzero value to rd. > ``` `rd` is for the return code, `rs2` is the value, and `rs1` is the memory address. For the syntax `sc.w A,B,(C)`: - `A` is where the result is stored, per convention. So, this is `rd`. - `B` is the value to be stored. So, this is `rs2`. - `C` is the address at which to store the value. So, this is `rs1`. The resulting syntax would be `stc.w rd,rs2,(rs1)`. The current assembly representation is: ``` "sc." ^ size_mnemonic(size) [...] reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ``` Note that the order is wrong. In addition, parentheses are missing around `rs2`. Fix this instance, as well as two other instances where parentheses are missing. Fixes #338. Fixes #344. Suggested-by: Tim Hutt <timothy.hutt@codasip.com>
2023-10-25Remove duplicate shift definitionsTim Hutt1-42/+4
SHIFTW and SHIFTIWOP were duplicated. This did not cause any harm except that the disassembly for the SHIFTW version was incorrect. Therefore I removed that version. The `execute()` functions were identical but the SHIFTW version is slightly neater (only one `[31..0]`) so I applied that to the SHIFTIWOP version. This should cause no functional changes to the model except that the disassembly will have the extra `w` which is correct.
2023-10-11Implement menvcfgTim Hutt1-0/+17
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-09-12Remove effectsTim Hutt1-1/+1
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-08-01Rename EXTZ and EXTSAlasdair1-16/+16
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 Richardson1-1/+0
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 Tomsich1-1/+3
2023-03-14Use not() instead of ~() for boolean negation (#210)Alexander Richardson1-8/+8
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-06Add wildcard cases to matches to suppress Sail warnings. (#197)Robert Norton1-16/+19
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
2021-07-29Use headache to apply copyright header at request of Peter Sewell.Robert Norton1-0/+68
2021-02-02Reformat excessively-long linesScott Johnson1-2/+8
2021-01-27MRET and SRET should increment minstret when successfulScott Johnson1-8/+6
2020-10-15Store PC in mtval on EBREAK to match a spec update.Prashanth Mundkur1-1/+1
Fixes #70.
2020-09-22Handle empty predecessor or successor RW sets in FENCE as no-ops, as IO ↵Prashanth Mundkur1-2/+4
concurrency is not yet modelled. Thanks to Christopher Pulte.
2020-05-27Fix bug: mtval (and [su]tval) should get vaddr, not paddrScott Johnson1-2/+2
2020-05-27Rename var to distinguish vaddr from paddrScott Johnson1-16/+16
2020-05-27Rename param to distinguish vaddr from paddrScott Johnson1-2/+2
2020-04-01Set mtval to 0 on ebreak. Fixes #44.Prashanth Mundkur1-1/+1
2019-11-05Add a hook to allow extensions to veto xret. This will be used by CHERI ↵xret_extRobert Norton1-11/+14
extension. Note that illegal exception on mode check failure takes precedence over CHERI to allow for virtualisation.
2019-09-04Merge remote-tracking branch 'origin/master' into vmem_ext.vmem_extRobert Norton1-18/+18
2019-08-20Whitespace fixes to nuke tabs.no_castsPrashanth Mundkur1-6/+6
2019-08-19RISC-V spec, without implicit castsAlasdair Armstrong1-18/+18
2019-08-09Allow accumulation of information during page-table-walk for extensions.Prashanth Mundkur1-4/+4
2019-07-22Make a custom exception code available for extensions, and remove the ↵Prashanth Mundkur1-8/+8
E_CHERI code. Enable extensions for PTE checks and PTW errors, and propagate those into exception codes.
2019-07-22Merge branch 'master' into vmem_extPrashanth Mundkur1-1/+45
2019-07-19Merge branch 'master-cleanup'Prashanth Mundkur1-1/+1
2019-07-19Add a new pc access function to get the architectural PC: on CHERI this is ↵master-cleanupRobert Norton1-1/+1
not what is in the PC register because the architectural PC is the offset of PCC and the PC register stores the absolute PC (at present -- may review this decision in future). This allows fix for AUIPC and RVFI reported PC.
2019-07-18Make sure everything builds correctlyAlasdair Armstrong1-0/+44
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
2019-07-18Revert "Support DMB/DSB domains"Alasdair Armstrong1-11/+11
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.
2019-07-18Support DMB/DSB domainsShaked Flur1-11/+11
2019-07-15Allow extensions to types of memory access, and factor out PTE and PTW ↵Prashanth Mundkur1-8/+8
definitions.
2019-06-24Add PMP checks to physical memory accesses.Prashanth Mundkur1-9/+9
- 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
2019-06-24Narrow the external interface to riscv_mem to mem_{read,write,write_ea}.Prashanth Mundkur1-4/+4
2019-05-23Be more careful about matching only instructions that are defined for xlen ↵Robert Norton1-5/+6
being built.
2019-05-10Rename regbits to regidx, to clarify the type is an index and not the ↵Prashanth Mundkur1-15/+15
contents of a register.
2019-05-10Use an explicit enum to indicate the retire status as opposed to a boolean ↵Prashanth Mundkur1-42/+42
to improve clarity.
2019-05-10Print canonical assembly for immediate loads/storesJames Clarke1-3/+3
2019-05-03Minor formatting cleanup and remove obsolete comments.Prashanth Mundkur1-2/+0
2019-05-03Fix inconsistency in accessing PC/nextPC, which also clarifies which ↵Prashanth Mundkur1-4/+4
handlers return nextPC values as opposed to setting them.
2019-05-02Push address calculation inside the data_check_addr hook and rename it to ↵rmn30Robert Norton1-6/+8
data_get_addr. This avoids a double register read in CHERI case.
2019-05-01Add base address register as extra argument to ext_data_check_addr hook to ↵Robert Norton1-2/+2
assist with implementing CHERI capability mode.
2019-04-24Add extended model from cheri-merge.Prashanth Mundkur1-58/+88
2019-03-14Merge branch 'master' into rmem_interpreterJon French1-49/+103
2019-03-12refactor memory access to use new sail intrinsicsJon French1-11/+11
2019-03-12fix missing separator in shift instruction disassembliesJon French1-2/+2
2019-03-11Add tlbs for Sv32 and Sv48, and some fixes to sfence.vma.Prashanth Mundkur1-18/+10
- handle sfence.vma in machine-mode - flush both tlb39 and tlb48 in 64-bit mode
2019-03-11Fixes for Sv39 TLB.Prashanth Mundkur1-5/+10
- fix and simplify model initialization, to enable generic TLB initialization - re-enable sfence.vma
2019-03-04Minor edit for consistency.Prashanth Mundkur1-5/+5
2019-03-04Fix missed RV32 check for shamt in sll/srl.Prashanth Mundkur1-5/+13
generated by cgit v1.1 at 2024-10-12 22:47:27 +0000