| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-09 | RISC-V: add missed c.ebreak instruction | Prashanth Mundkur | |
| 2018-11-08 | RISC-V: fix a typo-induced bug in updating the PTE. | Prashanth Mundkur | |
| 2018-11-07 | RISC-V: fix assembly mappings for lr/sc. | Prashanth Mundkur | |
| 2018-11-07 | Move inline forall in function definitions | Alasdair Armstrong | |
| * Previously we allowed the following bizarre syntax for a forall quantifier on a function: val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit this commit changes this to the more sane: val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit Having talked about it today, we could consider adding the syntax val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit which would avoid the forall (by implicitly quantifying variables in the constraint), and be slightly more friendly especially for documentation purposes. Only RISC-V used this syntax, so all uses of it there have been switched to the new style. * Second, there is a new (somewhat experimental) syntax for existentials, that is hopefully more readable and closer to minisail: val foo(x: int, y: int) -> int('m) with 'm >= 2 "type('n) with constraint" is equivalent to minisail: {'n: type | constraint} the type variables in typ are implicitly quantified, so this is equivalent to {'n, constraint. typ('n)} In order to make this syntax non-ambiguous we have to use == in constraints rather than =, but this is a good thing anyway because the previous situation where = was type level equality and == term level equality was confusing. Now all the type type-level and term-level operators can be consistent. However, to avoid breaking anything = is still allowed in non-with constraints, and produces a deprecated warning when parsed. | |||
| 2018-11-07 | RISC-V: add some consistency checks when run with spike. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: use stderr for terminal output in OCaml backend. | Prashanth Mundkur | |
| Also add a brief README for booting Linux on the C and OCaml backends. | |||
| 2018-10-23 | RISC-V: separate jalr execute clause for seq model and rmem. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Initial splitting of instructions across multiple files. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Allow the C platform to get the DTB from a file, so that OS boot is ↵ | Prashanth Mundkur | |
| possible without linking to Spike. When linked with Spike, ensure that the DTBs being used are identical. | |||
| 2018-10-23 | RISC-V: add cli option to dump the platform device-tree. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Add a platform knob to control mtval contents on illegal instruction ↵ | Prashanth Mundkur | |
| faults. | |||
| 2018-10-23 | RISC-V: various fixes | Prashanth Mundkur | |
| - add mstatus to cross-check - fix typo in assembly mapping for lr/sc | |||
| 2018-10-23 | RISC-V: fix: sstatus.SD depends on .XS and .FS. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: adjust main loop for the non-spike case. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: implement terminal output for C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: tick the clock in the C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Add device tree blob into rom, currently only when linked against spike. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: add default reset vector. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: fix up platform bits for lr/sc. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: set htif tohost port address using ELF symbol. | Prashanth Mundkur | |
| 2018-10-23 | Fix typo in plat_ram_size | Alasdair Armstrong | |
| 2018-10-23 | RISC-V: Add some debug logs for within_phys_mem. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Allow Spike linkage to be conditionally enabled. | Prashanth Mundkur | |
| 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 | 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-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 | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |