| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-26 | Main: further refinement of execution cycle | Alastair Reid | |
| Mostly improving error messages | |||
| 2018-06-26 | Prelude: as received from Alasdair | Alastair Reid | |
| 2018-06-26 | Main: attempt to capture AArch64 execution cycle | Alastair Reid | |
| 2018-06-26 | mips: fix duplication of cycle_count call that arose due to git merge. | Robert Norton | |
| 2018-06-26 | mips: comment out printing of EXCEPTION on every ISA exception. | Robert Norton | |
| 2018-06-26 | turn on warnings when compiling mips c then dial back ones that are ↵ | Robert Norton | |
| triggered by generated code (probably false positives). Fix some warnings in rts.c | |||
| 2018-06-26 | RTS: implement sleep primitives | Alastair Reid | |
| Note that an alternative implementation choice is just to implement them as SAIL functions manipulating a global variable. Not sure which is better. | |||
| 2018-06-26 | RTS: stub support for -C command line option | Alastair Reid | |
| 2018-06-26 | ELF: Restore error messages in ELF reader | Alastair Reid | |
| 2018-06-26 | In guarded pattern rewriting, irrefutable patterns subsume wildcards | Brian Campbell | |
| Necessary to prevent redundant clauses that Coq will reject (There's still a problem if you use a variable rather than a wildcard, see the test) | |||
| 2018-06-26 | In elf_loader don't attempt to convert paddr to int64 because on MIPS it is ↵ | Robert Norton | |
| quite likely to exceed representable range of signed 64-bit integer (e.g. address starting 0x9...). Also make clear which values are displayed in hex vs. decimal. | |||
| 2018-06-25 | Add a riscv platform parameter to control trapping to M-mode on misaligned ↵ | Prashanth Mundkur | |
| access, and a cli option to control it. | |||
| 2018-06-25 | Increment the riscv trace step counter only when instructions are executed. | Prashanth Mundkur | |
| 2018-06-25 | Hook in the missed misa legalizer. | Prashanth Mundkur | |
| 2018-06-25 | Fix riscv interrupt pending check to handle implicit enabling at lower ↵ | Prashanth Mundkur | |
| privileges. Also fix timer threshold comparison to be <= instead of <. | |||
| 2018-06-25 | Make sstatus.UXL legalization match spike for now. Leave a fixme to make ↵ | Prashanth Mundkur | |
| this a platform setting. | |||
| 2018-06-25 | Fix a missed fixme for the sstatus view of mstatus. | Prashanth Mundkur | |
| 2018-06-25 | Fix tracecmp for spike's recursive calls for sie/sip/sstatus csr writes. | Prashanth Mundkur | |
| 2018-06-25 | Check for variables in disjointness check | Thomas Bauereiss | |
| 2018-06-25 | Support bitlist representation in Sail2_string | Thomas Bauereiss | |
| 2018-06-25 | Fix a bug in pattern guard rewriting | Thomas Bauereiss | |
| Remember and use fallthrough clauses instead of dropping them when the last clause in a group has a guard | |||
| 2018-06-25 | Coq: add typeclass based comparison, and instantiate for enums | Brian Campbell | |
| 2018-06-25 | Coq: automatic cast introduction | Brian Campbell | |
| 2018-06-25 | Use getopt rather than argp for Mac compatibility in C runtime | Alasdair Armstrong | |
| Also further tweaks to Sail library for C and include sail lib files for tracing | |||
| 2018-06-25 | add device tree file for mips. | Robert Norton | |
| 2018-06-25 | mips: add optional tracing of register writes (commented out). | Robert Norton | |
| 2018-06-25 | flush stdout after putchar for terminal emulation purposes. | Robert Norton | |
| 2018-06-25 | Fix bugs in mips ldl/ldr that were probably introduced in porting to sail2. | Robert Norton | |
| 2018-06-23 | Add clock tick checks to the riscv tracecmp tool. | Prashanth Mundkur | |
| 2018-06-23 | Fix a missing check for interrupt dispatch when riscv clint registers are ↵ | Prashanth Mundkur | |
| written. | |||
| 2018-06-23 | Split Sail->ANF translation into its own file | Alasdair | |
| Refactor the C compilation process by moving out the conversion to A-normal form into its own file. Also make the A-normal form AST parameterised by the type of the types annotating it. The idea being we can have a typ aexp -> ctyp aexp translation, converting to low-level types at a slightly higher level before mapping into our low-level IR. This would fix some issues we have where the type of variables change due to flow typing, because we could map the sail types to low-level types in the ANF ast where we still have some knowledge about the structure of the original Sail. | |||
| 2018-06-22 | Make riscv pte dirty-bit update handling configurable via a platform cli option. | Prashanth Mundkur | |
| Fix a redundant clock tick. | |||
| 2018-06-22 | Some more riscv trace log tweaking for spike compatibility. | Prashanth Mundkur | |
| 2018-06-22 | Add cli options to riscv simulator to dump platform device-tree info. | Prashanth Mundkur | |
| 2018-06-22 | Fix Lem build of MIPS/CHERI | Thomas Bauereiss | |
| 2018-06-22 | Add a simple trace log comparison tool for riscv vs. a patched spike. | Prashanth Mundkur | |
| 2018-06-22 | Fix up constraints in OCaml reg_ref test | Brian Campbell | |
| 2018-06-22 | Add current state of mips_extras.v | Brian Campbell | |
| 2018-06-22 | Precise bitvector subrange functions for Coq. | Brian Campbell | |
| Also fix the constraints in the standard prelude files, add a couple of useful cast rewriting lemmas. | |||
| 2018-06-22 | Fix bug in elf_loader: zero memory when segment memsz exceeds size. | Prashanth Mundkur | |
| 2018-06-22 | More trace log tweaks. | Prashanth Mundkur | |
| 2018-06-22 | Add bitvector size constraints in MIPS | Brian Campbell | |
| 2018-06-22 | Add coq builtins for MIPS | Brian Campbell | |
| 2018-06-22 | Add coq generation rule for mips | Brian Campbell | |
| 2018-06-22 | Coq: use simple forms for simple pattern matches in E_internal_let | Brian Campbell | |
| 2018-06-22 | Coq: library updates, esp extending bitvector multiplies, Undefined | Brian Campbell | |
| 2018-06-22 | Coq: project away range types in comparisons | Brian Campbell | |
| 2018-06-22 | build mips and mips_c when running tests. | Robert Norton | |
| 2018-06-22 | add support for new cycle_limit feature in mips. | Robert Norton | |
| 2018-06-21 | Add command line option support for Sail->C compiled models | Alasdair Armstrong | |
| For example, the MIPS model can boot FreeBSD as ./mips_c --binary=0x100000,/path/to/kernel --image=/path/to/simboot.sailbin Or with short options as ./mips_c -b 0x100000,/path/to/kernel -i /path/to/simboot.sailbin The current options are: -e, --elf, which loads an elf file directly -n, --entry, which sets the entry point -i, --image, which loads an image file compiled by "sail -elf" using Linksem -b, --binary, which loads a plain binary image into memory at a specific address -l, --cyclelimit, which means the (new) cycle_count() builtin exits the model after a certain number of calls Also there are the default -? --help and --usage options. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |