From 4912a35cb945224222d55d0ef0df64f40c096298 Mon Sep 17 00:00:00 2001 From: KotorinMinami Date: Tue, 12 Nov 2024 11:47:13 +0800 Subject: [PATCH] use newtype to reflect address type --- Makefile | 2 +- model/prelude_mem.sail | 12 +++---- model/prelude_mem_addrtype.sail | 18 +++++++++++ model/riscv_addr_checks.sail | 8 ++--- model/riscv_addr_checks_common.sail | 10 +++--- model/riscv_fetch.sail | 3 +- model/riscv_fetch_rvfi.sail | 3 +- model/riscv_insts_aext.sail | 10 +++--- model/riscv_insts_base.sail | 16 +++++---- model/riscv_insts_fext.sail | 8 ++--- model/riscv_jalr_seq.sail | 4 +-- model/riscv_mem.sail | 50 ++++++++++++++--------------- model/riscv_platform.sail | 36 ++++++++++----------- model/riscv_pmp_control.sail | 6 ++-- model/riscv_step.sail | 2 +- model/riscv_sys_control.sail | 2 +- model/riscv_vmem.sail | 18 +++++------ 17 files changed, 115 insertions(+), 93 deletions(-) create mode 100644 model/prelude_mem_addrtype.sail diff --git a/Makefile b/Makefile index 4f3b63af5..607d3eee8 100644 --- a/Makefile +++ b/Makefile @@ -97,7 +97,7 @@ SAIL_VM_SRCS += riscv_vmem_tlb.sail SAIL_VM_SRCS += riscv_vmem.sail # Non-instruction sources -PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail +PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_addrtype.sail prelude_mem_metadata.sail prelude_mem.sail SAIL_REGS_SRCS = riscv_csr_begin.sail # Start of CSR scattered definitions. SAIL_REGS_SRCS += riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 03ac69e29..17813b93e 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -90,9 +90,9 @@ instantiation sail_mem_write with */ type max_mem_access : Int = 4096 -val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool +val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n), bits(8 * 'n), mem_meta) -> bool -function write_ram(wk, addr, width, data, meta) = { +function write_ram(wk, physaddr(addr), width, data, meta) = { let request : Mem_write_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { access_kind = match wk { Write_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }), @@ -125,14 +125,14 @@ function write_ram(wk, addr, width, data, meta) = { } } -val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n)) -> unit -function write_ram_ea(wk, addr, width) = () +val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n)) -> unit +function write_ram_ea(wk, physaddr(addr), width) = () instantiation sail_mem_read with pa_bits = xlenbits_identity -val read_ram : forall 'n, 0 < 'n <= max_mem_access. (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta) -function read_ram(rk, addr, width, read_meta) = { +val read_ram : forall 'n, 0 < 'n <= max_mem_access. (read_kind, physaddr, int('n), bool) -> (bits(8 * 'n), mem_meta) +function read_ram(rk, physaddr(addr), width, read_meta) = { let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta; let request : Mem_read_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { access_kind = match rk { diff --git a/model/prelude_mem_addrtype.sail b/model/prelude_mem_addrtype.sail new file mode 100644 index 000000000..c1b325d3e --- /dev/null +++ b/model/prelude_mem_addrtype.sail @@ -0,0 +1,18 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* Note: virtaddr includes physical addresses when address translation is disabled. + * It is used where the address would be virtual if address translation is active. + */ + +newtype physaddr = physaddr : xlenbits +newtype virtaddr = virtaddr : xlenbits + +function physaddr_bits(physaddr(paddr) : physaddr) -> xlenbits = paddr + +function virtaddr_bits(virtaddr(vaddr) : virtaddr) -> xlenbits = vaddr diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index 0d29d4ca4..991a9f280 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -18,7 +18,7 @@ type ext_fetch_addr_error = unit * any address translation errors are reported for pc, not the returned value. */ function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error) = - Ext_FetchAddr_OK(pc) + Ext_FetchAddr_OK(virtaddr(pc)) function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit = () @@ -38,11 +38,11 @@ type ext_control_addr_error = unit /* the control address is derived from a non-PC register, e.g. in JALR */ function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = - Ext_ControlAddr_OK(pc) + Ext_ControlAddr_OK(virtaddr(pc)) /* the control address is derived from the PC register, e.g. in JAL */ function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = - Ext_ControlAddr_OK(pc) + Ext_ControlAddr_OK(virtaddr(pc)) function ext_handle_control_check_error(err : ext_control_addr_error) -> unit = () @@ -56,7 +56,7 @@ type ext_data_addr_error = unit Extensions might override and add additional checks. */ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(1, max_mem_access)) -> Ext_DataAddr_Check(ext_data_addr_error) = - let addr = X(base) + offset in + let addr = virtaddr(X(base) + offset) in Ext_DataAddr_OK(addr) function ext_handle_data_check_error(err : ext_data_addr_error) -> unit = diff --git a/model/riscv_addr_checks_common.sail b/model/riscv_addr_checks_common.sail index b7a269842..a3d0219a4 100644 --- a/model/riscv_addr_checks_common.sail +++ b/model/riscv_addr_checks_common.sail @@ -15,17 +15,17 @@ */ union Ext_FetchAddr_Check ('a : Type) = { - Ext_FetchAddr_OK : xlenbits, /* PC value to use for the actual fetch */ + Ext_FetchAddr_OK : virtaddr, /* PC value to use for the actual fetch */ Ext_FetchAddr_Error : 'a } union Ext_ControlAddr_Check ('a : Type) = { - Ext_ControlAddr_OK : xlenbits, /* PC value to use for the target of the control operation */ + Ext_ControlAddr_OK : virtaddr, /* PC value to use for the target of the control operation */ Ext_ControlAddr_Error : 'a } union Ext_DataAddr_Check ('a : Type) = { - Ext_DataAddr_OK : xlenbits, /* Address to use for the data access */ + Ext_DataAddr_OK : virtaddr, /* Address to use for the data access */ Ext_DataAddr_Error : 'a } @@ -40,7 +40,7 @@ union Ext_PhysAddr_Check = { * return Some(exception) to abort the read or None to allow it to proceed. The * check is performed after PMP checks and does not apply to MMIO memory. */ -val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check +val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), physaddr, int('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check /*! * Validate a write to physical memory. @@ -48,4 +48,4 @@ val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType * to abort the write or None to allow it to proceed. The check is performed * after PMP checks and does not apply to MMIO memory. */ -val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check +val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, physaddr, int('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 170c38712..8cc34c893 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -19,7 +19,8 @@ function fetch() -> FetchResult = match ext_fetch_check_pc(PC, PC) { Ext_FetchAddr_Error(e) => F_Ext_Error(e), Ext_FetchAddr_OK(use_pc) => { - if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_Zca)))) + let use_pc_bits = virtaddr_bits(use_pc); + if (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(extensionEnabled(Ext_Zca)))) then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index b81d43915..d41a3abc9 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -17,7 +17,8 @@ function fetch() -> FetchResult = { Ext_FetchAddr_Error(e) => F_Ext_Error(e), Ext_FetchAddr_OK(use_pc) => { /* then check PC alignment */ - if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_Zca)))) + let use_pc_bits = virtaddr_bits(use_pc); + if (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(extensionEnabled(Ext_Zca)))) then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 17863b820..e8698aea7 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -86,13 +86,13 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { /* "LR faults like a normal load, even though it's in the AMO major opcode space." * - Andrew Waterman, isa-dev, 10 Jul 2018. */ - if not(is_aligned(vaddr, width)) + if not(is_aligned(virtaddr_bits(vaddr), width)) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) { - MemValue(result) => { load_reservation(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS }, + MemValue(result) => { load_reservation(physaddr_bits(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } }, } @@ -131,7 +131,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - if not(is_aligned(vaddr, width)) + if not(is_aligned(virtaddr_bits(vaddr), width)) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } else { match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here: @@ -139,7 +139,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { // Check reservation with physical address. - if not(match_reservation(addr)) then { + if not(match_reservation(physaddr_bits(addr))) then { /* cannot happen in rmem */ X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS } else { @@ -202,7 +202,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - if not(is_aligned(vaddr, width)) + if not(is_aligned(virtaddr_bits(vaddr), width)) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr, ReadWrite(Data, Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 1510dd425..c9becf1b7 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -72,13 +72,14 @@ function clause execute (RISCV_JAL(imm, rd)) = { }, Ext_ControlAddr_OK(target) => { /* Perform standard alignment check */ - if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca)) + let target_bits = virtaddr_bits(target); + if bit_to_bool(target_bits[1]) & not(extensionEnabled(Ext_Zca)) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL } else { X(rd) = get_next_pc(); - set_next_pc(target); + set_next_pc(target_bits); RETIRE_SUCCESS } } @@ -136,11 +137,12 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = { RETIRE_FAIL }, Ext_ControlAddr_OK(target) => { - if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca)) then { + let target_bits = virtaddr_bits(target); + if bit_to_bool(target_bits[1]) & not(extensionEnabled(Ext_Zca)) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL; } else { - set_next_pc(target); + set_next_pc(target_bits); RETIRE_SUCCESS } } @@ -317,8 +319,8 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool = } // Return true if the address is misaligned and we don't support misaligned access. -function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = - not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width)) +function check_misaligned(vaddr : virtaddr, width : word_width) -> bool = + not(plat_enable_misaligned_access()) & not(is_aligned(virtaddr_bits(vaddr), width)) function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let offset : xlenbits = sign_extend(imm); @@ -678,7 +680,7 @@ mapping clause encdec = EBREAK() <-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute EBREAK() = { - handle_mem_exception(PC, E_Breakpoint()); + handle_mem_exception(virtaddr(PC), E_Breakpoint()); RETIRE_FAIL } diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 966338db8..a543570db 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -290,7 +290,7 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if extensionEnabled /* Execution semantics ================================ */ -val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64))) +val process_fload64 : (regidx, virtaddr, MemoryOpResult(bits(64))) -> Retired function process_fload64(rd, addr, value) = if flen == 64 @@ -303,7 +303,7 @@ function process_fload64(rd, addr, value) = RETIRE_FAIL } -val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32))) +val process_fload32 : (regidx, virtaddr, MemoryOpResult(bits(32))) -> Retired function process_fload32(rd, addr, value) = match value { @@ -311,7 +311,7 @@ function process_fload32(rd, addr, value) = MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } -val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16))) +val process_fload16 : (regidx, virtaddr, MemoryOpResult(bits(16))) -> Retired function process_fload16(rd, addr, value) = match value { @@ -376,7 +376,7 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) /* Execution semantics ================================ */ -val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired +val process_fstore : (virtaddr, MemoryOpResult(bool)) -> Retired function process_fstore(vaddr, value) = match value { MemValue(true) => { RETIRE_SUCCESS }, diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index ea41ce49c..69ae789b2 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -23,9 +23,9 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { RETIRE_FAIL }, Ext_ControlAddr_OK(addr) => { - let target = [addr with 0 = bitzero]; /* clear addr[0] */ + let target = [virtaddr_bits(addr) with 0 = bitzero]; /* clear addr[0] */ if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca)) then { - handle_mem_exception(target, E_Fetch_Addr_Align()); + handle_mem_exception(addr, E_Fetch_Addr_Align()); RETIRE_FAIL } else { X(rd) = get_next_pc(); diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 82227ad7e..2c96a2bc5 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -35,7 +35,7 @@ * per the platform memory map. */ -function is_aligned_addr forall 'n. (addr : xlenbits, width : int('n)) -> bool = +function is_aligned_addr forall 'n. (physaddr(addr) : physaddr, width : int('n)) -> bool = unsigned(addr) % width == 0 function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) = @@ -64,7 +64,7 @@ function write_kind_of_flags (aq : bool, rl : bool, con : bool) -> write_kind = } // 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 : int('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 : physaddr, 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() @@ -74,13 +74,13 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext (Read(Data), None()) => MemException(E_Load_Access_Fault()), (_, None()) => MemException(E_SAMO_Access_Fault()), (_, Some(v, m)) => { if get_config_print_mem() - then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v)); + then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(physaddr_bits(paddr)) ^ "] -> " ^ BitStr(v)); MemValue(v, m) } } } // 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) +val phys_access_check : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, physaddr, 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. @@ -91,7 +91,7 @@ function phys_access_check (t, p, paddr, width) = { function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . ( t : AccessType(ext_access_type), priv : Privilege, - paddr : xlenbits, + paddr : physaddr, width : int('n), aq : bool, rl : bool, @@ -118,8 +118,8 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . ( /* 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, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit -function rvfi_read (addr, width, result) = { +val rvfi_read : forall 'n, 'n > 0. (physaddr, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit +function rvfi_read (physaddr(addr), width, result) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { @@ -132,14 +132,14 @@ function rvfi_read (addr, width, result) = { }; } $else -val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit -function rvfi_read (addr, width, result) = () +val rvfi_read : forall 'n, 'n > 0. (physaddr, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit +function rvfi_read (physaddr(addr), width, result) = () $endif -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)) +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), physaddr, 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, physaddr, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), physaddr, 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, physaddr, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) /* The most generic memory read operation */ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = { @@ -166,15 +166,15 @@ 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, int('n), bool, bool, bool) -> MemoryOpResult(unit) +val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (physaddr, 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 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, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit -function rvfi_write (addr, width, value, meta, result) = { +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (physaddr, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit +function rvfi_write (physaddr(addr), width, value, meta, result) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { @@ -190,21 +190,21 @@ function rvfi_write (addr, width, value, meta, result) = { } } $else -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) = () +val rvfi_write : forall 'n, 'n > 0. (physaddr, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit +function rvfi_write (physaddr(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 : int('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 : physaddr, 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)); + then print_mem("mem[" ^ BitStr(physaddr_bits(paddr)) ^ "] <- " ^ BitStr(data)); result } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . ( - paddr : xlenbits, + paddr : physaddr, width : int('n), data: bits(8 * 'n), typ : AccessType(ext_access_type), @@ -237,7 +237,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . ( * 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, int('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 . (physaddr, 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()) @@ -249,12 +249,12 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl } /* Memory write with explicit Privilege, implicit AccessType and metadata */ -val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (physaddr, 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, int('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 . (physaddr, 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); @@ -262,7 +262,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, int('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (physaddr, 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) } diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 687ba3a34..c7bbaf16b 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -71,7 +71,7 @@ function phys_mem_segments() = /* Physical memory map predicates */ -function within_phys_mem forall 'n, 'n <= max_mem_access. (addr : xlenbits, width : int('n)) -> bool = { +function within_phys_mem forall 'n, 'n <= max_mem_access. (physaddr(addr) : physaddr, width : int('n)) -> bool = { /* To avoid overflow issues when physical memory extends to the end * of the addressable range, we need to perform address bound checks * on unsigned unbounded integers. @@ -99,7 +99,7 @@ function within_phys_mem forall 'n, 'n <= max_mem_access. (addr : xlenbits, widt } } -function within_clint forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = { +function within_clint forall 'n, 0 < 'n <= max_mem_access . (physaddr(addr) : physaddr, width : int('n)) -> bool = { /* To avoid overflow issues when physical memory extends to the end * of the addressable range, we need to perform address bound checks * on unsigned unbounded integers. @@ -111,10 +111,10 @@ function within_clint forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, wi & (addr_int + sizeof('n)) <= (clint_base_int + clint_size_int) } -function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = +function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (physaddr(addr) : physaddr, width : int('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) -function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = +function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (physaddr(addr) : physaddr, width : int('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) /* CLINT (Core Local Interruptor), based on Spike. */ @@ -149,8 +149,8 @@ let MTIMECMP_BASE_HI : xlenbits = zero_extend(0x04004) let MTIME_BASE : xlenbits = zero_extend(0x0bff8) let MTIME_BASE_HI : xlenbits = zero_extend(0x0bffc) -val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) -function clint_load(t, addr, width) = { +val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), physaddr, int('n)) -> MemoryOpResult(bits(8 * 'n)) +function clint_load(t, physaddr(addr), width) = { let addr = addr - plat_clint_base (); /* FIXME: For now, only allow exact aligned access. */ if addr == MSIP_BASE & ('n == 8 | 'n == 4) @@ -230,8 +230,8 @@ function clint_dispatch() -> unit = { } /* The rreg effect is due to checking mtime. */ -val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) -function clint_store(addr, width, data) = { +val clint_store: forall 'n, 'n > 0. (physaddr, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) +function clint_store(physaddr(addr), width, data) = { let addr = addr - plat_clint_base (); if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { if get_config_print_platform() @@ -331,8 +331,8 @@ function reset_htif () -> unit = { * dispatched the address. */ -val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) -function htif_load(t, paddr, width) = { +val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), physaddr, int('n)) -> MemoryOpResult(bits(8 * 'n)) +function htif_load(t, physaddr(paddr), width) = { if get_config_print_platform() then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ @@ -350,8 +350,8 @@ function htif_load(t, paddr, width) = { } /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */ -val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) -function htif_store(paddr, width, data) = { +val htif_store: forall 'n, 0 < 'n <= 8. (physaddr, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) +function htif_store(physaddr(paddr), width, data) = { if get_config_print_platform() then print_platform("htif[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data)); /* Store the written value so that we can ack it later. */ @@ -417,20 +417,20 @@ function htif_tick() = { /* Top-level MMIO dispatch */ $ifndef RVFI_DII -function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = +function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : physaddr, width : int('n)) -> bool = within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n) $else -function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = false +function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : physaddr, width : int('n)) -> bool = false $endif $ifndef RVFI_DII -function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = +function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : physaddr, width : int('n)) -> bool = within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) $else -function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = false +function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : physaddr, width : int('n)) -> bool = false $endif -function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n)) -> MemoryOpResult(bits(8 * 'n)) = +function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : physaddr, width : int('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(paddr, width) then clint_load(t, paddr, width) else if within_htif_readable(paddr, width) & (1 <= 'n) @@ -441,7 +441,7 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc _ => MemException(E_SAMO_Access_Fault()) } -function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : int('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = +function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : physaddr, width : int('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = if within_clint(paddr, width) then clint_store(paddr, width, data) else if within_htif_writable(paddr, width) & 'n <= 8 diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 433fd6606..c662da2d6 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -63,7 +63,7 @@ function pmpCheckPerms(ent, acc, priv) = { enum pmpAddrMatch = {PMP_NoMatch, PMP_PartialMatch, PMP_Match} -function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range_in_words) -> pmpAddrMatch = { +function pmpMatchAddr(physaddr(addr): physaddr, width: xlenbits, rng: pmp_addr_range_in_words) -> pmpAddrMatch = { match rng { None() => PMP_NoMatch, Some((lo, hi)) => { @@ -89,7 +89,7 @@ function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range_in_wo enum pmpMatch = {PMP_Success, PMP_Continue, PMP_Fail} -function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege, +function pmpMatchEntry(addr: physaddr, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege, ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmpMatch = { let rng = pmpAddrRange(ent, pmpaddr, prev_pmpaddr); match pmpMatchAddr(addr, width, rng) { @@ -111,7 +111,7 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType = Execute() => E_Fetch_Access_Fault(), } -function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: int('n), acc: AccessType(ext_access_type), priv: Privilege) +function pmpCheck forall 'n, 'n > 0. (addr: physaddr, width: int('n), acc: AccessType(ext_access_type), priv: Privilege) -> option(ExceptionType) = { let width : xlenbits = to_bits(xlen, width); diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 21bd82e47..9f8e919cc 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -41,7 +41,7 @@ function step(step_no : int) -> bool = { }, /* standard error */ F_Error(e, addr) => { - handle_mem_exception(addr, e); + handle_mem_exception(virtaddr(addr), e); (RETIRE_FAIL, false) }, /* non-error cases: */ diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index d370f0400..28731f6be 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -326,7 +326,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, } } -function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = { +function handle_mem_exception(virtaddr(addr) : virtaddr, e : ExceptionType) -> unit = { let t : sync_exception = struct { trap = e, excinfo = Some(addr), ext = None() } in diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index 17a44c268..64fe15696 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -101,7 +101,7 @@ function pt_walk(sv_params, // Below, 'pte_phys_addr' is XLEN bits because it's an arg to // 'mem_read_priv()' [riscv_mem.sail] where it's declared as xlenbits. // That def and this use need to be fixed together (TODO) - let pte_phys_addr : xlenbits = pte_addr[(xlen - 1) .. 0]; + let pte_phys_addr : physaddr = physaddr(pte_addr[(xlen - 1) .. 0]); // Read this-level PTE from mem let mem_result = mem_read_priv(Read(Data), // AccessType @@ -270,7 +270,7 @@ function translationMode(priv : Privilege) -> SATPMode = { // for Sv32 where they are actually 32 bits. `pte_size` is used to indicate // the actual size in bytes that we want to write. function write_pte forall 'n, 'n in {4, 8} . ( - paddr : xlenbits, + paddr : physaddr, pte_size : int('n), pte : bits(64), ) -> MemoryOpResult(bool) = @@ -320,7 +320,7 @@ function translate_TLB_hit(sv_params : SV_Params, // Writeback the PTE (which has new A/D bits) let n_ent = {ent with pte=pte'}; write_TLB(tlb_index, n_ent); - let pte_phys_addr = ent.pteAddr[(xlen - 1) .. 0]; + let pte_phys_addr = physaddr(ent.pteAddr[(xlen - 1) .. 0]); match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => (), @@ -366,7 +366,7 @@ function translate_TLB_miss(sv_params : SV_Params, TR_Failure(PTW_PTE_Update(), ext_ptw) else { // Writeback the PTE (which has new A/D bits) - let pte_phys_addr = pteAddr[(xlen - 1) .. 0]; + let pte_phys_addr = physaddr(pteAddr[(xlen - 1) .. 0]); match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => { @@ -407,18 +407,18 @@ function translate(sv_params : SV_Params, // Top-level addr-translation function // PUBLIC: invoked from instr-fetch and load/store/amo -function translateAddr(vAddr : xlenbits, +function translateAddr(vAddr : virtaddr, ac : AccessType(ext_access_type)) - -> TR_Result(xlenbits, ExceptionType) = { + -> TR_Result(physaddr, ExceptionType) = { // Internally the vmem code works with 64-bit values, whether xlen==32 or xlen==64 // This 'extend' is a no-op when xlen==64 and extends when xlen==32 - let vAddr_64b : bits(64) = zero_extend(vAddr); + let vAddr_64b : bits(64) = zero_extend(virtaddr_bits(vAddr)); // Effective privilege takes into account mstatus.PRV, mstatus.MPP // See riscv_sys_regs.sail for effectivePrivilege() and cur_privilege let effPriv : Privilege = effectivePrivilege(ac, mstatus, cur_privilege); let mode : SATPMode = translationMode(effPriv); let (valid_va, sv_params) : (bool, SV_Params) = match mode { - Sbare => return TR_Address(vAddr, init_ext_ptw), + Sbare => return TR_Address(physaddr(virtaddr_bits(vAddr)), init_ext_ptw), Sv32 => (true, sv32_params), Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params), Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params), @@ -439,7 +439,7 @@ function translateAddr(vAddr : xlenbits, init_ext_ptw); // Fixup result PA or exception match tr_result1 { - TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, xlen), ext_ptw), + TR_Address(pa, ext_ptw) => TR_Address(physaddr(truncate(pa, xlen)), ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } }