aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)AuthorFilesLines
2021-06-18Add an extension point to allow validation of physical memory accesses.ext_check_phys_memRobert Norton3-3/+36
This is required for implementing memory version support for CHERI.
2020-08-04Add a line pointing to the instructions for latex inclusion in the prose ↵Prashanth Mundkur1-0/+1
specifications.
2020-08-04Add a pointer in README to riscv-config PRRobert Norton1-0/+4
2020-08-01Fix readme link.Prashanth Mundkur1-1/+1
2020-08-01update README and LICENCEpes202-11/+26
2020-08-01update READMEpes201-1/+1
2020-08-01update READMEpes201-2/+5
2020-08-01update READMEpes201-131/+129
2020-08-01Update README.mdPeter Sewell1-1/+1
2020-08-01update README, copying and adapting material from Formal Spec pagepes201-7/+227
2020-06-30Merge pull request #64 from nwf:pte-check-split with minor edits.Prashanth Mundkur6-19/+46
Split ext_ptw into pieces and add documentation
2020-06-30Split ext_ptw into pieces and add documentationNathaniel Wesley Filardo6-19/+43
It was somewhat annoying that CHERI would have had to track both successful and erroneous occurrences within the same type. Break the failures out to their own form and, while here, attempt to write down my understanding of the extension's information flow through vmem.
2020-06-30SV32: allow external specification of PTE extension bitsNathaniel Wesley Filardo2-1/+12
Just because they're not present in the SV32 PTE doesn't mean that models necessarily need to interpret them as zeros; any constant will do just fine. This allows extensions (like CHERI) that have both RV32 and RV64 versions to define more standard idiomatic interpretation to the bits within the PTE extension field.
2020-06-29Merge pull request #63 from nwf/split-eat-rwPrashanth Mundkur6-31/+37
A kinder, gentler splitting of ext_access_type's ReadWrite
2020-06-27A kinder, gentler splitting of ext_access_type's ReadWriteNathaniel Wesley Filardo6-31/+37
This redoes https://github.com/rems-project/sail-riscv/pull/57 without nearly as much excitement. We sill want it for CHERI, so that we can signal from the instruction to the PTW whether we are prepared to load a capability (or will strip any tags that we load) and whether the store will (or might) set a tag. Thanks to Prashanth Mundkur for several improvements.
2020-06-22Add some comments and docs.Prashanth Mundkur2-1/+9
2020-06-20Allow extensions to override page fault causesJessica Clarke4-5/+8
Otherwise there's no use for PTW_Ext_Error. This is required for sail-cheri-riscv to be able to make use of its own page table exceptions. The alternative to this is to pass the ext_ptw to translationException, but given PTW_Ext_Error exists it seems this was the intended way, and aligns with how access faults vs page faults are distinguished.
2020-06-20Fix non-coverage buildJessica Clarke1-0/+2
2020-06-18Update Coq snapshotsBrian Campbell35-85390/+98033
2020-06-18Make duopod build in coq again, and fix locationBrian Campbell1-5/+5
2020-06-18add Nikhil to authors; update install instructionspes202-5/+5
2020-06-17check error status returns from makeeroom19661-4/+14
2020-06-16Use an output file for generated branch information in the coverage build.Prashanth Mundkur1-2/+3
2020-06-15Remove obsolete Coq axiomBrian Campbell1-2/+0
2020-06-15Update handwritten Coq support files to match current Sail.Brian Campbell2-10/+4
2020-06-15Update Coq part of the Makefile to use opam packages by defaultBrian Campbell1-5/+28
2020-06-15Release version 0.50.5Thibaut Pérami1-1/+1
2020-06-15c emulator makefile tweak, as suggested by ThibautChristopher Pulte1-1/+1
2020-06-10Enable sailcov support in c_emulator if SAILCOV is set in the environment.Prashanth Mundkur2-1/+19
2020-06-09Properly handle invalid virtual addresses in address translation.Prashanth Mundkur2-6/+28
Fixes #58.
2020-06-05Avoid relying on ext_access_type values in PMP, to be compatible with ↵Prashanth Mundkur1-8/+8
extensions.
2020-06-04- upgrade to opam 2 packageChristopher Pulte4-6/+10
- make opam package include files required for building rmem
2020-05-28Remove effects on assembly introduced in 1bb74ef9, fix effects on ↵Prashanth Mundkur4-18/+18
encdec_compressed.
2020-05-28Merge pull request #54 from scottj97/fix-mtvalPrashanth Mundkur1-18/+18
Fix mtval when store gets bad PMP
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-05-26Fix FMIN/FMAX when QNaN+SNaN (#53)Scott Johnson2-40/+33
* New functions to simplify float NaN detection * Remove unnecessary intermediate values Now that we have simpler function f_is_NaN * FMIN/FMAX should return canonical NaN if both operands are NaN Fixes #52. * Simplify logic for FMIN/FMAX Spec says "If only one operand is a NaN, the result is the non-NaN operand." So no need to distinguish SNaN from QNaN here.
2020-05-22Add compressed F,D instructions.Prashanth Mundkur4-4/+166
Fixes #51.
2020-05-22Prevent access to N-mode registers and mstatus/mip/mie bits when N-mode is ↵Prashanth Mundkur2-12/+16
disabled. Fixes #50.
2020-05-22Add a Makefile target for new Sail->C backendAlasdair2-0/+35
2020-04-28Update status doc to mention xlen handling limitations.Prashanth Mundkur1-0/+4
2020-04-27Clear mstatus.mprv on mret and sret, and hardwire it to 0 when user-mode is ↵Prashanth Mundkur2-2/+6
not supported.
2020-04-27Add the mcountinhibit register.Prashanth Mundkur3-1/+19
2020-04-27Handle writes to misa.{F,D}.Prashanth Mundkur1-3/+8
2020-04-21Fix mstatus.MPRV fetches (#48)Scott Johnson4-14/+11
* Add {} so I can add a new variable here next * Create new variable which I will soon reuse * Plumb in the access type to effectivePrivilege So I can use it to fix #47 next. * Instruction fetches should not be affected by mstatus.MPRV Fixes #47. * Remove now-redundant privilege calculation
2020-04-14Update pointers to the Sail-annotated specifications, and update model ↵Prashanth Mundkur2-5/+6
status for F/D.
2020-04-07Switch floating-point comparisons to using softfloat to avoid missed ↵Prashanth Mundkur8-55/+199
corner-cases in hand-rolled helpers.
2020-04-06Fix fcsr exception accrual for non-softfloat paths.Prashanth Mundkur3-103/+92
2020-04-02Fix a bug in the softfloat interface that caused exception flags not to get ↵Prashanth Mundkur5-17/+19
accrued into fcsr.
generated by cgit v1.1 at 2024-07-17 07:13:55 +0000