summaryrefslogtreecommitdiff
path: root/riscv
AgeCommit message (Expand)Author
2018-09-19separate decimal_string_of_bits from string_of_bitsJon French
2018-09-14More monomorphisations for hex_bits_N...Jon French
2018-09-14RISCV prelude: fix typo in ocaml extern for negate_*Jon French
2018-09-14Sail_lib and RISCV prelude: functions for bitwise operations on intsJon French
2018-09-12Coq: update RISC-V patchBrian Campbell
2018-09-10RISC-V: move the PC and minstret updates into the step function, to better lo...Prashanth Mundkur
2018-09-07RISCV: Run RISC-V tests using version compiled to CAlasdair Armstrong
2018-09-06Coq: fill in a few more RISC-V axiomsBrian Campbell
2018-09-06Coq: fix up some barrier/memory definitions for RISC-VBrian Campbell
2018-09-06RISCV: Get enough of the RISCV platform into C to run some testsAlasdair Armstrong
2018-09-05Coq: fill in trivial ranges in constraint solverBrian Campbell
2018-09-04C: Tweaks to RISC-V to get compiling to CAlasdair Armstrong
2018-09-04Add a rewrite to minimise the number of functions marked as recursiveBrian Campbell
2018-09-03Coq: solver should split earlierBrian Campbell
2018-09-03Coq: update RISC-V patch againBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-31Some C stubs for platform bits for RISC-V.Prashanth Mundkur
2018-08-31riscv prelude: yet more manual monomorphisations for hex_bitsJon French
2018-08-30Annotate the RISC-V prelude for C builtins.Prashanth Mundkur
2018-08-30Add a C header containing declarations needed by RISC-V.Prashanth Mundkur
2018-08-29C: Fix some issues with tuples as arguments to polymorphic constructorsAlasdair Armstrong
2018-08-29Updated snapshots for Isabelle 2018Thomas Bauereiss
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
2018-08-28fix bug in RISCV assembly mapping, incorrect order of FENCE pred/succ bitsJon French
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-15Temporary fix for RISC-V Lem generationBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-08-13More RISC-V built-in type constraintsBrian Campbell
2018-08-13Coq: more strings for RISC-VBrian Campbell
2018-08-13Add constraints to RISC-V duopod, makefile rulesBrian Campbell
2018-08-13RISC-V: mult_range is ill-typed, use mult_atom insteadBrian Campbell
2018-08-13Basic Coq support for RISC-VBrian Campbell
2018-07-27Add some missing rv64i instructions, discovered when annotating the riscv isa...Prashanth Mundkur
2018-07-27Add a riscv latex target.Prashanth Mundkur
2018-07-20Add assorted comments, consistency fixes and cleanup.Prashanth Mundkur
2018-07-12Fixed a nested comment issueShaked Flur
2018-07-11Add fixme note about riscv jalr.Prashanth Mundkur
2018-07-11Update the exception code for riscv LR after clarification on isa-dev.Prashanth Mundkur
2018-07-11RISC-V model fixes for RMEMJon French
2018-07-11Fix riscv_duopod build.Robert Norton
2018-07-10Add an option to specify the dtc to use for the riscv platform.Prashanth Mundkur
2018-07-10Turn off some riscv debug tracing.Prashanth Mundkur
2018-07-10Start adding c-backend bits for riscv.Prashanth Mundkur
2018-07-10Support riscv atomic accesses to mmio regions, used by linux to access device...Prashanth Mundkur
2018-07-10Make HOL build properly again for all of the modelsBrian Campbell
2018-07-10RISCV load-acquire in Lem (-> rmem)Jon French
2018-07-10correct pretty-printing using mappingsJon French
2018-07-10disable printing when compiling to Lem to keep rmem happyJon French
2018-07-09Log some timing info at the end of riscv execution.Prashanth Mundkur
2018-07-09add riscv_analysis.sail to SAIL_SRCSJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:38:56 +0000