| Age | Commit message (Collapse) | Author | Files | Lines | |
|---|---|---|---|---|---|
| 2019-11-26 | Fix RV32 Coq build | Thomas Bauereiss | 1 | -4/+4 | |
| 2019-11-25 | Fix RV32 Lem build | Thomas Bauereiss | 2 | -4/+4 | |
| 2019-10-09 | Add {read,write}_ram for Coq | Thomas Bauereiss | 1 | -0/+11 | |
| 2019-10-09 | Read/write memory values and metadata together atomically | Thomas Bauereiss | 2 | -0/+32 | |
| 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-08-13 | Update barriers in Coq. | Brian Campbell | 1 | -11/+11 | |
| 2019-07-18 | Make sure everything builds correctly | Alasdair Armstrong | 2 | -45/+79 | |
| 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 | 2 | -22/+22 | |
| 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 | 2 | -22/+22 | |
| 2019-06-24 | Add PMP checks to physical memory accesses. | Prashanth Mundkur | 2 | -0/+8 | |
| - 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-04-25 | Fix coq build. | Prashanth Mundkur | 1 | -19/+19 | |
| 2019-04-25 | riscv_extras.lem: update read/write_mem calls with (dummy) addrsize argument | Jon French | 1 | -18/+18 | |
| 2019-04-10 | Update Coq memory interfaces | Brian Campbell | 1 | -20/+27 | |
| (requires recent changes to the Coq library) | |||||
| 2019-04-04 | Add `sys_enable_writable_misa` and `sys_enable_rvc` to Coq extras file | Brian Campbell | 1 | -0/+3 | |
| 2019-04-03 | Tweak print_* bindings for Lem | Thomas Bauereiss | 2 | -0/+6 | |
| Map to a function that does not actuaylly output anything, in order to not confuse rmem. | |||||
| 2019-04-01 | Add missed lem definitions for sys misa/rvcflags. | Prashanth Mundkur | 2 | -0/+16 | |
| 2019-02-26 | Restore riscv_extras damaged by merge. | Prashanth Mundkur | 1 | -9/+13 | |
| 2019-02-13 | Make repository have shape RMEM expects | Alasdair Armstrong | 4 | -3/+140 | |
| 2019-02-13 | Switch version of riscv_extras.lem depending on Sail version | Alasdair Armstrong | 1 | -0/+137 | |
| Works around change to write_mem function signature in monad embedding | |||||
| 2019-01-22 | Add build Makefile targets for prover backends | Thomas Bauereiss | 1 | -4/+6 | |
| 2019-01-21 | Output auxiliary Isabelle theories into generated_definitions/isabelle | Thomas Bauereiss | 1 | -2/+2 | |
| Also copy ROOT file into the same directory | |||||
| 2019-01-19 | Moved gen/ to handwritten_support/hgen | Shaked Flur | 19 | -0/+1367 | |
| 2019-01-16 | More reorg. | Prashanth Mundkur | 5 | -0/+439 | |
| . move prover files into a single support directory . generated_models -> generated_definitions . reset vector -> c_emulator | |||||
 |
index : sail-riscv.git | |
| Unnamed repository; edit this file 'description' to name the repository. | root |
| aboutsummaryrefslogtreecommitdiff |
path: root/handwritten_support