diff options
Diffstat (limited to 'model/riscv_mem.sail')
| -rw-r--r-- | model/riscv_mem.sail | 258 |
1 files changed, 102 insertions, 156 deletions
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 0f36dee..ccf4d2f 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -1,71 +1,9 @@ /*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ /* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ /* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ +/* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ /* Physical memory model. @@ -97,7 +35,7 @@ * per the platform memory map. */ -function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool = +function is_aligned_addr forall 'n. (addr : xlenbits, width : int('n)) -> bool = unsigned(addr) % width == 0 function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) = @@ -112,8 +50,21 @@ function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_ki (false, true, true) => None() } +function write_kind_of_flags (aq : bool, rl : bool, con : bool) -> write_kind = + match (aq, rl, con) { + (false, false, false) => Write_plain, + (false, true, false) => Write_RISCV_release, + (false, false, true) => Write_RISCV_conditional, + (false, true , true) => Write_RISCV_conditional_release, + (true, true, false) => Write_RISCV_strong_release, + (true, true , true) => Write_RISCV_conditional_strong_release, + // throw an illegal instruction here? + (true, false, false) => throw(Error_not_implemented("store.aq")), + (true, false, true) => throw(Error_not_implemented("sc.aq")) + } + // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = { +function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = { let result = (match read_kind_of_flags(aq, rl, res) { Some(rk) => Some(read_ram(rk, paddr, width, meta)), None() => None() @@ -128,63 +79,74 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext } } -/* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = - if within_mmio_readable(paddr, width) - then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta) - else if within_phys_mem(paddr, width) - then match ext_check_phys_mem_read(t, paddr, width, aq, rl, res, meta) { - Ext_PhysAddr_OK() => phys_mem_read(t, paddr, width, aq, rl, res, meta), - Ext_PhysAddr_Error(e) => MemException(e) - } else match t { - Execute() => MemException(E_Fetch_Access_Fault()), - Read(Data) => MemException(E_Load_Access_Fault()), - _ => MemException(E_SAMO_Access_Fault()) - } +// Check if access is permitted according to PMPs and PMAs. +val phys_access_check : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n)) -> option(ExceptionType) +function phys_access_check (t, p, paddr, width) = { + let pmpError : option(ExceptionType) = if sys_pmp_count() == 0 then None() else pmpCheck(paddr, width, t, p); + // TODO: Also check PMAs and select the highest priority fault. + pmpError +} -/* PMP checks if enabled */ -function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = - if not(plat_enable_pmp()) - then checked_mem_read(t, paddr, width, aq, rl, res, meta) - else { - match pmpCheck(paddr, width, t, p) { - None() => checked_mem_read(t, paddr, width, aq, rl, res, meta), - Some(e) => MemException(e) +/* dispatches to MMIO regions or physical memory regions depending on physical memory map */ +function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . ( + t : AccessType(ext_access_type), + priv : Privilege, + paddr : xlenbits, + width : int('n), + aq : bool, + rl : bool, + res: bool, + meta : bool, +) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = + match phys_access_check(t, priv, paddr, width) { + Some(e) => MemException(e), + None() => { + if within_mmio_readable(paddr, width) + then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta) + else if within_phys_mem(paddr, width) + then match ext_check_phys_mem_read(t, paddr, width, aq, rl, res, meta) { + Ext_PhysAddr_OK() => phys_mem_read(t, paddr, width, aq, rl, res, meta), + Ext_PhysAddr_Error(e) => MemException(e) + } else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } } } /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ $ifdef RVFI_DII -val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit +val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit function rvfi_read (addr, width, result) = { - rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { /* TODO: report tag bit for capability writes and extend mask by one bit. */ MemValue(v, _) => if width <= 16 - then { rvfi_mem_data->rvfi_mem_rdata() = sail_zero_extend(v, 256); - rvfi_mem_data->rvfi_mem_rmask() = rvfi_encode_width_mask(width) } + then { rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(v, 256); + rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width) } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") }, MemException(_) => () }; } $else -val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit +val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit function rvfi_read (addr, width, result) = () $endif /* NOTE: The rreg effect is due to MMIO. */ $ifdef RVFI_DII -val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) -val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) $else -val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) -val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) $endif /* The most generic memory read operation */ @@ -195,7 +157,7 @@ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = { else match (aq, rl, res) { (false, true, false) => throw(Error_not_implemented("load.rl")), (false, true, true) => throw(Error_not_implemented("lr.rl")), - (_, _, _) => pmp_mem_read(typ, priv, paddr, width, aq, rl, res, meta) + (_, _, _) => checked_mem_read(typ, priv, paddr, width, aq, rl, res, meta) }; rvfi_read(paddr, width, result); result @@ -212,34 +174,23 @@ function mem_read_priv (typ, priv, paddr, width, aq, rl, res) = function mem_read (typ, paddr, width, aq, rel, res) = mem_read_priv(typ, effectivePrivilege(typ, mstatus, cur_privilege), paddr, width, aq, rel, res) -val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) - -function mem_write_ea (addr, width, aq, rl, con) = { +val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(unit) +function mem_write_ea (addr, width, aq, rl, con) = if (rl | con) & not(is_aligned_addr(addr, width)) then MemException(E_SAMO_Addr_Align()) - else match (aq, rl, con) { - (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)), - (false, true, false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)), - (false, false, true) => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)), - (false, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)), - (true, false, false) => throw(Error_not_implemented("store.aq")), - (true, true, false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)), - (true, false, true) => throw(Error_not_implemented("sc.aq")), - (true, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width)) - } -} + else MemValue(write_ram_ea(write_kind_of_flags(aq, rl, con), addr, width)) $ifdef RVFI_DII -val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit function rvfi_write (addr, width, value, meta, result) = { - rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { /* Log only the memory address (without the value) if the write fails. */ MemValue(_) => if width <= 16 then { /* TODO: report tag bit for capability writes and extend mask by one bit. */ - rvfi_mem_data->rvfi_mem_wdata() = sail_zero_extend(value,256); - rvfi_mem_data->rvfi_mem_wmask() = rvfi_encode_width_mask(width); + rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value,256); + rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width); } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); }, @@ -247,12 +198,12 @@ function rvfi_write (addr, width, value, meta, result) = { } } $else -val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit +val rvfi_write : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit function rvfi_write (addr, width, value, meta, result) = () $endif // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { +function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { let result = MemValue(write_ram(wk, paddr, width, data, meta)); if get_config_print_mem() then print_mem("mem[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data)); @@ -260,24 +211,30 @@ function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) = - if within_mmio_writable(paddr, width) - then mmio_write(paddr, width, data) - else if within_phys_mem(paddr, width) - then match ext_check_phys_mem_write (wk, paddr, width, data, meta) { - Ext_PhysAddr_OK() => phys_mem_write(wk, paddr, width, data, meta), - Ext_PhysAddr_Error(e) => MemException(e) - } - else MemException(E_SAMO_Access_Fault()) - -/* PMP checks if enabled */ -function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) = - if not(plat_enable_pmp()) - then checked_mem_write(wk, paddr, width, data, meta) - else { - match pmpCheck(paddr, width, typ, priv) { - None() => checked_mem_write(wk, paddr, width, data, meta), - Some(e) => MemException(e) +function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . ( + paddr : xlenbits, + width : int('n), + data: bits(8 * 'n), + typ : AccessType(ext_access_type), + priv : Privilege, + meta: mem_meta, + aq : bool, + rl : bool, + con : bool, +) -> MemoryOpResult(bool) = + match phys_access_check(typ, priv, paddr, width) { + Some(e) => MemException(e), + None() => { + if within_mmio_writable(paddr, width) + then mmio_write(paddr, width, data) + else if within_phys_mem(paddr, width) + then { + let wk = write_kind_of_flags(aq, rl, con); + match ext_check_phys_mem_write (wk, paddr, width, data, meta) { + Ext_PhysAddr_OK() => phys_mem_write(wk, paddr, width, data, meta), + Ext_PhysAddr_Error(e) => MemException(e), + } + } else MemException(E_SAMO_Access_Fault()) } } @@ -288,35 +245,24 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, pa * data. * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */ -val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl, con) = { if (rl | con) & not(is_aligned_addr(paddr, width)) then MemException(E_SAMO_Addr_Align()) else { - let wk : write_kind = match (aq, rl, con) { - (false, false, false) => Write_plain, - (false, true, false) => Write_RISCV_release, - (false, false, true) => Write_RISCV_conditional, - (false, true , true) => Write_RISCV_conditional_release, - (true, true, false) => Write_RISCV_strong_release, - (true, true , true) => Write_RISCV_conditional_strong_release, - // throw an illegal instruction here? - (true, false, false) => throw(Error_not_implemented("store.aq")), - (true, false, true) => throw(Error_not_implemented("sc.aq")) - }; - let result = pmp_mem_write(wk, paddr, width, value, typ, priv, meta); + let result = checked_mem_write(paddr, width, value, typ, priv, meta, aq, rl, con); rvfi_write(paddr, width, value, meta, result); result } } /* Memory write with explicit Privilege, implicit AccessType and metadata */ -val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value_priv (paddr, width, value, priv, aq, rl, con) = mem_write_value_priv_meta(paddr, width, value, Write(default_write_acc), priv, default_meta, aq, rl, con) /* Memory write with explicit metadata and AccessType, implicit and Privilege */ -val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = { let typ = Write(ext_acc); let ep = effectivePrivilege(typ, mstatus, cur_privilege); @@ -324,7 +270,7 @@ function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) } /* Memory write with default AccessType, Privilege, and metadata */ -val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value (paddr, width, value, aq, rl, con) = { mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con) } |