| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-12 | Make progress on HOL4 test_raw_add | Ramana Kumar | |
| The proof now gets through simulation of the first instruction of the test. | |||
| 2018-06-12 | Work on HOL symbolic evaluation of installing code | Ramana Kumar | |
| 2018-06-12 | Experimentation with PrePost for test_raw_add | Ramana Kumar | |
| 2018-06-12 | Speculation on executing a CHERI test in HOL4 | Ramana Kumar | |
| 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 | add 'pat as id' mapping-patterns | Jon French | |
| 2018-06-11 | Merge branch 'mappings' into sail2 | Jon French | |
| 2018-06-11 | actually fix exist_pattern test | Jon French | |
| 2018-06-11 | fix test exist_pattern.sail -- lem needed much more of the stdlib to be imported | Jon French | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| 2018-06-11 | Add string.sail file to lib | Alasdair Armstrong | |
| 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 | ocaml test prelude: option is now in stdlib | Jon French | |
| 2018-06-11 | drop now-unnecessary type annotation clutter from riscv decode mappings | Jon French | |
| 2018-06-11 | better type inference of union-constructors and 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-09 | Fix issue in C_backend, and run C tests with undefined behavior sanitizer | Alasdair | |
| 2018-06-09 | Fix issue with catch block return values not being compiled correctly | Alasdair | |
| This should fix the issue raised in commit 45554f Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations | |||
| 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 | Fix use of non-tail-recursive calls in elf_loader. | Prashanth Mundkur | |
| 2018-06-08 | type checking mappings: allow inferring based on the other side's id inferences | Jon French | |
| 2018-06-08 | Coq: some handling of existential types as function return types | Brian Campbell | |
| 2018-06-08 | Coq: add destructuring of atom existentials in patterns | Brian Campbell | |
| Plus test case, broken builtin name | |||
| 2018-06-08 | Coq: track add_typquant change | Brian Campbell | |
| 2018-06-08 | Correct dependencies of bytecode sail | Brian Campbell | |
| 2018-06-08 | Coq: existential and constraint solving work | Brian Campbell | |
| - add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving | |||
| 2018-06-08 | Coq: some very basic existential support | Brian Campbell | |
| Only single variable in places, only packed at literals and variables, no unpacking | |||
| 2018-06-08 | Coq: fix axiom generation | Brian Campbell | |
| 2018-06-08 | Coq: ignore some currently unsupported tests | Brian Campbell | |
| 2018-06-08 | Coq: update foreach handling, correct field accesses | Brian Campbell | |
| 2018-06-08 | Fill in most Coq built-ins | Brian Campbell | |
| 2018-06-08 | Coq: skip two tests with redundant pattern matches | Brian Campbell | |
| 2018-06-08 | Coq: correct failure on unsupported undefined values | Brian Campbell | |
| 2018-06-08 | Coq: use record update syntax (only single fields work for now) | Brian Campbell | |
| 2018-06-08 | Coq: correct implicitness of type arguments in unions | Brian Campbell | |
| 2018-06-08 | Add missing Coq builtin info to vector_inc | Brian Campbell | |
| 2018-06-08 | add sail as dependency of mips targets. | Robert Norton | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |