summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-10-23RISC-V: implement terminal output for C platform.Prashanth Mundkur
2018-10-23RISC-V: tick the clock in the C platform.Prashanth Mundkur
2018-10-23RISC-V: Add device tree blob into rom, currently only when linked against spike.Prashanth Mundkur
2018-10-23RISC-V: add default reset vector.Prashanth Mundkur
2018-10-23RISC-V: fix up platform bits for lr/sc.Prashanth Mundkur
2018-10-23RISC-V: set htif tohost port address using ELF symbol.Prashanth Mundkur
2018-10-23RTS: Add elf symbol lookup support.Prashanth Mundkur
2018-10-23Fix typo in plat_ram_sizeAlasdair Armstrong
2018-10-23RISC-V: Add some debug logs for within_phys_mem.Prashanth Mundkur
2018-10-23RISC-V: Allow Spike linkage to be conditionally enabled.Prashanth Mundkur
2018-10-23RISC-V: flush logs at each step.Prashanth Mundkur
2018-10-23RISC-V: Flesh out more of the tandem checks in the C platform simulator.Prashanth Mundkur
2018-10-23RISC-V: An initial C Sail model linked against Spike for testing.Prashanth Mundkur
2018-10-23RTS: allow elf-loader to provide entry info.Prashanth Mundkur
2018-10-23RISC-V: Refactor c platform bits.Prashanth Mundkur
2018-10-22Coq: use function type more carefully in untuplingBrian Campbell
2018-10-22Update Coq patch for RISC-V, add string_take to Coq libraryBrian Campbell
2018-10-22Coq: work around constructors with tupled argumentsBrian Campbell
2018-10-22Fix lem arguments for functions with tuple argumentsAlasdair Armstrong
2018-10-22Pretty_print_lem.untuple_args_pat: temporary hack to allow functions that act...Jon French
2018-10-16add a couple more RISC-V things to gitignoreJon French
2018-10-16Re-implement space-related mapping functions in Sail rather than backendsJon French
2018-10-16rewrites: remove now-unnecessary temporary string hack from rewrite_defs_pat_...Jon French
2018-10-15Update manual snapshotAlasdair Armstrong
2018-10-13Adapt checked_mem_read to have acquire/release/reserve arguments soChristopher Pulte
2018-10-12Prevent accidental test failures when Coq compiles in the wrong orderBrian Campbell
2018-10-11Change the function type in the ASTAlasdair
2018-10-10refer to Util.list_init.ml rather than List.init in sail_lib.mlChristopher Pulte
2018-10-08Produce lists of constructors and ast building functions for test generationBrian Campbell
2018-10-05interpreter: Remove boxes (no longer used)Jon French
2018-10-05RISC-V: encode/decode and assembly mappings for compressed instructionsJon French
2018-10-05fix bug in infer_mpat losing types of identifiers inferred from other_envJon French
2018-10-04Merge branch 'ocaml-instruction-generation' into sail2Brian Campbell
2018-10-04Bit of commentary, proper TODO errorBrian Campbell
2018-10-04rename stringappend ids for more readable generated codeJon French
2018-10-03Drop unnecessary thunking; more trouble than it's worthBrian Campbell
2018-10-02Tidy up some whitespaceBrian Campbell
2018-10-02Clean up generator pretty printingBrian Campbell
2018-10-02Remove some old debugging messagesBrian Campbell
2018-10-02Trigger random generator generation with a command line optionBrian Campbell
2018-10-02Rough code to generate random instructions for testingBrian Campbell
2018-10-01Update Coq RISC-V patch now that the assembler is in good shapeBrian Campbell
2018-10-01Extend Coq pattern match completeness rewrite to let patternsBrian Campbell
2018-10-01New rewriting pass toplevel_string_appendJon French
2018-09-28Add a regression test for bug in commit 88b25e9Alasdair Armstrong
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong
2018-09-27Add new functions in ast_util.ml for working with locationsAlasdair Armstrong
2018-09-27Add an additional type checking testAlasdair Armstrong
2018-09-24Coq: avoid variables called tt (the unit constant)Brian Campbell
2018-09-24Coq: more constraint solutions for aarch64Brian Campbell