| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-31 | riscv prelude: yet more manual monomorphisations for hex_bits | Jon French | |
| 2018-08-30 | Annotate the RISC-V prelude for C builtins. | Prashanth Mundkur | |
| Add some builtins to the C sail lib. Enable some gcc warnings. | |||
| 2018-08-30 | Add a C header containing declarations needed by RISC-V. | Prashanth Mundkur | |
| 2018-08-29 | C: Fix some issues with tuples as arguments to polymorphic constructors | Alasdair Armstrong | |
| Now all we need to do is make sure the RISC-V builtins are mapped to the correct C functions, and RISC-V in C should work (hopefully). We're still missing some of the functions in sail.c for the mappings so those have to be implemented. | |||
| 2018-08-29 | Updated snapshots for Isabelle 2018 | Thomas Bauereiss | |
| 2018-08-28 | Adapt theory imports for Isabelle 2018 | Thomas Bauereiss | |
| Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860 | |||
| 2018-08-28 | fix bug in RISCV assembly mapping, incorrect order of FENCE pred/succ bits | Jon French | |
| 2018-08-16 | Add the type an expression was checked against to tannots, and use for Coq | Brian Campbell | |
| Tweak extra Coq files to match. Tweak early return rewrite to use declared return type, which can always be put into an E_cast. | |||
| 2018-08-15 | Temporary fix for RISC-V Lem generation | Brian Campbell | |
| 2018-08-15 | Get RISC-V on Coq into reasonable state to show | Brian Campbell | |
| - Fill in Coq builtins for more of the RISC-V prelude - Update Barriers - More general autocast - Temporary sub_nat definition (until the backend handles nat better) - Patch to bring results into a reasonable state - Use Let rather than Definition for non-dependent top-level values | |||
| 2018-08-13 | More RISC-V built-in type constraints | Brian Campbell | |
| 2018-08-13 | Coq: more strings for RISC-V | Brian Campbell | |
| 2018-08-13 | Add constraints to RISC-V duopod, makefile rules | Brian Campbell | |
| 2018-08-13 | RISC-V: mult_range is ill-typed, use mult_atom instead | Brian Campbell | |
| 2018-08-13 | Basic Coq support for RISC-V | Brian Campbell | |
| Note that constraints have been added to ensure that all bitvector types are inhabited. | |||
| 2018-07-27 | Add some missing rv64i instructions, discovered when annotating the riscv ↵ | Prashanth Mundkur | |
| isa spec. | |||
| 2018-07-27 | Add a riscv latex target. | Prashanth Mundkur | |
| 2018-07-20 | Add assorted comments, consistency fixes and cleanup. | Prashanth Mundkur | |
| 2018-07-12 | Fixed a nested comment issue | Shaked Flur | |
| 2018-07-11 | Add fixme note about riscv jalr. | Prashanth Mundkur | |
| 2018-07-11 | Update the exception code for riscv LR after clarification on isa-dev. | Prashanth Mundkur | |
| 2018-07-11 | RISC-V model fixes for RMEM | Jon French | |
| 2018-07-11 | Fix riscv_duopod build. | Robert Norton | |
| 2018-07-10 | Add an option to specify the dtc to use for the riscv platform. | Prashanth Mundkur | |
| 2018-07-10 | Turn off some riscv debug tracing. | Prashanth Mundkur | |
| 2018-07-10 | Start adding c-backend bits for riscv. | Prashanth Mundkur | |
| 2018-07-10 | Support riscv atomic accesses to mmio regions, used by linux to access ↵ | Prashanth Mundkur | |
| device registers. | |||
| 2018-07-10 | Make HOL build properly again for all of the models | Brian Campbell | |
| 2018-07-10 | RISCV load-acquire in Lem (-> rmem) | Jon French | |
| 2018-07-10 | correct pretty-printing using mappings | Jon French | |
| 2018-07-10 | disable printing when compiling to Lem to keep rmem happy | Jon French | |
| 2018-07-09 | Log some timing info at the end of riscv execution. | Prashanth Mundkur | |
| 2018-07-09 | add riscv_analysis.sail to SAIL_SRCS | Jon French | |
| 2018-07-09 | add LOADRES, STORECON, AMO to analysis | Jon French | |
| 2018-07-09 | Support writes to misa.C in riscv. | Prashanth Mundkur | |
| 2018-07-08 | Make the riscv fetch-execute loop return instead of exiting when done. | Prashanth Mundkur | |
| 2018-07-08 | Move the riscv analysis function into its own file for coverage purposes. | Prashanth Mundkur | |
| 2018-07-08 | Add a riscv coverage target using bisect-ppx. | Prashanth Mundkur | |
| 2018-07-07 | Add reservation traces to riscv tracecmp tool. | Prashanth Mundkur | |
| 2018-07-07 | Cancel riscv reservation before i/o scheduling, tweak reservation tracing. | Prashanth Mundkur | |
| 2018-07-07 | An initial fix to riscv lr/sc, needs a review. | Prashanth Mundkur | |
| This uses a stronger model than the version in Sail-1 in order to perform address alignment checks. The reservation is kept on virtual addresses, and maintained in the platform model, but now the lr/sc definitions need calls to externs to update this state. An alternative was to reserve physical addresses, but that appeared to be more complicated without a lot more changes. Ideally, the model should be parameterizable over both options. | |||
| 2018-07-07 | Add some tracing to riscv address translation. | Prashanth Mundkur | |
| 2018-07-05 | Fix printing of aq/rl flags in risc-v lr/sc. | Prashanth Mundkur | |
| 2018-07-05 | support acquire/release loads/stores in RISCV initial_analysis | Jon French | |
| 2018-07-05 | print to stdout not stderr to stop upsetting rmem regression tests | Jon French | |
| 2018-07-05 | restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵ | Jon French | |
| cleanly | |||
| 2018-07-03 | Add htif tohost to the riscv tracecmp tool. | Prashanth Mundkur | |
| 2018-07-03 | Allow the riscv htif_tohost mmio port to be readable, and ack writes to that ↵ | Prashanth Mundkur | |
| port. | |||
| 2018-06-28 | further changes to support rmem | Jon French | |
| 2018-06-26 | Fix duplicate riscv mem-ea, spotted by Jon French. | Prashanth Mundkur | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |