aboutsummaryrefslogtreecommitdiff
path: root/handwritten_support
AgeCommit message (Expand)AuthorFilesLines
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-04-07Switch floating-point comparisons to using softfloat to avoid missed corner-c...Prashanth Mundkur2-0/+32
2020-01-23Add lem stubs for softfloat externs.rsnikhilPrashanth Mundkur2-0/+218
2020-01-22Some fixes for lem build.Prashanth Mundkur2-0/+8
2020-01-22Fix coq build.Prashanth Mundkur1-0/+1
2020-01-17Update handwritten Coq to use boolean predicatesBrian Campbell2-11/+13
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-08-16 23:24:50 +0000