| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-23 | RISC-V: Initial splitting of instructions across multiple files. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Allow the C platform to get the DTB from a file, so that OS boot is ↵ | Prashanth Mundkur | |
| possible without linking to Spike. When linked with Spike, ensure that the DTBs being used are identical. | |||
| 2018-10-23 | RISC-V: add cli option to dump the platform device-tree. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Add a platform knob to control mtval contents on illegal instruction ↵ | Prashanth Mundkur | |
| faults. | |||
| 2018-10-23 | RISC-V: various fixes | Prashanth Mundkur | |
| - add mstatus to cross-check - fix typo in assembly mapping for lr/sc | |||
| 2018-10-23 | RISC-V: fix: sstatus.SD depends on .XS and .FS. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: adjust main loop for the non-spike case. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: implement terminal output for C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: tick the clock in the C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Add device tree blob into rom, currently only when linked against spike. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: add default reset vector. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: fix up platform bits for lr/sc. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: set htif tohost port address using ELF symbol. | Prashanth Mundkur | |
| 2018-10-23 | RTS: Add elf symbol lookup support. | Prashanth Mundkur | |
| 2018-10-23 | Fix typo in plat_ram_size | Alasdair Armstrong | |
| 2018-10-23 | RISC-V: Add some debug logs for within_phys_mem. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Allow Spike linkage to be conditionally enabled. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: flush logs at each step. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Flesh out more of the tandem checks in the C platform simulator. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: An initial C Sail model linked against Spike for testing. | Prashanth Mundkur | |
| 2018-10-23 | RTS: allow elf-loader to provide entry info. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Refactor c platform bits. | Prashanth Mundkur | |
| 2018-10-22 | Coq: use function type more carefully in untupling | Brian Campbell | |
| And update the RISC-V patch accordingly. | |||
| 2018-10-22 | Update Coq patch for RISC-V, add string_take to Coq library | Brian Campbell | |
| 2018-10-22 | Coq: work around constructors with tupled arguments | Brian Campbell | |
| 2018-10-22 | Fix lem arguments for functions with tuple arguments | Alasdair Armstrong | |
| Make lem output understand difference between functions taking a tuple and functions taking multiple arguments. Previously it assumed that no functions ever took a tuple as an argument, which is incorrect for mappings. | |||
| 2018-10-22 | Pretty_print_lem.untuple_args_pat: temporary hack to allow functions that ↵ | Jon French | |
| actually take a tuple argument | |||
| 2018-10-16 | add a couple more RISC-V things to gitignore | Jon French | |
| 2018-10-16 | Re-implement space-related mapping functions in Sail rather than backends | Jon French | |
| Uses new primop 'string_take' which is much easier to implement in e.g. C | |||
| 2018-10-16 | rewrites: remove now-unnecessary temporary string hack from ↵ | Jon French | |
| rewrite_defs_pat_lits | |||
| 2018-10-15 | Update manual snapshot | Alasdair Armstrong | |
| 2018-10-13 | Adapt checked_mem_read to have acquire/release/reserve arguments so | Christopher Pulte | |
| that this information propagates from the instruction definition to the memory accesses. Necessary for Promising RISC-V concurrency model. | |||
| 2018-10-12 | Prevent accidental test failures when Coq compiles in the wrong order | Brian Campbell | |
| 2018-10-11 | Change the function type in the AST | Alasdair | |
| Changes the representation of function types in the ast from Typ_fn : typ -> typ to Typ_fn : typ list -> typ to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...). In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so f : (x, y) -> z f _ = ... would be disallowed (as _ matches both x and y), forcing f(_, _) = z this would simply quite a few things, Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax how it is now. Some issues I noticed when doing this refactoring: Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function arguments so maybe it still is. Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong. Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same. | |||
| 2018-10-10 | refer to Util.list_init.ml rather than List.init in sail_lib.ml | Christopher Pulte | |
| 2018-10-08 | Produce lists of constructors and ast building functions for test generation | Brian Campbell | |
| 2018-10-05 | interpreter: Remove boxes (no longer used) | Jon French | |
| 2018-10-05 | RISC-V: encode/decode and assembly mappings for compressed instructions | Jon French | |
| 2018-10-05 | fix bug in infer_mpat losing types of identifiers inferred from other_env | Jon French | |
| 2018-10-04 | Merge branch 'ocaml-instruction-generation' into sail2 | Brian Campbell | |
| 2018-10-04 | Bit of commentary, proper TODO error | Brian Campbell | |
| 2018-10-04 | rename stringappend ids for more readable generated code | Jon French | |
| 2018-10-03 | Drop unnecessary thunking; more trouble than it's worth | Brian Campbell | |
| 2018-10-02 | Tidy up some whitespace | Brian Campbell | |
| 2018-10-02 | Clean up generator pretty printing | Brian Campbell | |
| 2018-10-02 | Remove some old debugging messages | Brian Campbell | |
| 2018-10-02 | Trigger random generator generation with a command line option | Brian Campbell | |
| 2018-10-02 | Rough code to generate random instructions for testing | Brian Campbell | |
| (aimed at RISC-V) | |||
| 2018-10-01 | Update Coq RISC-V patch now that the assembler is in good shape | Brian Campbell | |
| 2018-10-01 | Extend Coq pattern match completeness rewrite to let patterns | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |