| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-07-31 | More cleanup | Alasdair | |
| 2018-12-28 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-12-20 | RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ↵ | Robert Norton | |
| and tests. | |||
| 2018-12-13 | Add hooks to call cgen stub file for RISC-V | Alasdair Armstrong | |
| 2018-12-11 | Fix all tests with type checking changes | Alasdair Armstrong | |
| 2018-11-30 | RISC-V: update the riscv/readme to point to the new repository. | Prashanth Mundkur | |
| 2018-11-29 | RISC-V: more tidying up of the Spike interface. | Prashanth Mundkur | |
| 2018-11-29 | RISC-V: implement WFI in the platform model. | Prashanth Mundkur | |
| The initial implementation tries to optimize for simulator execution, especially for OS boots. | |||
| 2018-11-29 | RISC-V: factor the execution trace. | Prashanth Mundkur | |
| This is now split into instructions, regs, memory and platform, each controlled individually. Currently all are enabled and not connected to any command-line options, so a recompile is needed for trace tuning. | |||
| 2018-11-29 | RISC-V: no ldu for rv64i | Brian Campbell | |
| 2018-11-29 | RISC-V: properly set mstatus.FS in absence of floating-point support. | Prashanth Mundkur | |
| 2018-11-29 | RISC-V: minor cleanup of the spike interface. | Prashanth Mundkur | |
| 2018-11-29 | RISC-V: add some missing constraints on compressed instruction encodings | Brian Campbell | |
| 2018-11-29 | RISC-V: add checks for misaligned targets to jumps and branches | Brian Campbell | |
| 2018-11-29 | Merge branch 'rvfi-dii' into sail2 | Brian Campbell | |
| (except without the accidentally committed aarch64 files from the branch) | |||
| 2018-11-27 | Fix memory leak in string_of_bits | Alasdair Armstrong | |
| Should hopefully fix memory leak in RISC-V. Also adds an optimization pass that removes copying structs and allows some structs to simply alias each other and avoid copying their contents. This requires knowing certain things about the lifetimes of the structs involved, as can't free the struct if another variable is referencing it - therefore we conservatively only apply this optimization for variables that are lifted outside function definitions, and should therefore never get freed until the model exits - however this may cause issues outside ARMv8, as there may be cases where a struct can exist within a variant type (which are not yet subject to this lifting optimisation), that would break these assumptions - therefore this optimisation is only enabled with the -Oexperimental flag. | |||
| 2018-11-21 | RISC-V: allow platform ram size to be configurable. | Prashanth Mundkur | |
| 2018-11-20 | Minor coq updates | Brian Campbell | |
| 2018-11-14 | Add option to turn off RISC-V compressed instruction support | Brian Campbell | |
| 2018-11-14 | Fix memory map in RVFI-DII mode | Brian Campbell | |
| 2018-11-14 | update riscv_all.sail and riscv_platform.sail for updated riscv model | Jon French | |
| 2018-11-12 | rvfi_dii: take port number with option | Brian Campbell | |
| 2018-11-12 | Add RVFI DII version of the RISC-V simulator for TestRIG | Brian Campbell | |
| The new riscv_rvfi target should still be usable as a normal simulator, but also has extra registers in the model for the RVFI DII protocol and code to update them, and the driver has a -r option to enable RVFI mode. | |||
| 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-11-01 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-10-24 | Interpreter, RISC-V: move memory actions to parts of the interpreter ↵ | Jon French | |
| response and refactor RISC-V model accordingly | |||
| 2018-10-24 | RISC-V: add Sail implementations of just enough platform for interpreter to work | Jon French | |
| 2018-10-24 | Interpreter: don't silently use OCaml externs, only interpreter externs | Jon French | |
| (Adds 'interpreter' externs as appropriate.) | |||
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |