aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)AuthorFilesLines
2020-01-23Add lem stubs for softfloat externs.rsnikhilPrashanth Mundkur1-2/+2
2020-01-22Merge branch 'master' into rsnikhilPrashanth Mundkur1-2/+2
2020-01-18Allow extensions to provide their own exception codes/namesJames Clarke1-2/+2
2020-01-08Add softfloat to rvfi build.Prashanth Mundkur1-1/+1
2020-01-07Merge branch 'master' into rsnikhil.Prashanth Mundkur1-26/+31
2020-01-07Separate out RVFI simulators like non-RVFIJames Clarke1-4/+4
2019-12-05Fix RVFI buildThomas Bauereiss1-1/+1
2019-12-03Merge remote-tracking branch 'origin/master' into mem_meta_mergeRobert Norton1-3/+10
2019-11-28Fix check for BBV_DIRThomas Bauereiss1-1/+1
2019-11-26Fix RV32 build for F/D extensions.Prashanth Mundkur1-4/+7
2019-11-26Add individual ocaml stubs for the softfloat functions.Prashanth Mundkur1-1/+1
2019-11-25Work around Isabelle problem in PTW functionsThomas Bauereiss1-0/+1
The standard pattern completeness proof for recursive functions generated by Lem for Isabelle seems to get confused in some situations when there are variables with unit type (in particular the ext_ptw argument of the page table walk functions). Solving this properly requires some more digging into the Isabelle simplifier, but the ad-hoc workaround in this commit fixes the problem for now.
2019-11-14Create a RISC-V specialization for the default NaN bitpatterns in softfloat.Prashanth Mundkur1-2/+3
2019-11-06Separate out fdext control and update makefile.Prashanth Mundkur1-11/+7
2019-11-05Merge pull request #24 from rems-project/csr_extPrashanth Mundkur1-0/+6
Extension hooks for CSR access control
2019-11-04First cut at adding externs for softfloat.Prashanth Mundkur1-5/+15
This uses a couple of internal registers to avoid anonymous structs as C return types.
2019-11-01Fix up riscv_duopod and make self containedAlasdair Armstrong1-3/+3
2019-10-31Add convenience targets for c emulator and rvfi.Robert Norton1-0/+6
2019-10-23Split 'riscv_insts_fdext.sail' into separate files for F and D, ↵rsnikhil1-1/+1
'riscv_insts_fext.sail' and 'riscv_insts_dext.sail' The two files correspond very closely to each other when viewed side-by-side.
2019-10-22Work-in-progress commit; some 'execute' clauses completed (detail below).rsnikhil1-1/+2
Added riscv_softfloat_interface.sail file with stubs for external calls to Berkeley softfloat. These are invoked by the 'execute' clauses. Finished execute clauses for FADD/FSUB/FMUL/FDIV for _S and _D. Finished execute clauses for FMADD/FMSUB/FNMSUB/FNMADD for _S and _D.
2019-10-21Interim commit while developing code for F, D extensions (detail below).rsnikhil1-1/+13
Commit ecb29cb115c9 added all the AST, encdec, and assembly clauses for F,D, and execute clauses with empty bodies (just LOAD_FP and STORE_FP are done). This commit is after fixing all syntax and type-checking errors.
2019-10-09Add {read,write}_ram for CoqThomas Bauereiss1-5/+6
2019-10-09Read/write memory values and metadata together atomicallyThomas Bauereiss1-16/+12
For Lem, bypass the Sail implementation of {read,write}_ram and map to atomic primitives directly. We might want to make these functions primitive for other backends as well.
2019-09-18Add a hook for extensions to supress writes to misa.C if necessary.Robert Norton1-1/+1
2019-09-17Run Sail with -dno_cast even when it comes from opam packageScott Johnson1-1/+3
2019-09-04Merge remote-tracking branch 'origin/master' into vmem_ext.vmem_extRobert Norton1-2/+2
2019-08-19RISC-V spec, without implicit castsAlasdair Armstrong1-1/+1
2019-08-13Fix Coq duopod build by giving missing termination measureBrian Campbell1-1/+1
2019-07-22Make a custom exception code available for extensions, and remove the ↵Prashanth Mundkur1-1/+3
E_CHERI code. Enable extensions for PTE checks and PTW errors, and propagate those into exception codes.
2019-07-22Merge branch 'master' into vmem_extPrashanth Mundkur1-4/+4
2019-07-19Fixed two typosShaked Flur1-1/+1
2019-07-18Make sure everything builds correctlyAlasdair Armstrong1-4/+4
Move updated 0.11 lem files from Shaked's commit into their own directory Remove the 0.7.1 lem directory that performed a similar purpose during the prompt monad changes Re-add model changes from Shaked's commit with a feature flag
2019-07-15Allow extensions to types of memory access, and factor out PTE and PTW ↵Prashanth Mundkur1-2/+2
definitions.
2019-07-02Crank up optimisation (sail and gcc).Robert Norton1-2/+2
2019-06-26Merge branch 'master-cleanup' into pmpPrashanth Mundkur1-0/+7
2019-06-20Add PMP address and entry matching, and priority logic.Prashanth Mundkur1-1/+5
This is specialized for now for the smallest PMP grain of 4 bytes.
2019-06-17Add basic PMP definitions.Prashanth Mundkur1-1/+1
2019-06-11Remove unused directory from Coq imports, removing warningBrian Campbell1-1/+1
2019-06-06Add a makefile target to pre-compile the model for axiomatic concurrency toolAlasdair1-0/+3
2019-06-03Merge remote-tracking branch 'origin/master' into master-cleanupRobert Norton1-14/+11
2019-06-03Install sail and C sources in share directory of opam package.Robert Norton1-0/+7
2019-05-31Fix build on MacPorts/MacOS.Prashanth Mundkur1-2/+6
2019-05-30Include riscv_sim.c in C_SRCSScott Johnson1-5/+5
Since it was being explicitly included everywhere C_SRCS was being used.
2019-05-30Remove obsolete targets from MakefileScott Johnson1-7/+0
Per email from Prashanth
2019-05-24Attempt to fix opam build with opam2: use a .install file and don't rely on ↵Robert Norton1-3/+3
opam being in path to get SAIL_DIR (which seems to be unreliable).
2019-05-24Add Makefile rule to get line count.Robert Norton1-0/+3
2019-05-23Merge branch 'master' into master-cleanupPrashanth Mundkur1-0/+17
2019-05-20Add opam file and make targets to build and install C emulator (32 and 64 bit).Robert Norton1-0/+15
2019-05-17Work around name clash in IsabelleThomas Bauereiss1-0/+2
Until properly fixed in Lem
2019-05-14Merge branch 'master' into master-cleanupPrashanth Mundkur1-1/+1
generated by cgit v1.1 at 2024-08-27 10:53:06 +0000