summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-06-25Hook in the missed misa legalizer.Prashanth Mundkur
2018-06-25Fix riscv interrupt pending check to handle implicit enabling at lower privil...Prashanth Mundkur
2018-06-25Make sstatus.UXL legalization match spike for now. Leave a fixme to make this...Prashanth Mundkur
2018-06-25Fix a missed fixme for the sstatus view of mstatus.Prashanth Mundkur
2018-06-25Fix tracecmp for spike's recursive calls for sie/sip/sstatus csr writes.Prashanth Mundkur
2018-06-25Check for variables in disjointness checkThomas Bauereiss
2018-06-25Support bitlist representation in Sail2_stringThomas Bauereiss
2018-06-25Fix a bug in pattern guard rewritingThomas Bauereiss
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-25Use getopt rather than argp for Mac compatibility in C runtimeAlasdair Armstrong
2018-06-25add device tree file for mips.Robert Norton
2018-06-25mips: add optional tracing of register writes (commented out).Robert Norton
2018-06-25flush stdout after putchar for terminal emulation purposes.Robert Norton
2018-06-25Fix bugs in mips ldl/ldr that were probably introduced in porting to sail2.Robert Norton
2018-06-23Add clock tick checks to the riscv tracecmp tool.Prashanth Mundkur
2018-06-23Fix a missing check for interrupt dispatch when riscv clint registers are wri...Prashanth Mundkur
2018-06-23Split Sail->ANF translation into its own fileAlasdair
2018-06-22Make riscv pte dirty-bit update handling configurable via a platform cli option.Prashanth Mundkur
2018-06-22Some more riscv trace log tweaking for spike compatibility.Prashanth Mundkur
2018-06-22Add cli options to riscv simulator to dump platform device-tree info.Prashanth Mundkur
2018-06-22Fix Lem build of MIPS/CHERIThomas Bauereiss
2018-06-22Add a simple trace log comparison tool for riscv vs. a patched spike.Prashanth Mundkur
2018-06-22Fix up constraints in OCaml reg_ref testBrian Campbell
2018-06-22Add current state of mips_extras.vBrian Campbell
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
2018-06-22Fix bug in elf_loader: zero memory when segment memsz exceeds size.Prashanth Mundkur
2018-06-22More trace log tweaks.Prashanth Mundkur
2018-06-22Add bitvector size constraints in MIPSBrian Campbell
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Add coq generation rule for mipsBrian Campbell
2018-06-22Coq: use simple forms for simple pattern matches in E_internal_letBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-22Coq: project away range types in comparisonsBrian Campbell
2018-06-22build mips and mips_c when running tests.Robert Norton
2018-06-22add support for new cycle_limit feature in mips.Robert Norton
2018-06-21Add command line option support for Sail->C compiled modelsAlasdair Armstrong
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-06-21Remove loading kernel from mips mainAlasdair Armstrong
2018-06-21Merge branch 'sail2' of github.com:rems-project/sail into sail2Alasdair Armstrong
2018-06-21add PMP registers to CSR, fix buildJon French
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Fix MIPS wrt changes to C runtimeAlasdair Armstrong
2018-06-21Simplify the ANF->IR translationAlasdair Armstrong
2018-06-21changes to riscv model to support rmemJon French
2018-06-20Coq: Generate MR when appropriate; syntax fixesBrian Campbell
2018-06-20Coq: reverse_endiannessBrian Campbell
2018-06-20Coq: add missing existential projection on simple let expressionsBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: print div/mod/abs in nexps; avoid mod as an identifierBrian Campbell