| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-29 | RISC-V: more tidying up of the Spike interface. | Prashanth Mundkur | |
| 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-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 Spike linkage to be conditionally enabled. | 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-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-08-31 | Some C stubs for platform bits for RISC-V. | Prashanth Mundkur | |
| 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-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-13 | Add constraints to RISC-V duopod, makefile rules | 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 a riscv latex target. | Prashanth Mundkur | |
| 2018-07-10 | Start adding c-backend bits for riscv. | Prashanth Mundkur | |
| 2018-07-10 | Make HOL build properly again for all of the models | Brian Campbell | |
| 2018-07-09 | add riscv_analysis.sail to SAIL_SRCS | Jon French | |
| 2018-07-08 | Add a riscv coverage target using bisect-ppx. | Prashanth Mundkur | |
| 2018-06-22 | Add a simple trace log comparison tool for riscv vs. a patched spike. | Prashanth Mundkur | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| (involved some manual tinkering with gitignore, type_check, riscv) | |||
| 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-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 mem-op-result to _sys to be usable from _platform. | Prashanth Mundkur | |
| 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-11 | Merge branch 'sail2' into cheri-mono | Thomas Bauereiss | |
| In order to use up-to-date sequential CHERI model for test suite | |||
| 2018-05-10 | RISC-V in HOL4 | Brian Campbell | |
| 2018-05-10 | Merge branch 'sail2' into mappings | Jon French | |
| 2018-05-10 | riscv/Makefile: add SAIL variable for easier debugging | Jon French | |
| 2018-05-09 | remove redundant cloc targets. | Robert Norton | |
| 2018-05-09 | Add targets for counting lines in mips, cheri and riscv. Can use either ↵ | Robert Norton | |
| sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount. | |||
| 2018-05-09 | add SAIL_FLAGS env var to riscv makefile | Jon French | |
| 2018-05-03 | Implement fetch to properly handle RVC and address translation, and add a ↵ | Prashanth Mundkur | |
| step function for execution. | |||
| 2018-04-23 | Make riscv build depend on Makefile updates. | Prashanth Mundkur | |
| 2018-04-13 | Move riscv memory definitions into a separate file. | Prashanth Mundkur | |
| 2018-03-21 | Patch AST datatypes in generated Isabelle theories | Thomas Bauereiss | |
| Deactivate plugins of the datatype package except for the size plugin in order to keep processing time reasonable. This is currently only needed for the big AST datatypes, so we just patch this using a sed command. | |||
| 2018-02-15 | Rebase state monad onto prompt monad | Thomas Bauereiss | |
| Generate only one Lem model based on the prompt monad (instead of two models with different monads), and add a lifting from prompt to state monad. Add some Isabelle lemmas about the monad lifting. Also drop the "_embed" and "_sequential" suffixes from names of generated files. | |||
| 2018-02-01 | Clean up riscv_duopod sail and add make targets for ocaml and Isabelle. | Robert Norton | |
| 2018-01-29 | riscv: fix warnings about incomplete patterns. Add a check target in ↵ | Robert Norton | |
| Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings. | |||
| 2018-01-29 | Added ecall/mret and exception support. | Prashanth Mundkur | |
| 2018-01-27 | Add Makefile for RISC-V | Thomas Bauereiss | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |