aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)AuthorFilesLines
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.
2018-08-30Add a C header containing declarations needed by RISC-V.Prashanth Mundkur1-3/+3
2018-08-29C: Fix some issues with tuples as arguments to polymorphic constructorsAlasdair Armstrong1-2/+6
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-28Adapt theory imports for Isabelle 2018Thomas Bauereiss1-2/+2
Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
2018-08-13Add constraints to RISC-V duopod, makefile rulesBrian Campbell1-0/+4
2018-08-13Basic Coq support for RISC-VBrian Campbell1-0/+9
Note that constraints have been added to ensure that all bitvector types are inhabited.
2018-07-27Add a riscv latex target.Prashanth Mundkur1-0/+3
2018-07-10Start adding c-backend bits for riscv.Prashanth Mundkur1-0/+3
2018-07-10Make HOL build properly again for all of the modelsBrian Campbell1-1/+2
2018-07-09add riscv_analysis.sail to SAIL_SRCSJon French1-1/+1
2018-07-08Add a riscv coverage target using bisect-ppx.Prashanth Mundkur1-1/+13
2018-06-22Add a simple trace log comparison tool for riscv vs. a patched spike.Prashanth Mundkur1-0/+3
2018-06-11Merge branch 'sail2' into mappingsJon French1-4/+28
(involved some manual tinkering with gitignore, type_check, riscv)
2018-05-23Fix riscv build for older versions of ocamlbuild (e.g. 4.02.3) by copying ↵Robert Norton1-5/+7
platform ocaml files into _sbuild directory generated by sail and then running ocamlbuild there.
2018-05-22Re-enable the RISC-V lem build, and switch the test-suite to use the ↵Prashanth Mundkur1-1/+2
platform build.
2018-05-21Add in the platform files and update the ocaml build. Disable the isabelle ↵Prashanth Mundkur1-4/+11
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-21Move mem-op-result to _sys to be usable from _platform.Prashanth Mundkur1-1/+1
2018-05-17Tidy up HOL4 riscv a littleBrian Campbell1-0/+5
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell1-4/+4
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-11Merge branch 'sail2' into cheri-monoThomas Bauereiss1-0/+4
In order to use up-to-date sequential CHERI model for test suite
2018-05-10RISC-V in HOL4Brian Campbell1-0/+9
2018-05-10Merge branch 'sail2' into mappingsJon French1-1/+5
2018-05-10riscv/Makefile: add SAIL variable for easier debuggingJon French1-5/+6
2018-05-09remove redundant cloc targets.Robert Norton1-3/+0
2018-05-09Add targets for counting lines in mips, cheri and riscv. Can use either ↵Robert Norton1-0/+7
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-09add SAIL_FLAGS env var to riscv makefileJon French1-5/+5
2018-05-03Implement fetch to properly handle RVC and address translation, and add a ↵Prashanth Mundkur1-1/+1
step function for execution.
2018-04-23Make riscv build depend on Makefile updates.Prashanth Mundkur1-7/+7
2018-04-13Move riscv memory definitions into a separate file.Prashanth Mundkur1-1/+1
2018-03-21Patch AST datatypes in generated Isabelle theoriesThomas Bauereiss1-0/+1
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-15Rebase state monad onto prompt monadThomas Bauereiss1-18/+18
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-01Clean up riscv_duopod sail and add make targets for ocaml and Isabelle.Robert Norton1-0/+14
2018-01-29riscv: fix warnings about incomplete patterns. Add a check target in ↵Robert Norton1-0/+3
Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings.
generated by cgit v1.1 at 2024-10-19 12:05:47 +0000