| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-02-21 | Add barriers to regfp.sail for full ARMv8 | Alasdair Armstrong | |
| Again use an $ifdef to avoid breaking RMEM. We can't use the same barrier_kind, because we *really* want a plain enumeration both for its simple SMT representation and a simple 1 to 1 mapping to the cat models used by herd. Technically for Isla, all the read_kind/write_kind/barrier_kind etc types can be defined separately on a per-architecture basis anyway, so maybe using this file at all is a bit of an anachronism. | |||
| 2020-02-03 | Add an __instr_announce builtin in regfp.sail | Alasdair Armstrong | |
| Allows keeping track of which instructions actually get executed in a trace | |||
| 2020-02-03 | Update regfp.sail with ifetch changes from poly_mapping branch | Alasdair Armstrong | |
| However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because otherwise the generated lem for RMEM will break. | |||
| 2019-07-31 | Remove redundant ifdef and run SMT tests by default | Alasdair Armstrong | |
| 2019-07-18 | Add a feature flag for barrier type change | Alasdair Armstrong | |
| Fix SMT mem_builtin test case | |||
| 2019-07-18 | Update aarch64_small to build with new barriers | Alasdair Armstrong | |
| Make sure barrier changes don't affect other models for now | |||
| 2019-07-18 | Support DMB/DSB domains | Shaked Flur | |
| 2019-05-17 | SMT: Finish adding all memory builtins from lib/regfp.sail | Alasdair Armstrong | |
| 2019-05-14 | Add feature that allows functions to require type variables are constant | Alasdair Armstrong | |
| can now write e.g. forall (constant 'n : Int) rather than forall ('n: Int) which requires 'n to be a constant integer value whenever the function is called. I added this to the 'addrsize variable on memory reads/writes to absolutely guarantee in the SMT generation that we don't have to worry about the address being a variable length bitvector. | |||
| 2019-05-13 | fix typo in excl_res extern | Jon French | |
| 2019-04-18 | Parameterise memory read/write primitives by address length | Jon French | |
| 2019-04-12 | lib/regfp.sail: add explicit C binding for memory access functions | Jon French | |
| 2019-03-14 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2019-03-13 | lib/regfp.sail: new standard intrinsics for triggering memory effects | Jon French | |
| 2019-03-08 | Adds the DC and IC instructions to AArch64_small; | Shaked Flur | |
| Also, removes etc/regfp.sail and etc/regfp2.sail in favour of lib/regfp.sail | |||
| 2018-12-28 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-12-22 | Added RISC-V fence.tso | Shaked Flur | |
| 2018-10-24 | Interpreter, RISC-V: move memory actions to parts of the interpreter ↵ | Jon French | |
| response and refactor RISC-V model accordingly | |||
| 2018-07-05 | restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵ | Jon French | |
| cleanly | |||
| 2018-06-21 | add PMP registers to CSR, fix build | Jon French | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |