Age | Commit message (Collapse) | Author | Files | Lines | |
---|---|---|---|---|---|
2019-11-05 | Add extension point for checking CSR access.csr_ext | Robert Norton | 2 | -0/+17 | |
2019-11-05 | Add a hook to allow extensions to veto xret. This will be used by CHERI ↵xret_ext | Robert Norton | 3 | -11/+21 | |
extension. Note that illegal exception on mode check failure takes precedence over CHERI to allow for virtualisation. | |||||
2019-10-31 | Add convenience targets for c emulator and rvfi. | Robert Norton | 1 | -0/+6 | |
2019-10-13 | paste in pointers to the Sail-enabled versions of the RISC-V spec | pes20 | 1 | -0/+7 | |
2019-09-18 | Update docs on extension support for disabling RVC. | Prashanth Mundkur | 1 | -0/+6 | |
2019-09-18 | Add a hook for extensions to supress writes to misa.C if necessary. | Robert Norton | 3 | -3/+10 | |
2019-09-18 | Squashed commit of various patches from @scottj97: | Prashanth Mundkur | 2 | -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-18 | Merge pull request #19 from scottj97/upstream-2 | Robert Norton | 1 | -1/+3 | |
Run Sail with -dno_cast even when it comes from opam package | |||||
2019-09-18 | Merge pull request #18 from scottj97/upstream-1 | Robert Norton | 1 | -1/+19 | |
Expand getopt_long option string to multiple lines | |||||
2019-09-17 | Run Sail with -dno_cast even when it comes from opam package | Scott Johnson | 1 | -1/+3 | |
2019-09-17 | Expand getopt_long option string to multiple lines | Scott Johnson | 1 | -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-12 | tweak README | Peter Sewell | 1 | -38/+26 | |
2019-09-12 | tweak Status page | Peter Sewell | 1 | -7/+6 | |
2019-09-12 | update funding ack | Peter Sewell | 235 | -1285/+311246 | |
2019-09-11 | Update the svg figs. | Prashanth Mundkur | 2 | -55/+63 | |
2019-09-11 | Update the docs for the virtual memory and exception-code extensions. | Prashanth Mundkur | 3 | -14/+28 | |
2019-09-11 | Add a brief status doc page. | Prashanth Mundkur | 2 | -1/+61 | |
2019-09-10 | Refactor CSR code to use scattered functions / mappings for ease of extension. | Robert Norton | 4 | -240/+151 | |
2019-09-10 | Call ext_fetch_check_pc for rvfi fetch as for normal fetch. | Robert Norton | 1 | -19/+31 | |
2019-09-10 | Changes from Peter Rugg to make misa.C only writable if enabled at boot by ↵ | Robert Norton | 1 | -3/+5 | |
sys_enable_rvc. | |||||
2019-09-06 | Fix rvfi build for cast free prelude. | Robert Norton | 1 | -2/+2 | |
2019-09-04 | Merge remote-tracking branch 'origin/master' into vmem_ext.vmem_ext | Robert Norton | 184 | -276/+308615 | |
2019-08-20 | Whitespace fixes to nuke tabs.no_casts | Prashanth Mundkur | 7 | -15/+15 | |
2019-08-19 | RISC-V spec, without implicit casts | Alasdair Armstrong | 24 | -254/+261 | |
2019-08-14 | Update Coq snapshots | Brian Campbell | 23 | -2543/+6122 | |
2019-08-13 | Fix Coq duopod build by giving missing termination measure | Brian Campbell | 2 | -1/+2 | |
2019-08-13 | Update barriers in Coq. | Brian Campbell | 1 | -11/+11 | |
2019-08-09 | Allow accumulation of information during page-table-walk for extensions. | Prashanth Mundkur | 13 | -138/+150 | |
2019-08-05 | Add some effects to execute function declarationand remove val specs for ↵ | Robert Norton | 3 | -8/+4 | |
calling functions to allow effects to be inferred. | |||||
2019-07-26 | Fix HOL4 snapshot for recent versions of HOL4 | Thomas Bauereiss | 2 | -4/+2 | |
Also fix "clean" target in Holmakefile | |||||
2019-07-25 | Update directory map in readme. | Prashanth Mundkur | 1 | -0/+2 | |
2019-07-25 | Add snapshots of theorem prover definitions | Thomas Bauereiss | 148 | -0/+304756 | |
2019-07-23 | Fix compile error in cheri mode. | Prashanth Mundkur | 1 | -1/+1 | |
2019-07-22 | Make a custom exception code available for extensions, and remove the ↵ | Prashanth Mundkur | 15 | -242/+320 | |
E_CHERI code. Enable extensions for PTE checks and PTW errors, and propagate those into exception codes. | |||||
2019-07-22 | Merge branch 'master' into vmem_ext | Prashanth Mundkur | 13 | -61/+518 | |
2019-07-19 | Remove cheri-specific comment. | Prashanth Mundkur | 1 | -1/+0 | |
2019-07-19 | Merge branch 'master-cleanup' | Prashanth Mundkur | 9 | -11/+215 | |
2019-07-19 | Add a new pc access function to get the architectural PC: on CHERI this is ↵master-cleanup | Robert Norton | 4 | -3/+12 | |
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-19 | Fixed two typos | Shaked Flur | 1 | -1/+1 | |
2019-07-18 | More tweaks to reading guide and diagram. | Prashanth Mundkur | 3 | -31/+36 | |
2019-07-18 | Minor tweaks. | Prashanth Mundkur | 1 | -4/+7 | |
2019-07-18 | Add info about the C emulator to the reading guide. | Prashanth Mundkur | 4 | -6/+186 | |
2019-07-18 | Make sure everything builds correctly | Alasdair Armstrong | 5 | -49/+303 | |
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-18 | Revert "Support DMB/DSB domains" | Alasdair Armstrong | 4 | -44/+44 | |
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-18 | Support DMB/DSB domains | Shaked Flur | 4 | -44/+44 | |
2019-07-17 | Disable mmio devices (clint and htif interfaces) when using RVFI to prevent ↵ | Robert Norton | 1 | -1/+8 | |
divergence when using TestRIG. | |||||
2019-07-16 | Use reserved bits in PTEs for vmem extensions on RV64, as allowed by the ↵ | Prashanth Mundkur | 7 | -32/+49 | |
spec. This is not possible for RV32, so pass zeros there. | |||||
2019-07-15 | Allow extensions to types of memory access, and factor out PTE and PTW ↵ | Prashanth Mundkur | 15 | -168/+178 | |
definitions. | |||||
2019-07-11 | Merge branch 'master-cleanup' | Prashanth Mundkur | 17 | -355/+419 | |
2019-07-11 | Tweak fig. | Prashanth Mundkur | 2 | -10/+12 | |