| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-17 | Merge branch 'cheri-mono' into sail2 | Brian Campbell | |
| 2018-05-17 | Tidy up HOL4 riscv a little | Brian Campbell | |
| 2018-05-17 | Use an intermediate base_monad type alias in Lem, | Brian Campbell | |
| resolving the difference in type parameters between the prompt and state monads, and allowing a single output file to be used with either. Normally, the type alias is to the prompt monad, but for HOL4 we use the state monad. | |||
| 2018-05-15 | Fix the ebreak instruction to trap, and remove the now obsolete internal ↵ | Prashanth Mundkur | |
| exception. This should fix the sbreak test. | |||
| 2018-05-12 | Add ROOT files | Thomas Bauereiss | |
| 2018-05-11 | Work around Lem generation problem in RISC-V | Thomas Bauereiss | |
| "sum" is an existing constant in Isabelle, and the Lem constant avoiding mechanism does not seem to pick it up when used as the name of a function parameter. | |||
| 2018-05-11 | Merge branch 'sail2' into cheri-mono | Thomas Bauereiss | |
| In order to use up-to-date sequential CHERI model for test suite | |||
| 2018-05-11 | Remove buggy bit list comparison functions from Lem library | Thomas Bauereiss | |
| Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do. | |||
| 2018-05-10 | RISC-V in HOL4 | Brian Campbell | |
| 2018-05-09 | Remove unused definitions. | Prashanth Mundkur | |
| 2018-05-09 | remove redundant cloc targets. | Robert Norton | |
| 2018-05-09 | Add targets for counting lines in mips, cheri and riscv. Can use either ↵ | Robert Norton | |
| sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount. | |||
| 2018-05-07 | Add a register indicating no trigger/breakpoint support, which allows the ↵ | Prashanth Mundkur | |
| breakpoint test to pass. | |||
| 2018-05-07 | Fix another mask computation bug. | Prashanth Mundkur | |
| 2018-05-07 | Adjust default pte update setting to match spike's default. | Prashanth Mundkur | |
| 2018-05-07 | Log trap value on traps. | Prashanth Mundkur | |
| 2018-05-07 | Fix a missed csr read. | Prashanth Mundkur | |
| 2018-05-04 | Tweak the execution log. | Prashanth Mundkur | |
| 2018-05-04 | Fix two bugs in the page-table walker, and add some comments. | Prashanth Mundkur | |
| 2018-05-04 | Fix printing of ld. | Prashanth Mundkur | |
| 2018-05-03 | Fix a typo in sret decode and privilege checks in xret. | Prashanth Mundkur | |
| 2018-05-03 | Add implementation of sfence with a fixme note. | Prashanth Mundkur | |
| 2018-05-03 | Fix a bug in privilege transition, add better transition logging. | Prashanth Mundkur | |
| 2018-05-03 | Implement wfi, and cleanup handling illegal operations. | Prashanth Mundkur | |
| 2018-05-03 | Fix interrupt dispatch, improve execution logs, cleanup unused bits. | Prashanth Mundkur | |
| 2018-05-03 | Simplify the top-level execute loop using the step function. | Prashanth Mundkur | |
| 2018-05-03 | Fix up interrupt and exception dispatch. | Prashanth Mundkur | |
| 2018-05-03 | Implement fetch to properly handle RVC and address translation, and add a ↵ | Prashanth Mundkur | |
| step function for execution. | |||
| 2018-05-03 | Fix duopod with latest riscv prelude | Alasdair Armstrong | |
| 2018-05-03 | Hook in address translation for stores and atomics. | Prashanth Mundkur | |
| 2018-05-03 | Log csr writes in the execution log. | Prashanth Mundkur | |
| 2018-05-02 | Hook in address translation for loads. | Prashanth Mundkur | |
| 2018-05-02 | Finish up Sv39 address translation. | Prashanth Mundkur | |
| 2018-05-02 | Tick cycle counter in execute loop. | Prashanth Mundkur | |
| 2018-05-02 | Fix printing of csr immediates. | Prashanth Mundkur | |
| 2018-05-02 | Fix typo in riscv model. | Prashanth Mundkur | |
| 2018-04-26 | Add riscv SV39 page-table walk. | Prashanth Mundkur | |
| 2018-04-26 | Ensure riscv interrupt delegation does not reduce current privilege. | Prashanth Mundkur | |
| 2018-04-26 | Fix bug introduced in alignment check. | Prashanth Mundkur | |
| 2018-04-26 | Initial support for faults of writes to physical addresses. | Prashanth Mundkur | |
| 2018-04-26 | Initial support for faults of reads to physical addresses. | Prashanth Mundkur | |
| 2018-04-23 | Make riscv build depend on Makefile updates. | Prashanth Mundkur | |
| 2018-04-23 | Add riscv PTE definitions and access control checks. | Prashanth Mundkur | |
| 2018-04-20 | Fix a typo. | Prashanth Mundkur | |
| 2018-04-20 | Add a riscv instruction printer for the execution log. | Prashanth Mundkur | |
| 2018-04-20 | Some cleanup and comments. | Prashanth Mundkur | |
| 2018-04-20 | Have sign_extend in common Sail Lem library, use it and zero_extend in | Brian Campbell | |
| mono rewrites | |||
| 2018-04-18 | Remove obsolete comment. | Prashanth Mundkur | |
| 2018-04-18 | Add interrupt prioritization and delegation. | Prashanth Mundkur | |
| 2018-04-18 | Fix mideleg semantics after spec clarification from Andrew Waterman. | Prashanth Mundkur | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |