| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-23 | RISC-V: flush logs at each step. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Flesh out more of the tandem checks in the C platform simulator. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: An initial C Sail model linked against Spike for testing. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Refactor c platform bits. | Prashanth Mundkur | |
| 2018-10-22 | Coq: use function type more carefully in untupling | Brian Campbell | |
| And update the RISC-V patch accordingly. | |||
| 2018-10-22 | Update Coq patch for RISC-V, add string_take to Coq library | Brian Campbell | |
| 2018-10-16 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-10-16 | Re-implement space-related mapping functions in Sail rather than backends | Jon French | |
| Uses new primop 'string_take' which is much easier to implement in e.g. C | |||
| 2018-10-15 | Add interpreted RISC-V model to test suite | Jon French | |
| 2018-10-13 | Adapt checked_mem_read to have acquire/release/reserve arguments so | Christopher Pulte | |
| that this information propagates from the instruction definition to the memory accesses. Necessary for Promising RISC-V concurrency model. | |||
| 2018-10-05 | RISC-V: encode/decode and assembly mappings for compressed instructions | Jon French | |
| 2018-10-01 | Update Coq RISC-V patch now that the assembler is in good shape | Brian Campbell | |
| 2018-09-19 | Coq: track changes elsewhere | Brian Campbell | |
| - more hex_bits functions, add decimal_string_of_bits - extra tuple unfolding in constructors - note that variables can be redundant wildcard clauses - update RISC-V patch | |||
| 2018-09-19 | separate decimal_string_of_bits from string_of_bits | Jon French | |
| 2018-09-14 | More monomorphisations for hex_bits_N... | Jon French | |
| I got bored of this so I wrote a Python script to generate all of them between 1 and 33, plus 48 and 64. It's in a comment. We should really get around to making the typechecker work with polymorphic mappings... | |||
| 2018-09-14 | RISCV prelude: fix typo in ocaml extern for negate_* | Jon French | |
| 2018-09-14 | Sail_lib and RISCV prelude: functions for bitwise operations on ints | Jon French | |
| 2018-09-12 | Coq: update RISC-V patch | Brian Campbell | |
| 2018-09-10 | RISC-V: move the PC and minstret updates into the step function, to better ↵ | Prashanth Mundkur | |
| localize them, making loop() purely a platform function. | |||
| 2018-09-07 | RISCV: Run RISC-V tests using version compiled to C | Alasdair Armstrong | |
| Current pass rate is 170 out of 181. Looks like there are some issues with rv64ua-p-lrsc.elf, rv64ua-v-lrsc.elf, and rv64uc-p-rvc.elf which I think are caused by me not implementing parts of the RISC-V platform correctly in C. Some of the div and mod tests also fail, which is probably an issue with using the correct rounding. | |||
| 2018-09-06 | Coq: fill in a few more RISC-V axioms | Brian Campbell | |
| 2018-09-06 | Coq: fix up some barrier/memory definitions for RISC-V | Brian Campbell | |
| 2018-09-06 | RISCV: Get enough of the RISCV platform into C to run some tests | Alasdair Armstrong | |
| 2018-09-05 | Coq: fill in trivial ranges in constraint solver | Brian Campbell | |
| 2018-09-04 | C: Tweaks to RISC-V to get compiling to C | Alasdair Armstrong | |
| Revert a change to string_of_bits because it broke all the RISC-V tests in OCaml. string_of_int (int_of_string x) is not valid because x may not fit within an integer. | |||
| 2018-09-04 | Add a rewrite to minimise the number of functions marked as recursive | Brian Campbell | |
| Particularly useful when execute has been split up (e.g., on RISC-V). Only enabled on Coq for now. | |||
| 2018-09-03 | Coq: solver should split earlier | Brian Campbell | |
| otherwise some other parts don't work properly. Also update RISC-V patch. | |||
| 2018-09-03 | Coq: update RISC-V patch again | Brian Campbell | |
| 2018-09-03 | Coq: rework generation of dependent pairs so that they are only | Brian Campbell | |
| constructed when a function call, cast, or binder demands them, removing some ambiguous corner cases. Also - Don't simplify nexps before printing (note that we usually end up needing a (8 * x) / 8 lemma as a result) - More extraction of properties in the goal - Splitting of conditionals/matches in goals (which can occur more often because of the new positions of build_ex in definitions) - Try simple solving first to improve speed / reduce proof sizes / help fill in metavariables (because manipulating the goal can interfere with instantiating them) - Update RISC-V patch | |||
| 2018-08-31 | Some C stubs for platform bits for RISC-V. | Prashanth Mundkur | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |