| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-15 | Fix riscv system register initialization. | Prashanth Mundkur | |
| 2018-06-14 | rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem | Jon French | |
| 2018-06-13 | Tracing instrumentation for C backend | Alasdair Armstrong | |
| 2018-06-11 | Use riscv platform insns_per_tick to tick the clock. | Prashanth Mundkur | |
| 2018-06-11 | Put the riscv model's output on stderr, leaving stdout for the platform ↵ | Prashanth Mundkur | |
| terminal. | |||
| 2018-06-11 | Update retire semantics for riscv WFI. | Prashanth Mundkur | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| (involved some manual tinkering with gitignore, type_check, riscv) | |||
| 2018-06-11 | change double-caret for string-append-pattern to single caret, since that ↵ | Jon French | |
| wouldn't be legal in a pattern anyway | |||
| 2018-06-11 | drop now-unnecessary type annotation clutter from riscv decode mappings | Jon French | |
| 2018-06-09 | Increment minstret on instruction retires, and handle the case when the ↵ | Prashanth Mundkur | |
| minstret CSR is explicitly written to. | |||
| 2018-06-09 | Some fixes to counteren handling. | Prashanth Mundkur | |
| 2018-06-08 | Fix mmio address matching for clint device. | Prashanth Mundkur | |
| 2018-06-08 | Add counteren registers. | Prashanth Mundkur | |
| 2018-06-08 | Slightly condense execution trace log. | Prashanth Mundkur | |
| 2018-06-08 | Update initialization of misa. | Prashanth Mundkur | |
| 2018-06-08 | Make the simulation loop use the platform interface to detect exits via htif. | Prashanth Mundkur | |
| 2018-06-08 | Add mem and mmio access tracing. | Prashanth Mundkur | |
| 2018-06-08 | type checking mappings: allow inferring based on the other side's id inferences | Jon French | |
| 2018-06-07 | Slight refactor to keep platform handling localized to the _platform file. | Prashanth Mundkur | |
| 2018-06-07 | Fix width guards on htif accesses. | Prashanth Mundkur | |
| 2018-06-07 | Update physical memory and address translation for MMIO. | Prashanth Mundkur | |
| - Assume for now that atomic accesses are only to memory regions, to leave their effects unchanged. - The top-level mem_read and mem_write functions for physical memory now have rreg and wreg effects due to MMIO (due to reads/writes to device registers). It would be nice to have a separate construct for non-CPU-register state to avoid polluting the footprint. - Assume for now that page-table walks access physical memory regions only, and not MMIO regions. Leave a fixme note there to address this later, perhaps when PMP/PMA is added. | |||
| 2018-06-07 | More definitions for the physical memory map. | Prashanth Mundkur | |
| 2018-06-07 | Remove unused file. | Prashanth Mundkur | |
| 2018-06-07 | Add terminal output to riscv platform, with incomplete handling of input. | Prashanth Mundkur | |
| 2018-06-07 | Fix Lem build of RISC-V | Thomas Bauereiss | |
| 2018-06-04 | Add the htif exit command, a top-level function to initialize the riscv ↵ | Prashanth Mundkur | |
| platform, and document the artificial wreg effect due to using registers for device state. | |||
| 2018-06-04 | Uncomment the clint implementation in riscv_platform. | Prashanth Mundkur | |
| 2018-05-31 | Fixes to get ARM u-boot working in Sail. | Alasdair Armstrong | |
| Also fixes to C backend for compiling MIPS spec to C - Fix an issue with const correctness in internal_vector_update functions generated by C backend - Add builtins for MIPS to sail.h - Fix an issue where reg_deref didn't work when called on pointers to large bitvectors, i.e. vectors containing references to large bitfields as in the MIPS TLB code - Various bug fixes and changes for running U-boot on ARM model, including for interpreter and OCaml compilation. - Fix memory leak issues and incorrect shadowing for foreach loops - Update C header file. Fixes memory leak in memory read/write builtins. - Add aux constructor to ANF representation to hold environment information. - Fix undefined behavior caused by optimisation left shifting uint64_t vectors 64 or more times. Unfortunately there's more issues because the same happens for X >> 64 right shifts. It would make sense for this to be zero, because that would guarantee the property that ((X >> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n - 1) >> 1) in the optimisation to ensure that we don't cause UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64 in one go isn't according to the C standard. This issue with right-shifts only occurs for zero-length vectors, so it's not a huge deal, but it's still annoying. - Add versions of print_bits and print_int that print to stderr. Follows OCaml convention of print/prerr. Should make things more explicit. Different backends had different ideas about where print should output to, not every backend needs to have this (e.g. theorem prover backends don't need to print) but having both stderr and stdout seperate and clear is useful for executable models (UART needs to be stdout, debug messages should be stderr). | |||
| 2018-05-23 | Fix incorrect channel in dtc i/o. | Prashanth Mundkur | |
| 2018-05-23 | riscv decode now uses mapping-decode and passes tests | Jon French | |
| 2018-05-23 | restore original riscv main | Jon French | |
| 2018-05-23 | Fix riscv build for older versions of ocamlbuild (e.g. 4.02.3) by copying ↵ | Robert Norton | |
| platform ocaml files into _sbuild directory generated by sail and then running ocamlbuild there. | |||
| 2018-05-22 | Re-enable the RISC-V lem build, and switch the test-suite to use the ↵ | Prashanth Mundkur | |
| platform build. | |||
| 2018-05-22 | Fix for E_cons not being compiled correctly into OCaml | Alasdair Armstrong | |
| 2018-05-22 | Fix Lem build for RISC-V | Thomas Bauereiss | |
| 2018-05-21 | Add the missed _tags file, and fix a typo. | Prashanth Mundkur | |
| 2018-05-21 | Start platform execution at the reset-vector in the rom. | Prashanth Mundkur | |
| 2018-05-21 | Add in the platform files and update the ocaml build. Disable the isabelle ↵ | Prashanth Mundkur | |
| build until we add suitable platform definitions/stubs. The platform bits are not yet hooked into the model, but only into the build, so are untested. | |||
| 2018-05-21 | Move the top-level loop from main to riscv_step, but remove elf bits. | Prashanth Mundkur | |
| 2018-05-21 | Move mem-op-result to _sys to be usable from _platform. | Prashanth Mundkur | |
| 2018-05-21 | further RISCV mapping: all extant non-compressed instructions done | Jon French | |
| 2018-05-18 | more riscv mapping | Jon French | |
| 2018-05-18 | more riscv mappings; riscv now builds successfully to lem which builds to ↵ | Jon French | |
| isabelle (but isabelle almost certainly broken) | |||
| 2018-05-17 | Merge branch 'cheri-mono' into sail2 | Brian Campbell | |
| 2018-05-17 | Tidy up HOL4 riscv a little | Brian Campbell | |
| 2018-05-17 | Use an intermediate base_monad type alias in Lem, | Brian Campbell | |
| resolving the difference in type parameters between the prompt and state monads, and allowing a single output file to be used with either. Normally, the type alias is to the prompt monad, but for HOL4 we use the state monad. | |||
| 2018-05-15 | Merge branch 'sail2' into mappings | Jon French | |
| 2018-05-15 | Fix the ebreak instruction to trap, and remove the now obsolete internal ↵ | Prashanth Mundkur | |
| exception. This should fix the sbreak test. | |||
| 2018-05-12 | Add ROOT files | Thomas Bauereiss | |
| 2018-05-11 | ...and actually working | Jon French | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |