aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)AuthorFilesLines
2020-01-07Fix parsing long options in the C emulator for RVFI-DIIJames Clarke1-3/+3
idx, passed as longindex to getopt_long, is updated every time a long option is parsed to be the index of that option in the options array, not argv. We should instead use optind as in the non-RVFI-DII case, and we can remove the variable to avoid confusion since it is unused.
2020-01-07Separate out RVFI simulators like non-RVFIJames Clarke1-4/+4
2020-01-07Merge pull request #22 from rems-project/rvfi_fixRobert Norton1-35/+29
Attempt to fix RVFI for instruction fetch exceptions.
2020-01-06Merge pull request #30 from jrtc27/amo-faultPrashanth Mundkur3-14/+30
Generate correct cause for AMO faults
2020-01-02improve pppes201-1/+1
2020-01-01add location and type info to pp-rawpes201-1/+1
2020-01-01pp tinkering - update snapshotpes201-1/+1
2019-12-31snapshot of experimental Ott-generated Sail internal ASTpes201-0/+1
2019-12-23Remove hard-coded E_Fetch_Access_Fault now mem_read checks the typeJames Clarke1-2/+2
2019-12-23Generate correct cause for AMO faultsJames Clarke2-12/+28
2019-12-05Fix RVFI buildThomas Bauereiss1-1/+1
2019-12-03Merge branch 'mem_meta_merge'Robert Norton14-72/+148
2019-12-03Merge remote-tracking branch 'origin/master' into mem_meta_mergeRobert Norton9-17/+60
2019-11-28Fix check for BBV_DIRThomas Bauereiss1-1/+1
2019-11-26Fix RV32 Coq buildThomas Bauereiss2-5/+5
2019-11-26Tweak base case of PTW functionsThomas Bauereiss3-12/+12
Make termination of the page table walk functions provable unconditionally in Isabelle by catching the case when "level" becomes negative. On the Sail level, this case cannot occur, because "level" has type "nat", but we currently don't automatically carry over the non-negativity constraint of the Sail type "nat" into Isabelle.
2019-11-25Work around Isabelle problem in PTW functionsThomas Bauereiss1-0/+1
The standard pattern completeness proof for recursive functions generated by Lem for Isabelle seems to get confused in some situations when there are variables with unit type (in particular the ext_ptw argument of the page table walk functions). Solving this properly requires some more digging into the Isabelle simplifier, but the ad-hoc workaround in this commit fixes the problem for now.
2019-11-25Fix RV32 Lem buildThomas Bauereiss4-7/+7
2019-11-21Bump opam version.0.4Robert Norton1-1/+1
2019-11-13Fix amo assembly mapping, fixes #26.Prashanth Mundkur1-1/+1
2019-11-05Merge pull request #24 from rems-project/csr_extPrashanth Mundkur6-11/+44
Extension hooks for CSR access control
2019-11-05Add extension point for checking CSR access.csr_extRobert Norton2-0/+17
2019-11-05Add a hook to allow extensions to veto xret. This will be used by CHERI ↵xret_extRobert Norton3-11/+21
extension. Note that illegal exception on mode check failure takes precedence over CHERI to allow for virtualisation.
2019-11-01Fix up riscv_duopod and make self containedAlasdair Armstrong2-5/+7
2019-10-31Add convenience targets for c emulator and rvfi.Robert Norton1-0/+6
2019-10-29Attempt to fix RVFI for instruction fetch exceptions. Not sure what ↵Robert Norton1-35/+29
'need_instr' was intended to do but does not seem to be what we want.
2019-10-13paste in pointers to the Sail-enabled versions of the RISC-V specpes201-0/+7
2019-10-09Add {read,write}_ram for CoqThomas Bauereiss3-7/+19
2019-10-09Read/write memory values and metadata together atomicallyThomas Bauereiss10-52/+114
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.
2019-09-18Update docs on extension support for disabling RVC.Prashanth Mundkur1-0/+6
2019-09-18Add a hook for extensions to supress writes to misa.C if necessary.Robert Norton3-3/+10
2019-09-18Squashed commit of various patches from @scottj97:Prashanth Mundkur2-64/+64
Rename var to make it clear it is physical and not virtual. There are a lot of variables in riscv_mem.sail and riscv_platform.sail named addr and it's not always clear if that is physical or virtual address. These changes rename those variables to paddr to reduce ambiguity.
2019-09-18Merge pull request #19 from scottj97/upstream-2Robert Norton1-1/+3
Run Sail with -dno_cast even when it comes from opam package
2019-09-18Merge pull request #18 from scottj97/upstream-1Robert Norton1-1/+19
Expand getopt_long option string to multiple lines
2019-09-17Run Sail with -dno_cast even when it comes from opam packageScott Johnson1-1/+3
2019-09-17Expand getopt_long option string to multiple linesScott Johnson1-1/+19
This will make future diffs easier to read and merge, since adding and removing options will show up as entire lines that change instead of a few characters in the middle of the line.
2019-09-12tweak READMEPeter Sewell1-38/+26
2019-09-12tweak Status pagePeter Sewell1-7/+6
2019-09-12update funding ackPeter Sewell235-1285/+311246
2019-09-11Update the svg figs.Prashanth Mundkur2-55/+63
2019-09-11Update the docs for the virtual memory and exception-code extensions.Prashanth Mundkur3-14/+28
2019-09-11Add a brief status doc page.Prashanth Mundkur2-1/+61
2019-09-10Refactor CSR code to use scattered functions / mappings for ease of extension.Robert Norton4-240/+151
2019-09-10Call ext_fetch_check_pc for rvfi fetch as for normal fetch.Robert Norton1-19/+31
2019-09-10Changes from Peter Rugg to make misa.C only writable if enabled at boot by ↵Robert Norton1-3/+5
sys_enable_rvc.
2019-09-06Fix rvfi build for cast free prelude.Robert Norton1-2/+2
2019-09-04Merge remote-tracking branch 'origin/master' into vmem_ext.vmem_extRobert Norton184-276/+308615
2019-08-20Whitespace fixes to nuke tabs.no_castsPrashanth Mundkur7-15/+15
2019-08-19RISC-V spec, without implicit castsAlasdair Armstrong24-254/+261
2019-08-14Update Coq snapshotsBrian Campbell23-2543/+6122
generated by cgit v1.1 at 2024-09-27 16:12:17 +0000