diff options
Diffstat (limited to 'riscv/prelude.sail')
| -rw-r--r-- | riscv/prelude.sail | 31 |
1 files changed, 28 insertions, 3 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 9ec1d86d..d99581a7 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -366,11 +366,36 @@ function __RISCV_write (addr, width, data) = { val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val __ReadRAM = "read_ram" : forall 'n 'm. +val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __RISCV_read : forall 'n. (bits(64), atom('n)) -> option(bits(8 * 'n)) effect {rmem} -function __RISCV_read (addr, width) = Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)) +val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __RISCV_read : forall 'n. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} +function __RISCV_read (addr, width, aq, rl, res) = + match (aq, rl, res) { + (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)), + (true, false, false) => Some(__ReadRAM_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (true, true, false) => Some(__ReadRAM_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (false, false, true) => Some(__ReadRAM_reserved(64, width, 0x0000_0000_0000_0000, addr)), + (true, false, true) => Some(__ReadRAM_reserved_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (true, true, true) => Some(__ReadRAM_reserved_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (false, true, false) => None(), + (false, true, true) => None() + } val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit |