aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)AuthorFilesLines
2019-03-04Merge branch 'master' into rv32Prashanth Mundkur1-4/+3
2019-03-03rmem does not need the -lem_sequential anymoreShaked Flur1-4/+2
2019-03-01Make clean remove coq extras build filesBrian Campbell1-0/+1
2019-02-27Initial attempt to separate generated files by ARCH. Some ↵Prashanth Mundkur1-56/+55
backends/rvfi/rmem still to be tested.
2019-02-26Merge branch 'master' into rv32Prashanth Mundkur1-6/+16
2019-02-20Add ELF architecture checks to the loaders in the OCaml and C emulators.Prashanth Mundkur1-1/+1
2019-02-19Adjust Makefile to use an ARCH argument. Undo xlen guards in ↵Prashanth Mundkur1-10/+47
riscv_analysis, instead conditionally include it in sources, depending on the ARCH.
2019-02-13Add Sv32 and Sv48 by essentially copying Sv39.Prashanth Mundkur1-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-13Pull out the Sv39 and its TLB into separate files.Prashanth Mundkur1-1/+1
2019-02-13Make repository have shape RMEM expectsAlasdair Armstrong1-2/+2
2019-02-13Switch version of riscv_extras.lem depending on Sail versionAlasdair Armstrong1-12/+13
Works around change to write_mem function signature in monad embedding
2019-02-12Start extracting bits of vmem that should be common to RV32, and add some ↵Prashanth Mundkur1-2/+4
definitions for Sv32 and Sv48.
2019-02-12Minor makefile cleanup h/t @fshaked.Prashanth Mundkur1-4/+3
2019-02-12Compatability fixes from Sail 0.7.1 to Sail 0.8Alasdair Armstrong1-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-11Fix xlen variable name.Prashanth Mundkur1-1/+1
2019-02-11More refactoring for RV32Prashanth Mundkur1-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-08Start parameterizing definitions by xlen, which is currently still 64.Prashanth Mundkur1-2/+2
2019-02-08Split out the mapping prelude into its own file.Prashanth Mundkur1-5/+7
2019-01-31Fix riscv_isa_build Makefile targetThomas Bauereiss1-1/+2
2019-01-29Update Makefile.Prashanth Mundkur1-1/+1
2019-01-29Add CSRs for the 'N' extension arch state and expose to CSR read/write.Prashanth Mundkur1-1/+1
2019-01-29Factor the _sys functionality into separate files for architectural state ↵Prashanth Mundkur1-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-29Added riscv_rmem that generates the lem files for rmem (which are different ↵Shaked Flur1-4/+19
from the lem files for the theorem provers)
2019-01-25Factor out each extension into separate files, do some minor cleanup.Prashanth Mundkur1-3/+4
2019-01-22Build HOL definitions by defaultThomas Bauereiss1-1/+1
2019-01-22Add build Makefile targets for prover backendsThomas Bauereiss1-3/+36
2019-01-21Output auxiliary Isabelle theories into generated_definitions/isabelleThomas Bauereiss1-6/+9
Also copy ROOT file into the same directory
2019-01-16More reorg.Prashanth Mundkur1-71/+71
. move prover files into a single support directory . generated_models -> generated_definitions . reset vector -> c_emulator
2019-01-16Properly locate generated latex.Prashanth Mundkur1-1/+2
2019-01-16Make it clearer that the outer c,ocaml sub-dirs contain supporting files for ↵Prashanth Mundkur1-27/+28
the emulators.
2019-01-15Ensure generated model sub-dirs are created.Prashanth Mundkur1-0/+12
2019-01-15Make the names of the OCaml and C simulators more similar, with C being the ↵Prashanth Mundkur1-9/+9
default one.
2019-01-14Reorganize directory structure.Prashanth Mundkur1-95/+89
2019-01-02Add termination measures to get patch-free Coq outputBrian Campbell1-2/+3
2018-12-20Commit changes from ↵Robert Norton1-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-17Fix stray - in Makefile accidentally introduced by previous commit.Robert Norton1-1/+1
2018-12-17Add build time COVERAGE option to build with gcc coverage. Attempt to choose ↵Robert Norton1-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-30Update default make targets and README.Prashanth Mundkur1-3/+9
2018-11-30Disable line-of-code counting which is broken if SAIL_DIR is not set.Robert Norton1-2/+2
2018-11-30Split out riscv from sail repo using git-filter-branch.Robert Norton1-14/+27
2018-11-29RISC-V: more tidying up of the Spike interface.Prashanth Mundkur1-12/+12
2018-11-12Add RVFI DII version of the RISC-V simulator for TestRIGBrian Campbell1-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-23RISC-V: separate jalr execute clause for seq model and rmem.Prashanth Mundkur1-3/+12
2018-10-23RISC-V: Initial splitting of instructions across multiple files.Prashanth Mundkur1-1/+3
2018-10-23RISC-V: Allow Spike linkage to be conditionally enabled.Prashanth Mundkur1-5/+13
2018-10-23RISC-V: An initial C Sail model linked against Spike for testing.Prashanth Mundkur1-0/+12
2018-10-23RISC-V: Refactor c platform bits.Prashanth Mundkur1-2/+3
2018-09-04C: Tweaks to RISC-V to get compiling to CAlasdair Armstrong1-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-31Some C stubs for platform bits for RISC-V.Prashanth Mundkur1-3/+5
2018-08-30Annotate the RISC-V prelude for C builtins.Prashanth Mundkur1-4/+4
Add some builtins to the C sail lib. Enable some gcc warnings.
generated by cgit v1.1 at 2024-08-27 15:19:58 +0000