diff options
author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-01-09 16:37:35 +0000 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-08 14:24:07 -0800 |
commit | 6e95fa391ba745f426805447b7ac760f6eaee551 (patch) | |
tree | 77fdb9329df440ddeb0e6beaaa1af9ea19fffd51 /model | |
parent | 10a0095336804ab33b473d021b8501d30ac38ae7 (diff) | |
download | sail-riscv-6e95fa391ba745f426805447b7ac760f6eaee551.zip sail-riscv-6e95fa391ba745f426805447b7ac760f6eaee551.tar.gz sail-riscv-6e95fa391ba745f426805447b7ac760f6eaee551.tar.bz2 |
Adapt to changes in Sail's Lem shallow embedding
In the monads branch of Sail, writing a memory value now requires
address and write_kind (instead of relying on parameters announced
earlier).
Diffstat (limited to 'model')
-rw-r--r-- | model/prelude.sail | 33 | ||||
-rw-r--r-- | model/riscv_mem.sail | 51 | ||||
-rw-r--r-- | model/riscv_vmem.sail | 4 |
3 files changed, 36 insertions, 52 deletions
diff --git a/model/prelude.sail b/model/prelude.sail index 4f5b98a..91efcc0 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -268,13 +268,36 @@ overload min = {min_nat, min_int} overload max = {max_nat, max_int} -val __WriteRAM = "write_ram" : forall 'n 'm. +val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} -val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmv} -function __RISCV_write (addr, width, data) = { - __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) -} +val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv} +function __RISCV_write (addr, width, data, aq, rl, con) = + match (aq, rl, con) { + (false, false, false) => __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data), + (false, true, false) => __WriteRAM_release(64, width, 0x0000_0000_0000_0000, addr, data), + (false, false, true) => __WriteRAM_conditional(64, width, 0x0000_0000_0000_0000, addr, data), + (false, true, true) => __WriteRAM_conditional_release(64, width, 0x0000_0000_0000_0000, addr, data), + (true, true, false) => __WriteRAM_strong_release(64, width, 0x0000_0000_0000_0000, addr, data), + (true, true, true) => __WriteRAM_conditional_strong_release(64, width, 0x0000_0000_0000_0000, addr, data), + (true, false, false) => false, + (true, false, true) => false + } val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 0b3e550..3549e80 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -26,20 +26,6 @@ function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, wid /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ -val MEMr : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -val MEMr_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -val MEMr_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -val MEMr_reserved : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -val MEMr_reserved_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -val MEMr_reserved_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} - -function MEMr (addr, width) = checked_mem_read(Data, addr, width, false, false, false) -function MEMr_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, false) -function MEMr_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, false) -function MEMr_reserved (addr, width) = checked_mem_read(Data, addr, width, false, false, true) -function MEMr_reserved_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, true) -function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, true) - $ifdef RVFI_DII val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult(bits(8 * 'n))) -> unit effect {wreg} function rvfi_read (addr, width, result) = { @@ -71,14 +57,9 @@ function mem_read (addr, width, aq, rl, res) = { if (aq | res) & (~ (is_aligned_addr(addr, width))) then MemException(E_Load_Addr_Align) else match (aq, rl, res) { - (false, false, false) => checked_mem_read(Data, addr, width, false, false, false), - (true, false, false) => MEMr_acquire(addr, width), - (false, false, true) => MEMr_reserved(addr, width), - (true, false, true) => MEMr_reserved_acquire(addr, width), (false, true, false) => throw(Error_not_implemented("load.rl")), - (true, true, false) => MEMr_strong_acquire(addr, width), (false, true, true) => throw(Error_not_implemented("lr.rl")), - (true, true, true) => MEMr_reserved_strong_acquire(addr, width) + (_, _, _) => checked_mem_read(Data, addr, width, aq, rl, res) }; rvfi_read(addr, width, result); result @@ -115,36 +96,21 @@ function mem_write_ea (addr, width, aq, rl, con) = { } // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = { +function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = { print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); - MemValue(__RISCV_write(addr, width, data)) + MemValue(__RISCV_write(addr, width, data, aq, rl, con)) } // dispatches to MMIO regions or physical memory regions depending on physical memory map -function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = +function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = if within_mmio_writable(addr, width) then mmio_write(addr, width, data) else if within_phys_mem(addr, width) - then phys_mem_write(addr, width, data) + then phys_mem_write(addr, width, data, aq, rl, con) else MemException(E_SAMO_Access_Fault) /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ -val MEMval : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} -val MEMval_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} -val MEMval_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} -val MEMval_conditional : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} -val MEMval_conditional_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} -val MEMval_conditional_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} - -function MEMval (addr, width, data) = checked_mem_write(addr, width, data) -function MEMval_release (addr, width, data) = checked_mem_write(addr, width, data) -function MEMval_strong_release (addr, width, data) = checked_mem_write(addr, width, data) -function MEMval_conditional (addr, width, data) = checked_mem_write(addr, width, data) -function MEMval_conditional_release (addr, width, data) = checked_mem_write(addr, width, data) -function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data) - - $ifdef RVFI_DII val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wreg} function rvfi_write (addr, width, value) = { @@ -167,14 +133,9 @@ function mem_write_value (addr, width, value, aq, rl, con) = { if (rl | con) & (~ (is_aligned_addr(addr, width))) then MemException(E_SAMO_Addr_Align) else match (aq, rl, con) { - (false, false, false) => checked_mem_write(addr, width, value), - (false, true, false) => MEMval_release(addr, width, value), - (false, false, true) => MEMval_conditional(addr, width, value), - (false, true, true) => MEMval_conditional_release(addr, width, value), (true, false, false) => throw(Error_not_implemented("store.aq")), - (true, true, false) => MEMval_strong_release(addr, width, value), (true, false, true) => throw(Error_not_implemented("sc.aq")), - (true, true, true) => MEMval_conditional_strong_release(addr, width, value) + (_, _, _) => checked_mem_write(addr, width, value, aq, rl, con) } } diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index b617d29..ef56108 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -313,7 +313,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = { n_ent.pte = update_BITS(ent.pte, pbits.bits()); writeTLB39(idx, n_ent); /* update page table */ - match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits()) { + match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits(), false, false, false) { MemValue(_) => (), MemException(e) => internal_error("invalid physical address in TLB") }; @@ -339,7 +339,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = { TR39_Failure(PTW_PTE_Update) } else { w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); - match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) { + match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) { MemValue(_) => { addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR39_Address(pAddr) |