aboutsummaryrefslogtreecommitdiff
path: root/handwritten_support
AgeCommit message (Expand)AuthorFilesLines
2019-11-26Fix RV32 Coq buildThomas Bauereiss1-4/+4
2019-11-25Fix RV32 Lem buildThomas Bauereiss2-4/+4
2019-10-09Add {read,write}_ram for CoqThomas Bauereiss1-0/+11
2019-10-09Read/write memory values and metadata together atomicallyThomas Bauereiss2-0/+32
2019-08-13Update barriers in Coq.Brian Campbell1-11/+11
2019-07-18Make sure everything builds correctlyAlasdair Armstrong2-45/+79
2019-07-18Revert "Support DMB/DSB domains"Alasdair Armstrong2-22/+22
2019-07-18Support DMB/DSB domainsShaked Flur2-22/+22
2019-06-24Add PMP checks to physical memory accesses.Prashanth Mundkur2-0/+8
2019-04-25Fix coq build.Prashanth Mundkur1-19/+19
2019-04-25riscv_extras.lem: update read/write_mem calls with (dummy) addrsize argumentJon French1-18/+18
2019-04-10Update Coq memory interfacesBrian Campbell1-20/+27
2019-04-04Add `sys_enable_writable_misa` and `sys_enable_rvc` to Coq extras fileBrian Campbell1-0/+3
2019-04-03Tweak print_* bindings for LemThomas Bauereiss2-0/+6
2019-04-01Add missed lem definitions for sys misa/rvcflags.Prashanth Mundkur2-0/+16
2019-02-26Restore riscv_extras damaged by merge.Prashanth Mundkur1-9/+13
2019-02-13Make repository have shape RMEM expectsAlasdair Armstrong4-3/+140
2019-02-13Switch version of riscv_extras.lem depending on Sail versionAlasdair Armstrong1-0/+137
2019-01-22Add build Makefile targets for prover backendsThomas Bauereiss1-4/+6
2019-01-21Output auxiliary Isabelle theories into generated_definitions/isabelleThomas Bauereiss1-2/+2
2019-01-19Moved gen/ to handwritten_support/hgenShaked Flur19-0/+1367
2019-01-16More reorg.Prashanth Mundkur5-0/+439
generated by cgit v1.1 at 2024-07-17 22:32:37 +0000