Age | Commit message (Collapse) | Author | Files | Lines | |
---|---|---|---|---|---|
2019-03-04 | Merge branch 'master' into rv32 | Prashanth Mundkur | 1 | -4/+3 | |
2019-03-03 | rmem does not need the -lem_sequential anymore | Shaked Flur | 1 | -4/+2 | |
2019-03-01 | Make clean remove coq extras build files | Brian Campbell | 1 | -0/+1 | |
2019-02-27 | Initial attempt to separate generated files by ARCH. Some ↵ | Prashanth Mundkur | 1 | -56/+55 | |
backends/rvfi/rmem still to be tested. | |||||
2019-02-26 | Merge branch 'master' into rv32 | Prashanth Mundkur | 1 | -6/+16 | |
2019-02-20 | Add ELF architecture checks to the loaders in the OCaml and C emulators. | Prashanth Mundkur | 1 | -1/+1 | |
2019-02-19 | Adjust Makefile to use an ARCH argument. Undo xlen guards in ↵ | Prashanth Mundkur | 1 | -10/+47 | |
riscv_analysis, instead conditionally include it in sources, depending on the ARCH. | |||||
2019-02-13 | Add Sv32 and Sv48 by essentially copying Sv39. | Prashanth Mundkur | 1 | -1/+3 | |
Being first-order prevents straight-forward abstraction over the PTE operations, but perhaps there is another way to generalize and unify. | |||||
2019-02-13 | Pull out the Sv39 and its TLB into separate files. | Prashanth Mundkur | 1 | -1/+1 | |
2019-02-13 | Make repository have shape RMEM expects | Alasdair Armstrong | 1 | -2/+2 | |
2019-02-13 | Switch version of riscv_extras.lem depending on Sail version | Alasdair Armstrong | 1 | -12/+13 | |
Works around change to write_mem function signature in monad embedding | |||||
2019-02-12 | Start extracting bits of vmem that should be common to RV32, and add some ↵ | Prashanth Mundkur | 1 | -2/+4 | |
definitions for Sv32 and Sv48. | |||||
2019-02-12 | Minor makefile cleanup h/t @fshaked. | Prashanth Mundkur | 1 | -4/+3 | |
2019-02-12 | Compatability fixes from Sail 0.7.1 to Sail 0.8 | Alasdair Armstrong | 1 | -1/+11 | |
Two small compatability fixes: Small change to the prelude to make sure we are forwards compatable with the next release of Sail, which has slightly different syntax for implicit arguments. Due to changes in the monad embedding in the latest git version of Sail, we disable generating Lem by default when we detect we are on that version. It's a small one line fix to correct, but we want to keep the Lem definitions in this repository compatible with the opam release 0.7.1 for now. | |||||
2019-02-11 | Fix xlen variable name. | Prashanth Mundkur | 1 | -1/+1 | |
2019-02-11 | More refactoring for RV32 | Prashanth Mundkur | 1 | -2/+2 | |
- split out memory access definitions in prelude that depend on xlen - make riscv_xlen now part of the prelude set, so that riscv_duopod can use the definition - update xlen use in riscv_duopod so that it can now support rv32 | |||||
2019-02-08 | Start parameterizing definitions by xlen, which is currently still 64. | Prashanth Mundkur | 1 | -2/+2 | |
2019-02-08 | Split out the mapping prelude into its own file. | Prashanth Mundkur | 1 | -5/+7 | |
2019-01-31 | Fix riscv_isa_build Makefile target | Thomas Bauereiss | 1 | -1/+2 | |
2019-01-29 | Update Makefile. | Prashanth Mundkur | 1 | -1/+1 | |
2019-01-29 | Add CSRs for the 'N' extension arch state and expose to CSR read/write. | Prashanth Mundkur | 1 | -1/+1 | |
2019-01-29 | Factor the _sys functionality into separate files for architectural state ↵ | Prashanth Mundkur | 1 | -2/+4 | |
and processing logic. Also check misa.N() when lifting and lowering {ms}i{pe}, and misa.S() when accessing S-mode CSRs. | |||||
2019-01-29 | Added riscv_rmem that generates the lem files for rmem (which are different ↵ | Shaked Flur | 1 | -4/+19 | |
from the lem files for the theorem provers) | |||||
2019-01-25 | Factor out each extension into separate files, do some minor cleanup. | Prashanth Mundkur | 1 | -3/+4 | |
2019-01-22 | Build HOL definitions by default | Thomas Bauereiss | 1 | -1/+1 | |
2019-01-22 | Add build Makefile targets for prover backends | Thomas Bauereiss | 1 | -3/+36 | |
2019-01-21 | Output auxiliary Isabelle theories into generated_definitions/isabelle | Thomas Bauereiss | 1 | -6/+9 | |
Also copy ROOT file into the same directory | |||||
2019-01-16 | More reorg. | Prashanth Mundkur | 1 | -71/+71 | |
. move prover files into a single support directory . generated_models -> generated_definitions . reset vector -> c_emulator | |||||
2019-01-16 | Properly locate generated latex. | Prashanth Mundkur | 1 | -1/+2 | |
2019-01-16 | Make it clearer that the outer c,ocaml sub-dirs contain supporting files for ↵ | Prashanth Mundkur | 1 | -27/+28 | |
the emulators. | |||||
2019-01-15 | Ensure generated model sub-dirs are created. | Prashanth Mundkur | 1 | -0/+12 | |
2019-01-15 | Make the names of the OCaml and C simulators more similar, with C being the ↵ | Prashanth Mundkur | 1 | -9/+9 | |
default one. | |||||
2019-01-14 | Reorganize directory structure. | Prashanth Mundkur | 1 | -95/+89 | |
2019-01-02 | Add termination measures to get patch-free Coq output | Brian Campbell | 1 | -2/+3 | |
2018-12-20 | Commit changes from ↵ | Robert Norton | 1 | -0/+6 | |
rems-project/sail@b167a59affdb6428fa0656a092b335a3a6899d56 which was committed after forking sail-riscv from that repo. Adds some make targets for calling cgen WIP and interpreter. | |||||
2018-12-17 | Fix stray - in Makefile accidentally introduced by previous commit. | Robert Norton | 1 | -1/+1 | |
2018-12-17 | Add build time COVERAGE option to build with gcc coverage. Attempt to choose ↵ | Robert Norton | 1 | -6/+17 | |
amenable gcc and sail optimisation options in this case. Add a sed hack to remove very blank lines from sail c output for rvfi build. | |||||
2018-11-30 | Update default make targets and README. | Prashanth Mundkur | 1 | -3/+9 | |
2018-11-30 | Disable line-of-code counting which is broken if SAIL_DIR is not set. | Robert Norton | 1 | -2/+2 | |
2018-11-30 | Split out riscv from sail repo using git-filter-branch. | Robert Norton | 1 | -14/+27 | |
2018-11-29 | RISC-V: more tidying up of the Spike interface. | Prashanth Mundkur | 1 | -12/+12 | |
2018-11-12 | Add RVFI DII version of the RISC-V simulator for TestRIG | Brian Campbell | 1 | -0/+9 | |
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 | 1 | -3/+12 | |
2018-10-23 | RISC-V: Initial splitting of instructions across multiple files. | Prashanth Mundkur | 1 | -1/+3 | |
2018-10-23 | RISC-V: Allow Spike linkage to be conditionally enabled. | Prashanth Mundkur | 1 | -5/+13 | |
2018-10-23 | RISC-V: An initial C Sail model linked against Spike for testing. | Prashanth Mundkur | 1 | -0/+12 | |
2018-10-23 | RISC-V: Refactor c platform bits. | Prashanth Mundkur | 1 | -2/+3 | |
2018-09-04 | C: Tweaks to RISC-V to get compiling to C | Alasdair Armstrong | 1 | -1/+2 | |
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 | 1 | -3/+5 | |
2018-08-30 | Annotate the RISC-V prelude for C builtins. | Prashanth Mundkur | 1 | -4/+4 | |
Add some builtins to the C sail lib. Enable some gcc warnings. |