From f601c866153c79a7ae8404f939dc2d66aa2e41f9 Mon Sep 17 00:00:00 2001 From: "Rishiyur S. Nikhil" Date: Mon, 1 Apr 2024 11:07:57 -0400 Subject: [PATCH] Unify VM code Old vmem code had much 'cut-and-paste' replication for RV32 (Sv32) and (#408) RV64 (Sv39, Sv48), and was scattered over several files. New code unifies them into single set of parameterized functions that works for RV32/RV64 and Sv32/Sv39/Sv48 (and is ready for Sv57). Deleted old files: riscv_vmem_rv32.sail riscv_vmem_rv64.sail riscv_vmem_sv32.sail riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_pte.sail riscv_ptw.sail Current files: all named riscv_vmem_* riscv_vmem.sail (root file for vmem) riscv_vmem_common.sail riscv_vmem_pte.sail riscv_vmem_ptw.sail riscv_vmem_tlb.sail riscv_vmem_types.sail Modified top-level Makefile accordingly. Added documentation on new vmem code: doc/notes_Virtual_Memory.adoc --- Makefile | 24 +- doc/figs/notes_Virtual_Memory_Fig1.svg | 1027 +++++++++++++++++ doc/notes_Virtual_Memory.adoc | 119 ++ model/riscv_pte.sail | 92 -- model/riscv_vmem.sail | 452 ++++++++ model/riscv_vmem_common.sail | 245 ++-- model/riscv_vmem_pte.sail | 135 +++ model/{riscv_ptw.sail => riscv_vmem_ptw.sail} | 45 +- model/riscv_vmem_rv32.sail | 75 -- model/riscv_vmem_rv64.sail | 114 -- model/riscv_vmem_sv32.sail | 200 ---- model/riscv_vmem_sv39.sail | 194 ---- model/riscv_vmem_sv48.sail | 156 --- model/riscv_vmem_tlb.sail | 139 ++- 14 files changed, 1966 insertions(+), 1051 deletions(-) create mode 100644 doc/figs/notes_Virtual_Memory_Fig1.svg create mode 100644 doc/notes_Virtual_Memory.adoc delete mode 100644 model/riscv_pte.sail create mode 100644 model/riscv_vmem.sail create mode 100644 model/riscv_vmem_pte.sail rename model/{riscv_ptw.sail => riscv_vmem_ptw.sail} (59%) delete mode 100644 model/riscv_vmem_rv32.sail delete mode 100644 model/riscv_vmem_rv64.sail delete mode 100644 model/riscv_vmem_sv32.sail delete mode 100644 model/riscv_vmem_sv39.sail delete mode 100644 model/riscv_vmem_sv48.sail diff --git a/Makefile b/Makefile index 255224125..deaad558f 100644 --- a/Makefile +++ b/Makefile @@ -71,15 +71,21 @@ SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdex SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling -SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail -SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail - -SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail -ifeq ($(ARCH),RV32) -SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS) -else -SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS) -endif +# SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail +# SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail + +# SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail +# ifeq ($(ARCH),RV32) +# SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS) +# else +# SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS) +# endif + +SAIL_VM_SRCS += riscv_vmem_common.sail +SAIL_VM_SRCS += riscv_vmem_pte.sail +SAIL_VM_SRCS += riscv_vmem_ptw.sail +SAIL_VM_SRCS += riscv_vmem_tlb.sail +SAIL_VM_SRCS += riscv_vmem.sail # Non-instruction sources PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail diff --git a/doc/figs/notes_Virtual_Memory_Fig1.svg b/doc/figs/notes_Virtual_Memory_Fig1.svg new file mode 100644 index 000000000..4c5b2249c --- /dev/null +++ b/doc/figs/notes_Virtual_Memory_Fig1.svg @@ -0,0 +1,1027 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + + registersatp + + readCSR() + writeCSR() + Exec Fetch + Exec SFENCE.VMA + PUBLIC + legalize_satp() + + + + translateAddr() + union TR_Result + + + + + PRIVATE + + translate() + add_to_TLB() + write_TLB() + mem_read_priv() + mem_write_value_priv() + + PRIVATE + PUBLIC + + + registertlb + + translate_TLB_miss() + translate_TLB_hit() + lookup_TLB() + init_vmem() + init_TLB() + + + init_model() + + + + pt_walk() + + make_TLB_Entry() + match_TLB_Entry() + flush_TLB() + + flush_TLB_Entry() + + + + + + riscv_vmem.sail + riscv_vmem_tlb.sail + satp64Mode_of_Bits() + cur_privilege + effectivePrivilege() + Exec Load/Store/AMO + + plat_enable_dirty_update() + + + diff --git a/doc/notes_Virtual_Memory.adoc b/doc/notes_Virtual_Memory.adoc new file mode 100644 index 000000000..fba39a1e9 --- /dev/null +++ b/doc/notes_Virtual_Memory.adoc @@ -0,0 +1,119 @@ += Notes on the Virtual Memory part Sail RISC-V Spec + +NOTE: this is an AsciiDoc document and can be processed into + browser-readable HTML by the free, open-source tool + `asciidoctor`. + +NOTE: If you are a code maintainer, kindly update this document if + there are any significant developements in vmem code. + +This is a commentary/reader's guide to the virtual memory ("vmem") +code in the Sail RISC-V Formal Spec ("Golden Model"). The primary +vmem specification code is in file: + + model/riscv_vmem.sail + +Additional files: + + model/riscv_vmem_common.sail + model/riscv_vmem_pte.sail + model/riscv_vmem_ptw.sail + model/riscv_vmem_tlb.sail + model/riscv_vmem_types.sail + +`riscv_vmem_common.sail` contains the parameterization for Sv32, Sv39, +Sv48 and Sv57. + +`riscv_vmem_pte.sail` describes Page Table Entries, checks for +permission bits, etc. + +`riscv_vmem_ptw.sail` describes Page Table Walk exceptions. + +`riscv_vmem_tlb.sail` implements a simple TLB (Translation Look-Aside +Buffer). TLBs are not part of the RISC-V architecture spec. +Nevertheless, it is useful to model at least a minimal TLB so that we +can demonstrate and test SFENCE.VMA functionality (without TLBs, +SFENCE.VMA is a no-op and there's nothing to test). + +TLBs are also useful for sail-riscv model simulation speed. Without a +TLB, every Fetch and Load/Store/AMO in virtual memory mode requires a +full page table walk. Speed matters mostly for large simulations +(e.g., Linux-boot can speed up from tens of minutes to a few minutes). + +The main vmem code in `riscv_vmem.sail` is structured and commented to +make it is easy to ignore/skip TLB-related parts. + +`riscv_vmem_types.sail` concerns non-standard extensions to the vmem +system and can be ignored (it is used, e.g., by U.Cambridge's CHERI +system). + +// SECTION ================================================================ +== Simplified call graph + +The following figure shows a rough call graph, and this can serve as a +guide for understanding the code. + +image::./figs/notes_Virtual_Memory_Fig1.svg[align="center"] + +The yellow rectangle(s) represent the code in `riscv_vmem.sail`, and +the grey rectangle(s) represent the code in `riscv_vmem_tlb.sail`. In +each case, the lighter outer rectangle shows the publicly visible +resources ("API"), and the darker inner rectangle shows internal +(private) resources. + +On the left are shown the external places from which the vmem code is +invoked, using its public resources. On the right are shown the +external resources used by the vmem code. + +The main flow (ignoring TLBs) is at the top: The external execution +code for instruction fetch, load, store and AMO invoke +`translateAddr()` and receive a result of `TR_Result` type. +`translateAddr()`, in turn, invokes `translate()`, +`translate_TLB_miss()` and `pt_walk()`; the latter invokes the +external `mem_read_priv()` to read PTEs (Page Table Entries) from +memory. The SATP register lives in this vmem code, and is accessed by +the external general `readCSR()` and `writeCSR()` functions. + +`translate()` invokes `lookup_TLB()` and, if a hit, invokes +`translate_TLB_hit()`, avoiding a page-table walk (and therefore no +reads from memory). + +`mem_write_value_priv()` is called for writing back, to memory, PTEs +(Page Table Entries) whose A and/or D bits have been modified as part +of the access. + +// SECTION ================================================================ +== Status + +* 2024-02-18: Many stylistic updates based on PR comments. + +* 2023-11-30: Passing all ISA tests in `tests/riscv-tests` (163 for + RV32 and 229 for RV64, about half of which run with Virtual Memory). + Also passing 712 tests in GitHub CI flow. + +* 2023-11-30: Sv57 not yet implemented (the code has placeholders + for Sv57 support; search for "Sv57") + +* 2023-11-30: Sv48 or Sv57 have not been tested; we do not have any tests for them. + +// SECTION ================================================================ +== Diary notes + +2019: Original code written, primarily by https://github.com/pmundkur[@pmundkur] + +2023-11: Refactored by https://github.com/rsnikhil[@rsnikhil] for: + +* Unifying previously separate RV32/RV64, Sv32/Sv39/Sv57 code into a + single, parameterized code. +* Misc. stylistic improvements. +* Deleted older files: ++ + riscv_pte.sail + riscv_ptw.sail + riscv_vmem_common.sail + riscv_vmem_rv32.sail + riscv_vmem_rv64.sail + riscv_vmem_sv32.sail + riscv_vmem_sv39.sail + riscv_vmem_sv48.sail ++ diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail deleted file mode 100644 index 1a5bb0ecc..000000000 --- a/model/riscv_pte.sail +++ /dev/null @@ -1,92 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -/* PTE attributes, permission checks and updates */ - -type pteAttribs = bits(8) - -/* Reserved PTE bits could be used by extensions on RV64. There are - * no such available bits on RV32, so these bits will be zeros on RV32. - */ -type extPte = bits(10) - -/* - * On SV32, there are no reserved bits available to extensions. Therefore, by - * default, we initialize the PTE extension field with all zeros. However, - * extensions may wish, on SV39/48/56, to put flags in the reserved region of - * those PTEs. To avoid the need for "inhibit" bits in extensions (i.e., so - * that extensions can use the more common and more RISC-V flavored "enable" - * disposition), we allow extensions to use any constant value by overriding - * this default_sv32_ext_pte value. - */ -let default_sv32_ext_pte : extPte = zeros() - -bitfield PTE_Bits : pteAttribs = { - D : 7, - A : 6, - G : 5, - U : 4, - X : 3, - W : 2, - R : 1, - V : 0 -} - -function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = { - let a = Mk_PTE_Bits(p); - a[R] == 0b0 & a[W] == 0b0 & a[X] == 0b0 -} - -function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = { - let a = Mk_PTE_Bits(p); - a[V] == 0b0 | (a[W] == 0b1 & a[R] == 0b0) -} - -union PTE_Check = { - PTE_Check_Success : ext_ptw, - PTE_Check_Failure : (ext_ptw, ext_ptw_fail) -} - -function to_pte_check(b : bool) -> PTE_Check = - if b then PTE_Check_Success(()) else PTE_Check_Failure((), ()) - -/* For extensions: this function gets the extension-available bits of the PTE in extPte, - * and the accumulated information of the page-table-walk in ext_ptw. It should return - * the updated ext_ptw in both the success and failure cases. - */ -function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = { - match (ac, priv) { - (Read(_), User) => to_pte_check(p[U] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), - (Write(_), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1), - (ReadWrite(_, _), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), - (Execute(), User) => to_pte_check(p[U] == 0b1 & p[X] == 0b1), - - (Read(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), - (Write(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1), - (ReadWrite(_, _), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), - (Execute(), Supervisor) => to_pte_check(p[U] == 0b0 & p[X] == 0b1), - - (_, Machine) => internal_error(__FILE__, __LINE__, "m-mode mem perm check") - } -} - -function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = { - let update_d = p[D] == 0b0 & (match a { // dirty-bit - Execute() => false, - Read() => false, - Write(_) => true, - ReadWrite(_,_) => true - }); - - let update_a = p[A] == 0b0; // accessed-bit - if update_d | update_a then { - let np = update_A(p, 0b1); - let np = if update_d then update_D(np, 0b1) else np; - Some(np, ext) - } else None() -} diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail new file mode 100644 index 000000000..2d1e5d162 --- /dev/null +++ b/model/riscv_vmem.sail @@ -0,0 +1,452 @@ +/*=======================================================================================*/ +/* 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 */ +/*=======================================================================================*/ + +// **************************************************************** +// Virtual memory address translation and memory protection, +// including PTWs (Page Table Walks) and TLBs (Translation Look-aside Buffers) +// Supported VM modes: Sv32, Sv39, Sv48. TODO: Sv57 + +// STYLE NOTES: +// PRIVATE items are used only within this VM code. +// PUBLIC items are invoked from other parts of sail-riscv. + +// TLB NOTE: +// TLBs are not part of the RISC-V architecture specification. +// However, we model a simple TLB so that +// (1) we can meaningfully test SFENCE.VMA which is a no-op wihout TLBs; +// (2) we can greatly speed up simulation speed +// (e.g., from 10s or minutes to few minutes for Linux boot) +// The TLB implementation is in a separate file: riscv_vmem_tlb.sail +// The code in this file is structured and commented so you can easily +// ignore TLB functionality at first reading. + +// **************************************************************** +// Fields of virtual addresses + +// PRIVATE: Extract full VPN field from VA +function vpns_of_va(sv_params : SV_Params, + va : bits(64)) -> bits(64) = { + let mask : bits(64) = zero_extend(ones(sv_params.va_size_bits)); + (va & mask) >> pagesize_bits +} + +// PRIVATE: Extract VPN[level] from VA +function vpn_j_of_va(sv_params : SV_Params, + va : bits(64), + level : PTW_Level) -> bits(64) = { + let lsb : range(0,63) = pagesize_bits + level * sv_params.vpn_size_bits; + assert (lsb < sizeof(xlen)); + let mask : bits(64) = zero_extend(ones(sv_params.vpn_size_bits)); + ((va >> lsb) & mask) +} + +// PRIVATE: Extract offset within page from VA +function offset_of_va(va : bits(64)) -> bits(PAGESIZE_BITS) = va[pagesize_bits - 1 .. 0] + +// Valid xlen-wide values containing virtual addrs must have upper +// bits equal to the MSB of the virtual address. +// Virtual address widths depend on the virtual memory mode. +// PRIVATE +function is_valid_vAddr(struct { va_size_bits, _ } : SV_Params, + vAddr : bits(64)) -> bool = + vAddr == sign_extend(vAddr[va_size_bits - 1 .. 0]) + +// **************************************************************** +// Results of Page Table Walk (PTW) + +// PRIVATE +union PTW_Result = { + PTW_Success: (bits(64), bits(64), bits(64), nat, bool, ext_ptw), + PTW_Failure: (PTW_Error, ext_ptw) +} + +// **************************************************************** +// Page Table Walk (PTW) + +// Note: 'pt_walk()' is recursive => needs separate 'val' decls + +// PRIVATE +val pt_walk : (SV_Params, + bits(64), // virtual addr + AccessType(ext_access_type), // Read/Write/ReadWrite/Execute + Privilege, // User/Supervisor/Machine + bool, // mstatus.MXR + bool, // do_sum + bits(64), // PT base addr + PTW_Level, // tree level for this recursive call + bool, // global translation, + ext_ptw) // ext_ptw + -> PTW_Result + +function pt_walk(sv_params, + va, + ac, + priv, + mxr, + do_sum, + pt_base, + level, + global, + ext_ptw) = { + let vpn_j = vpn_j_of_va(sv_params, va, level); + let pte_offset = vpn_j << sv_params.log_pte_size_bytes; + let pte_addr = pt_base + pte_offset; + + // In Sv32, physical addrs are actually 34 bits, not XLEN(=32) bits. + // 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[(sizeof(xlen) - 1) .. 0]; + + // Read this-level PTE from mem + let mem_result = mem_read_priv(Read(Data), // AccessType + Supervisor, // Privilege + pte_phys_addr, + 8, // atom (8) + false, // aq + false, // rl + false); // res + + match mem_result { + MemException(_) => PTW_Failure(PTW_Access(), ext_ptw), + MemValue(pte) => { + let pte_flags = Mk_PTE_Flags(pte[7 .. 0]); + if pte_is_invalid(pte_flags) then + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + else { + let ppns : bits(64) = PPNs_of_PTE(sv_params, pte); + let global' = global | (pte_flags[G] == 0b1); + if pte_is_ptr(pte_flags) then { + // Non-Leaf PTE + if level > 0 then { + // follow the pointer to walk next level + let pt_base' : bits(64) = ppns << pagesize_bits; + let level' = level - 1; + pt_walk(sv_params, va, ac, priv, mxr, do_sum, + pt_base', level', global', ext_ptw) + } + else + // level 0 PTE, but contains a pointer instead of a leaf + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } + else { + // Leaf PTE + let ext_pte = msbs_of_PTE(sv_params, pte); + let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags, + ext_pte, ext_ptw); + match pte_check { + PTE_Check_Failure(ext_ptw, ext_ptw_fail) => + PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw), + PTE_Check_Success(ext_ptw) => + if level > 0 then { + // Superpage; construct mask for lower-level PPNs from the PTE + let mask_bits = level * sv_params.pte_PPN_j_size_bits; + // Clear the lowest `mask_bits` bits. + let ppns_masked = (ppns >> mask_bits) << mask_bits; + if not(ppns == ppns_masked) then + // misaligned superpage mapping + PTW_Failure(PTW_Misaligned(), ext_ptw) + else { + // Compose final PA in superpage: + // Superpage PPN + lower VPNs + pagesize_bits page-offset + let mask : bits(64) = ~ (ones() << mask_bits); + let ppn = ppns | (vpns_of_va(sv_params, va) & mask); + let pa = (ppn << pagesize_bits) | zero_extend(offset_of_va(va)); + PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) + } + } + else { + let pa = (ppns << pagesize_bits) | zero_extend(offset_of_va(va)); + PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) + } + } + } + } + } + } +} + +// **************************************************************** +// Architectural SATP CSR + +// PUBLIC: see also riscv_insts_zicsr.sail and other CSR-related files +register satp : xlenbits + +// See riscv_sys_regs.sail for legalize_satp{32,64}(). +// WARNING: those functions legalize Mode but not ASID? +// PUBLIC: invoked from writeCSR() to fixup WARL fields +function legalize_satp(a : Architecture, + o : xlenbits, // previous value of satp + v : xlenbits) // proposed new value of satp + -> xlenbits = { // new legal value of satp + if sizeof(xlen) == 32 then { + // The slice and extend ops below are no-ops when xlen==32, + // but appease the type-checker when xlen==64 (when this code is not executed!) + let o32 : bits(32) = o[31 .. 0]; + let v32 : bits(32) = v[31 .. 0]; + let new_satp : bits(32) = legalize_satp32(a, o32, v32); + zero_extend(new_satp); + } else if sizeof(xlen) == 64 then { + // The extend and truncate ops below are no-ops when xlen==64, + // but appease the type-checker when xlen==32 (when this code is not executed!) + let o64 : bits(64) = zero_extend(o); + let v64 : bits(64) = zero_extend(v); + let new_satp : bits(64) = legalize_satp64(a, o64, v64); + truncate(new_satp, sizeof(xlen)) + } else + internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(sizeof(xlen))) +} + +// ---------------- +// Fields of SATP + +// ASID is 9b in Sv32, 16b in Sv39/Sv48/Sv57: we use 16b for both +// PRIVATE +function satp_to_asid(satp_val : xlenbits) -> asidbits = + if sizeof(xlen) == 32 then zero_extend(Mk_Satp32(satp_val)[Asid]) + else if sizeof(xlen) == 64 then Mk_Satp64(satp_val)[Asid] + else internal_error(__FILE__, __LINE__, + "Unsupported xlen" ^ dec_str(sizeof(xlen))) + +// Result is 64b to cover both RV32 and RV64 addrs +// PRIVATE +function satp_to_PT_base(satp_val : xlenbits) -> bits(64) = { + let ppn = if sizeof(xlen) == 32 then zero_extend (64, Mk_Satp32(satp_val)[PPN]) + else if sizeof(xlen) == 64 then zero_extend (64, Mk_Satp64(satp_val)[PPN]) + else internal_error(__FILE__, __LINE__, + "Unsupported xlen" ^ dec_str(sizeof(xlen))); + ppn << pagesize_bits +} + +// Compute address translation mode from SATP register +// PRIVATE +function translationMode(priv : Privilege) -> SATPMode = { + if priv == Machine then + Sbare + else if sizeof(xlen) == 32 then + match Mk_Satp32(satp)[Mode] { + 0b0 => Sbare, + 0b1 => Sv32 + } + else if sizeof(xlen) == 64 then { + // Translation mode is based on mstatus.SXL, which could be RV32 when xlen==64 + let arch = architecture(get_mstatus_SXL(mstatus)); + match arch { + Some(RV64) => { let mbits : bits(4) = satp[63 .. 60]; + match satp64Mode_of_bits(RV64, mbits) { // see riscv_types.sail + Some(m) => m, + None() => internal_error(__FILE__, __LINE__, + "invalid RV64 translation mode in satp") + } + }, + Some(RV32) => match Mk_Satp32(satp[31 .. 0])[Mode] { // Note: satp is 64bits here + // When xlen is 64, mstatus.SXL (for S privilege) can be RV32 + 0b0 => Sbare, + 0b1 => Sv32 + }, + _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") + } + } + else + internal_error(__FILE__, __LINE__, "unsupported xlen") +} + +// **************************************************************** +// VA to PA translation + +// Result of address translation + +// PUBLIC +union TR_Result('paddr : Type, 'failure : Type) = { + TR_Address : ('paddr, ext_ptw), + TR_Failure : ('failure, ext_ptw) +} + +// This function can be ignored on first reading since TLBs are not +// part of RISC-V architecture spec (see TLB_NOTE above). +// PRIVATE: translate on TLB hit, and maintenance of PTE in TLB +function translate_TLB_hit(sv_params : SV_Params, + asid : asidbits, + ptb : bits(64), + vAddr : bits(64), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + ext_ptw : ext_ptw, + tlb_index : nat, + ent : TLB_Entry) + -> TR_Result(bits(64), PTW_Error) = { + let pte = ent.pte; + let ext_pte = msbs_of_PTE(sv_params, pte); + let pte_flags = Mk_PTE_Flags(pte[7 .. 0]); + let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags, + ext_pte, + ext_ptw); + match pte_check { + PTE_Check_Failure(ext_ptw, ext_ptw_fail) => + TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw), + PTE_Check_Success(ext_ptw) => + match update_PTE_Bits(sv_params, pte, ac) { + None() => TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw), + Some(pte') => + // See riscv_platform.sail + if not(plat_enable_dirty_update()) then + // pte needs dirty/accessed update but that is not enabled + TR_Failure(PTW_PTE_Update(), ext_ptw) + else { + // 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[(sizeof(xlen) - 1) .. 0]; + let mv = mem_write_value_priv(pte_phys_addr, + 8, + pte', + Supervisor, + false, + false, + false); + match mv { + MemValue(_) => (), + MemException(e) => internal_error(__FILE__, __LINE__, + "invalid physical address in TLB") + }; + TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw) + } + } + } +} + +// PRIVATE: translate on TLB miss (do a page-table walk) +function translate_TLB_miss(sv_params : SV_Params, + asid : asidbits, + ptb : bits(64), + vAddr : bits(64), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + ext_ptw : ext_ptw) -> TR_Result(bits(64), PTW_Error) = { + let initial_level = sv_params.levels - 1; + let ptw_result = pt_walk(sv_params, vAddr, ac, priv, mxr, do_sum, + ptb, initial_level, false, ext_ptw); + match ptw_result { + PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), + PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { + let ext_pte = msbs_of_PTE(sv_params, pte); + // Without TLBs, this 'match' expression can be replaced simply + // by: 'TR_Address(pAddr, ext_ptw)' (see TLB_NOTE above) + match update_PTE_Bits(sv_params, pte, ac) { + None() => { + add_to_TLB(asid, vAddr, pAddr, pte, pteAddr, level, global, + sv_params.vpn_size_bits, + pagesize_bits); + TR_Address(pAddr, ext_ptw) + }, + Some(pte') => + // See riscv_platform.sail + if not(plat_enable_dirty_update()) then + // pte needs dirty/accessed update but that is not enabled + TR_Failure(PTW_PTE_Update(), ext_ptw) + else { + // Writeback the PTE (which has new A/D bits) + let pte_phys_addr = pteAddr[(sizeof(xlen) - 1) .. 0]; + let mv = mem_write_value_priv(pte_phys_addr, // pteAddr, + 8, + pte', + Supervisor, + false, + false, + false); + match mv { + MemValue(_) => { + add_to_TLB(asid, vAddr, pAddr, pte', pteAddr, level, global, + sv_params.vpn_size_bits, + pagesize_bits); + TR_Address(pAddr, ext_ptw) + }, + MemException(e) => + TR_Failure(PTW_Access(), ext_ptw) + } + } + } + } + } +} + +// PRIVATE +function translate(sv_params : SV_Params, + asid : asidbits, + ptb : bits(64), + vAddr_arg : bits(64), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + ext_ptw : ext_ptw) + -> TR_Result(bits(64), PTW_Error) = { + let va_mask : bits(64) = zero_extend(ones(sv_params.va_size_bits)); + let vAddr = (vAddr_arg & va_mask); + + // On first reading, assume lookup_TLB returns None(), since TLBs + // are not part of RISC-V archticture spec (see TLB_NOTE above) + match lookup_TLB(asid, vAddr) { + Some(index, ent) => translate_TLB_hit(sv_params, asid, ptb, vAddr, ac, priv, + mxr, do_sum, ext_ptw, index, ent), + None() => translate_TLB_miss(sv_params, asid, ptb, vAddr, ac, priv, + mxr, do_sum, ext_ptw) + } +} + +// Top-level addr-translation function +// PUBLIC: invoked from instr-fetch and load/store/amo +function translateAddr(vAddr : xlenbits, + ac : AccessType(ext_access_type)) + -> TR_Result(xlenbits, 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); + // 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), + Sv32 => (true, sv32_params), + Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params), + Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params), + // Sv57 => (is_valid_vAddr(sv57_params, vAddr_64b), sv57_params), // TODO + }; + if not(valid_va) then + TR_Failure(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw) + else { + let mxr = mstatus.MXR() == 0b1; + let do_sum = mstatus.SUM() == 0b1; + let asid : asidbits = satp_to_asid(satp); + let ptb : bits(64) = satp_to_PT_base(satp); + let tr_result1 = translate(sv_params, + asid, + ptb, + vAddr_64b, + ac, effPriv, mxr, do_sum, + init_ext_ptw); + // Fixup result PA or exception + match tr_result1 { + TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_ptw), + TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) + } + } +} + +// **************************************************************** +// Initialize Virtual Memory state + +// PUBLIC: invoked from init_model() +function init_vmem() -> unit = init_TLB() + +// **************************************************************** diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail index 375dfa370..d17cb0245 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -6,162 +6,109 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -/* Shared definitions for supervisor-mode page-table-entries and permission checks. - * - * These definitions are independent of xlen and do not involve - * accessing physical memory. - */ - -/* PageSize */ - -let PAGESIZE_BITS = 12 - -/* - * Definitions for RV32, which has a single address translation mode: Sv32. - */ - -type vaddr32 = bits(32) -type paddr32 = bits(34) -type pte32 = bits(32) - -/* asid */ -type asid32 = bits(9) - -function curAsid32(satp : bits(32)) -> asid32 = { - let s = Mk_Satp32(satp); - s[Asid] -} - -/* page table base from satp */ -function curPTB32(satp : bits(32)) -> paddr32 = { - let s : Satp32 = Mk_Satp32(satp); - shiftl(zero_extend(s[PPN]), PAGESIZE_BITS) +// **************************************************************** +// Parameters for VM modes sv32, sv39, sv48 and (TODO) Sv57 + +// All VM modes use the same page size (4KB, with 12-bit index) + +// This two-line idiom constrains the value (2nd line) to be a singleton, +// which helps in type-checking wherever it is used. +type PAGESIZE_BITS : Int = 12 +let pagesize_bits = sizeof(PAGESIZE_BITS) + +// PRIVATE +struct SV_Params = { + // VA + va_size_bits : {32, 39, 48}, // 32 39 48 + vpn_size_bits : {10, 9}, // 10 9 9 + + // PTE + levels : { 2, 3, 4}, // 2 3 4 + log_pte_size_bytes : { 2, 3}, // 2 3 3 + pte_msbs_lsb_index : {32, 54}, // 32 54 54 + pte_msbs_size_bits : { 0, 10}, // 0 10 10 + pte_PPNs_lsb_index : {10}, // 10 10 10 + pte_PPNs_size_bits : {22, 44}, // 22 44 44 + pte_PPN_j_size_bits : {10, 9} // 10 9 9 } -/* Sv32 parameters and bitfield layouts */ - -let SV32_LEVEL_BITS = 10 -let SV32_LEVELS = 2 -let PTE32_LOG_SIZE = 2 -let PTE32_SIZE = 4 - -bitfield SV32_Vaddr : vaddr32 = { - VPNi : 31 .. 12, - PgOfs : 11 .. 0 +// Current level during a page-table walk (0 to SV_Params.levels - 1) +type PTW_Level = range(0,3) // range(0,4) when add Sv57 (TODO) + +// PRIVATE +let sv32_params : SV_Params = struct { + // VA + va_size_bits = 32, + vpn_size_bits = 10, + + // PTE + levels = 2, + log_pte_size_bytes = 2, // 4 Bytes + pte_msbs_lsb_index = 32, + pte_msbs_size_bits = 0, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_bits = 22, + pte_PPN_j_size_bits = 10 } -bitfield SV32_Paddr : paddr32 = { - PPNi : 33 .. 12, - PgOfs : 11 .. 0 +// PRIVATE +let sv39_params : SV_Params = struct { + // VA + va_size_bits = 39, + vpn_size_bits = 9, + + // PTE + levels = 3, + log_pte_size_bytes = 3, // 8 Bytes + pte_msbs_lsb_index = 54, + pte_msbs_size_bits = 10, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_bits = 44, + pte_PPN_j_size_bits = 9 } -bitfield SV32_PTE : pte32 = { - PPNi : 31 .. 10, - RSW : 9 .. 8, - BITS : 7 .. 0 +// PRIVATE +let sv48_params : SV_Params = struct { + // VA + va_size_bits = 48, + vpn_size_bits = 9, + + // PTE + levels = 4, + log_pte_size_bytes = 3, // 8 Bytes + pte_msbs_lsb_index = 54, + pte_msbs_size_bits = 10, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_bits = 44, + pte_PPN_j_size_bits = 9 } +// TODO; not currently used +// PRIVATE /* - * Definitions for RV64, which has two defined address translation modes: Sv39 and Sv48. - */ - -/* Sv48 and Sv64 are reserved but not defined. The size of the VPN - * increases by 9 bits through Sv39, Sv48 and Sv57, but not for Sv64. - * Also, the 45-bit size of the VPN for Sv57 exceeds the 44-bit size - * of the PPN in satp64. Due to these corner cases, it is unlikely - * that definitions can be shared across all four schemes, so separate - * definitions might eventually be needed for each translation mode. - * - * But to keep things simple for now, since Sv39 and Sv48 have the - * same PPN size, we share some definitions. - */ - -type paddr64 = bits(56) -type pte64 = bits(64) - -/* asid */ - -type asid64 = bits(16) - -function curAsid64(satp : bits(64)) -> asid64 = { - let s = Mk_Satp64(satp); - s[Asid] -} - -/* page table base from satp */ -function curPTB64(satp : bits(64)) -> paddr64 = { - let s = Mk_Satp64(satp); - shiftl(zero_extend(s[PPN]), PAGESIZE_BITS) -} - -/* Sv39 parameters and bitfield layouts */ - -let SV39_LEVEL_BITS = 9 -let SV39_LEVELS = 3 -let PTE39_LOG_SIZE = 3 -let PTE39_SIZE = 8 - -type vaddr39 = bits(39) - -bitfield SV39_Vaddr : vaddr39 = { - VPNi : 38 .. 12, - PgOfs : 11 .. 0 -} - -bitfield SV39_Paddr : paddr64 = { - PPNi : 55 .. 12, - PgOfs : 11 .. 0 -} - -bitfield SV39_PTE : pte64 = { - Ext : 63 .. 54, - PPNi : 53 .. 10, - RSW : 9 .. 8, - BITS : 7 .. 0 -} - -/* Sv48 parameters and bitfield layouts */ - -let SV48_LEVEL_BITS = 9 -let SV48_LEVELS = 4 -let PTE48_LOG_SIZE = 3 -let PTE48_SIZE = 8 - -type vaddr48 = bits(48) -type pte48 = bits(64) - -bitfield SV48_Vaddr : vaddr48 = { - VPNi : 47 .. 12, - PgOfs : 11 .. 0 -} - -bitfield SV48_Paddr : paddr64 = { - PPNi : 55 .. 12, - PgOfs : 11 .. 0 -} - -bitfield SV48_PTE : pte48 = { - Ext : 63 .. 54, - PPNi : 53 .. 10, - RSW : 9 .. 8, - BITS : 7 .. 0 -} - -/* The types below are parameterized by 'paddr and 'pte to support - * various architectural widths (e.g. RV32, RV64). ext_ptw supports - * extensions to the default address translation and page-table-walk. - */ - -/* Result of a page-table walk. */ - -union PTW_Result('paddr : Type, 'pte : Type) = { - PTW_Success: ('paddr, 'pte, 'paddr, nat, bool, ext_ptw), - PTW_Failure: (PTW_Error, ext_ptw) -} - -/* Result of address translation */ - -union TR_Result('paddr : Type, 'failure : Type) = { - TR_Address : ('paddr, ext_ptw), - TR_Failure : ('failure, ext_ptw) +let sv57_params : SV_Params = struct { + // VA + va_size_bits = 57, + vpn_size_bits = 9, + + // PTE + levels = 5, + log_pte_size_bytes = 3, // 8 Bytes + pte_msbs_lsb_index = 54, + pte_msbs_size_bits = 10, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_bits = 44, + pte_PPN_j_size_bits = 9 } +*/ + +// This 'undefined_SV_Params()' function is not used anywhere, but is +// currently (2023-12) needed to work around an issue where Sail tries +// to figure out how it could do +// let x : SV_Params = undefined +// even though the code never does this. This has been fixed in Sail. +// The fix will become available in a new Sail release, at which point +// this function can be deleted (TODO). +// PRIVATE +val undefined_SV_Params : unit -> SV_Params +function undefined_SV_Params() = sv32_params diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail new file mode 100644 index 000000000..dfe032c0d --- /dev/null +++ b/model/riscv_vmem_pte.sail @@ -0,0 +1,135 @@ +/*=======================================================================================*/ +/* 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 */ +/*=======================================================================================*/ + +// **************************************************************** +// PTE (Page Table Entry) in PTN (Page Table Node) + +// PTE MSBs PPNs RSW BITs +// Sv32 - 31..10 9..8 7..0 +// Sv39 63..54 53..10 9..8 7..0 +// Sv48 63..54 53..10 9..8 7..0 + +// MSBs of PTE are reserved for RV64 extensions. +// There are not available bits on RV32, so these bits will be zeros on RV32. + +type pte_flags_bits = bits(8) + +// For PTW extensions (non-standard) +type extPte = bits(64) + +// PRIVATE: extract msbs of PTE above the PPN +function msbs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = { + let mask : bits(64) = zero_extend(ones(sv_params.pte_msbs_size_bits)); + (pte >> sv_params.pte_msbs_lsb_index) & mask +} + +// PRIVATE: extract PPNs of PTE +function PPNs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = { + let mask : bits(64) = zero_extend(ones(sv_params.pte_PPNs_size_bits)); + (pte >> sv_params.pte_PPNs_lsb_index) & mask +} + +// PRIVATE: 8 LSBs of PTEs in Sv32, Sv39, Sv48 and Sv57 +bitfield PTE_Flags : pte_flags_bits = { + D : 7, // dirty + A : 6, // accessed + G : 5, // global + U : 4, // User + X : 3, // Execute permission + W : 2, // Write permission + R : 1, // Read permission + V : 0 // Valid +} + +// PRIVATE: check if a PTE is a pointer to next level (non-leaf) +function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0) + & (pte_flags[W] == 0b0) + & (pte_flags[R] == 0b0) + +// PRIVATE: check if a PTE is valid +function pte_is_invalid(pte_flags : PTE_Flags) -> bool = (pte_flags[V] == 0b0) + | ((pte_flags[W] == 0b1) + & (pte_flags[R] == 0b0)) + +// ---------------- +// Check access permissions in PTE + +// For (non-standard) extensions: this function gets the extension-available bits +// of the PTE in extPte, and the accumulated information of the page-table-walk +// in ext_ptw. It should return the updated ext_ptw in both success and failure cases. + +union PTE_Check = { + PTE_Check_Success : ext_ptw, + PTE_Check_Failure : (ext_ptw, ext_ptw_fail) +} + +// PRIVATE +function check_PTE_permission(ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + pte_flags : PTE_Flags, + ext : extPte, + ext_ptw : ext_ptw) -> PTE_Check = { + let pte_U = pte_flags[U]; + let pte_R = pte_flags[R]; + let pte_W = pte_flags[W]; + let pte_X = pte_flags[X]; + let success : bool = + match (ac, priv) { + (Read(_), User) => (pte_U == 0b1) + & ((pte_R == 0b1) + | ((pte_X == 0b1 & mxr))), + (Write(_), User) => (pte_U == 0b1) & (pte_W == 0b1), + (ReadWrite(_, _), User) => (pte_U == 0b1) + & (pte_W == 0b1) + & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), + (Execute(), User) => (pte_U == 0b1) & (pte_X == 0b1), + (Read(_), Supervisor) => ((pte_U == 0b0) | do_sum) + & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), + (Write(_), Supervisor) => ((pte_U == 0b0) | do_sum) + & (pte_W == 0b1), + (ReadWrite(_, _), Supervisor) => ((pte_U == 0b0) | do_sum) + & (pte_W == 0b1) + & ((pte_R == 0b1) + | ((pte_X == 0b1) & mxr)), + (Execute(), Supervisor) => (pte_U == 0b0) & (pte_X == 0b1), + (_, Machine) => internal_error(__FILE__, __LINE__, + "m-mode mem perm check")}; + if success then PTE_Check_Success(()) + else PTE_Check_Failure((), ()) +} + +// Update PTE bits if needed; return new PTE if updated +// PRIVATE +function update_PTE_Bits(sv_params : SV_Params, + pte : bits(64), + a : AccessType(ext_access_type)) + -> option(bits(64)) = { + let pte_flags = Mk_PTE_Flags(pte [7 .. 0]); + + // Update 'dirty' bit? + let update_d : bool = (pte_flags[D] == 0b0) + & (match a { + Execute() => false, + Read() => false, + Write(_) => true, + ReadWrite(_, _) => true + }); + // Update 'accessed'-bit? + let update_a = (pte_flags[A] == 0b0); + + if update_d | update_a then { + let pte_flags = [pte_flags with + A = 0b1, + D = (if update_d then 0b1 else pte_flags[D])]; + Some(pte[63 .. 8] @ pte_flags.bits()) + } + else + None() +} diff --git a/model/riscv_ptw.sail b/model/riscv_vmem_ptw.sail similarity index 59% rename from model/riscv_ptw.sail rename to model/riscv_vmem_ptw.sail index a880def47..ab73b1909 100644 --- a/model/riscv_ptw.sail +++ b/model/riscv_vmem_ptw.sail @@ -6,21 +6,27 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -/* failure modes for address-translation/page-table-walks */ +// **************************************************************** +// PTW exceptions +// 'ext_ptw' supports (non-standard) extensions to the default addr-translation and PTW. +// See riscv_types_ext.sail for definitions. + +// Failure modes for address-translation/page-table-walks +// PRIVATE union PTW_Error = { - PTW_Invalid_Addr : unit, /* invalid source address */ - PTW_Access : unit, /* physical memory access error for a PTE */ + PTW_Invalid_Addr : unit, // invalid source address + PTW_Access : unit, // physical memory access error for a PTE PTW_Invalid_PTE : unit, PTW_No_Permission : unit, - PTW_Misaligned : unit, /* misaligned superpage */ - PTW_PTE_Update : unit, /* PTE update needed but not enabled */ - PTW_Ext_Error : ext_ptw_error /* parameterized for errors from extensions */ + PTW_Misaligned : unit, // misaligned superpage + PTW_PTE_Update : unit, // PTE update needed but not enabled + PTW_Ext_Error : ext_ptw_error // parameterized for errors from extensions } -val ptw_error_to_str : PTW_Error -> string -function ptw_error_to_str(e) = - match (e) { +// PRIVATE: only 'to_str' overload is public +function ptw_error_to_str(e : PTW_Error) -> string = { + match e { PTW_Invalid_Addr() => "invalid-source-addr", PTW_Access() => "mem-access-error", PTW_Invalid_PTE() => "invalid-pte", @@ -29,19 +35,23 @@ function ptw_error_to_str(e) = PTW_PTE_Update() => "pte-update-needed", PTW_Ext_Error(e) => "extension-error" } +} +// PUBLIC overload to_str = {ptw_error_to_str} -/* hook for extensions to customize errors reported by page-table - * walks during address translation; it typically works in conjunction - * with any customization to checkPTEPermission(). - */ +// hook for (non-standard) extensions to customize errors reported by page-table +// walks during address translation; it typically works in conjunction +// with any customization to check_PTE_permission(). + +// PRIVATE function ext_get_ptw_error(eptwf : ext_ptw_fail) -> PTW_Error = PTW_No_Permission() -/* conversion of these translation/PTW failures into architectural exceptions */ -function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = { - let e : ExceptionType = +// Convert translation/PTW failures into architectural exceptions +function translationException(a : AccessType(ext_access_type), + f : PTW_Error) + -> ExceptionType = { match (a, f) { (_, PTW_Ext_Error(e)) => E_Extension(ext_translate_exception(e)), (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), @@ -52,8 +62,5 @@ function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> (Write(_), _) => E_SAMO_Page_Fault(), (Execute(), PTW_Access()) => E_Fetch_Access_Fault(), (Execute(), _) => E_Fetch_Page_Fault() - } in { -/* print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */ - e } } diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail deleted file mode 100644 index 33cc9c123..000000000 --- a/model/riscv_vmem_rv32.sail +++ /dev/null @@ -1,75 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -/* RV32 Supervisor-mode address translation and page-table walks. */ - -/* Define the architectural satp and its legalizer. */ - -register satp : xlenbits - -function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = - legalize_satp32(a, o, v) - -/* Compute the address translation mode. */ - -val translationMode : (Privilege) -> SATPMode -function translationMode(priv) = { - if priv == Machine then Sbare - else { - let arch = architecture(get_mstatus_SXL(mstatus)); - match arch { - Some(RV32) => { - let s = Mk_Satp32(satp[31..0]); - if s[Mode] == 0b0 then Sbare else Sv32 - }, - _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") - } - } -} - -/* Top-level address translation dispatcher */ - -val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) -function translateAddr_priv(vAddr, ac, effPriv) = { - let mxr : bool = mstatus[MXR] == 0b1; - let do_sum : bool = mstatus[SUM] == 0b1; - let mode : SATPMode = translationMode(effPriv); - - let asid = curAsid32(satp); - let ptb = curPTB32(satp); - - /* PTW extensions: initialize the PTW extension state */ - let ext_ptw : ext_ptw = init_ext_ptw; - - match mode { - Sbare => TR_Address(vAddr, ext_ptw), - Sv32 => match translate32(asid, ptb, vAddr, ac, effPriv, mxr, do_sum, SV32_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(to_phys_addr(pa), ext_ptw), - TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) - }, - _ => internal_error(__FILE__, __LINE__, "unsupported address translation scheme") - } -} - -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) -function translateAddr(vAddr, ac) = - translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege)) - -val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit -function flush_TLB(asid_xlen, addr_xlen) -> unit = { - let asid : option(asid32) = - match (asid_xlen) { - None() => None(), - Some(a) => Some(a[8 .. 0]) - }; - flush_TLB32(asid, addr_xlen) -} - -function init_vmem () -> unit = { - init_vmem_sv32() -} diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail deleted file mode 100644 index 9ead6425f..000000000 --- a/model/riscv_vmem_rv64.sail +++ /dev/null @@ -1,114 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -/* RV64 Supervisor-mode address translation and page-table walks. */ - -/* Define the architectural satp and its legalizer. */ - -register satp : xlenbits - -function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = - legalize_satp64(a, o, v) - -/* Define valid source addresses for translation */ - -function isValidSv39Addr(vAddr : xlenbits) -> bool = { - vAddr[63 .. 39] == (if vAddr[38] == bitone - then ones() - else zeros()) -} - -function isValidSv48Addr(vAddr : xlenbits) -> bool = { - vAddr[63 .. 48] == (if vAddr[47] == bitone - then ones() - else zeros()) -} - -/* Compute the address translation mode. */ - -val translationMode : (Privilege) -> SATPMode -function translationMode(priv) = { - if priv == Machine then Sbare - else { - let arch = architecture(get_mstatus_SXL(mstatus)); - match arch { - Some(RV64) => { - let mbits : satp_mode = Mk_Satp64(satp)[Mode]; - match satp64Mode_of_bits(RV64, mbits) { - Some(m) => m, - None() => internal_error(__FILE__, __LINE__, "invalid RV64 translation mode in satp") - } - }, - Some(RV32) => { - let s = Mk_Satp32(satp[31..0]); - if s[Mode] == 0b0 then Sbare else Sv32 - }, - _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") - } - } -} - -/* Top-level address translation dispatcher */ - -val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) -function translateAddr_priv(vAddr, ac, effPriv) = { - let mxr : bool = mstatus[MXR] == 0b1; - let do_sum : bool = mstatus[SUM] == 0b1; - let mode : SATPMode = translationMode(effPriv); - - let asid = curAsid64(satp); - let ptb = curPTB64(satp); - - /* PTW extensions: initialize the PTW extension state. */ - let ext_ptw : ext_ptw = init_ext_ptw; - - match mode { - Sbare => TR_Address(vAddr, ext_ptw), - Sv39 => { if isValidSv39Addr(vAddr) - then match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw), - TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) - } - else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) - }, - Sv48 => { if isValidSv48Addr(vAddr) - then match translate48(asid, ptb, vAddr[47 .. 0], ac, effPriv, mxr, do_sum, SV48_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw), - TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) - } - else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) - }, - _ => internal_error(__FILE__, __LINE__, "unsupported address translation scheme") - } -} - -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) -function translateAddr(vAddr, ac) = - translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege)) - -val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit -function flush_TLB(asid_xlen, addr_xlen) -> unit = { - /* Flush both Sv39 and Sv48 TLBs. */ - let (addr39, addr48) : (option(vaddr39), option(vaddr48)) = - match addr_xlen { - None() => (None(), None()), - Some(a) => (Some(a[38 .. 0]), Some(a[47 .. 0])) - }; - let asid : option(asid64) = - match asid_xlen { - None() => None(), - Some(a) => Some(a[15 .. 0]) - }; - flush_TLB39(asid, addr39); - flush_TLB48(asid, addr48) -} - -function init_vmem() -> unit = { - init_vmem_sv39(); - init_vmem_sv48() -} diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail deleted file mode 100644 index 1de109c28..000000000 --- a/model/riscv_vmem_sv32.sail +++ /dev/null @@ -1,200 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -/* Sv32 address translation for RV32. */ - -/* FIXME: paddr32 is 34-bits, but phys_mem accesses in riscv_mem take 32-bit (xlenbits) addresses. - * Define a converter for now. - */ - -function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] - -val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) -function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { - let va = Mk_SV32_Vaddr(vaddr); - let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), - PTE32_LOG_SIZE); - let pte_addr = ptb + pt_ofs; - match (mem_read_priv(Read(Data), Supervisor, to_phys_addr(pte_addr), 4, false, false, false)) { - MemException(_) => { -/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) - ^ " pt_base=" ^ BitStr(to_phys_addr(ptb)) - ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) - ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) - ^ ": invalid pte address"); */ - PTW_Failure(PTW_Access(), ext_ptw) - }, - MemValue(v) => { - let pte = Mk_SV32_PTE(v); - let pbits = pte[BITS]; - let ext_pte : extPte = default_sv32_ext_pte; - let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr[G] == 0b1); -/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) - ^ " pt_base=" ^ BitStr(to_phys_addr(ptb)) - ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) - ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) - ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits, ext_pte) then { -/* print("walk32: invalid pte"); */ - PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - if isPTEPtr(pbits, ext_pte) then { - if level > 0 then { - /* walk down the pointer to the next level */ - walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) - } else { - /* last-level PTE contains a pointer instead of a leaf */ -/* print("walk32: last-level pte contains a ptr"); */ - PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } - } else { /* leaf PTE */ - match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { -/* print("walk32: pte permission check failure"); */ - PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) - }, - PTE_Check_Success(ext_ptw) => { - if level > 0 then { /* superpage */ - /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV32_LEVEL_BITS) - 1; - if (pte[PPNi] & mask) != zero_extend(0b0) then { - /* misaligned superpage mapping */ -/* print("walk32: misaligned superpage mapping"); */ - PTW_Failure(PTW_Misaligned(), ext_ptw) - } else { - /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); -/* let res = append(ppn, va[PgOfs]); - print("walk32: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) - ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) - } - } else { - /* normal leaf PTE */ -/* let res = append(pte[PPNi], va[PgOfs]); - print("walk32: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) - } - } - } - } - } - } - } -} - -/* TLB management: single entry for now */ - -// ideally we would use the below form: -// type TLB32_Entry = TLB_Entry(sizeof(asid32), sizeof(vaddr32), sizeof(paddr32), sizeof(pte32)) -type TLB32_Entry = TLB_Entry(9, 32, 34, 32) -register tlb32 : option(TLB32_Entry) - -val lookup_TLB32 : (asid32, vaddr32) -> option((nat, TLB32_Entry)) -function lookup_TLB32(asid, vaddr) = - match tlb32 { - None() => None(), - Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() - } - -val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit -function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV32_LEVEL_BITS); - tlb32 = Some(ent) -} - -function write_TLB32(idx : nat, ent : TLB32_Entry) -> unit = - tlb32 = Some(ent) - -val flush_TLB32 : (option(asid32), option(vaddr32)) -> unit -function flush_TLB32(asid, addr) = - match (tlb32) { - None() => (), - Some(e) => if flush_TLB_Entry(e, asid, addr) - then tlb32 = None() - else () - } - -/* address translation */ - -val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) -function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { - match lookup_TLB32(asid, vAddr) { - Some(idx, ent) => { -/* print("translate32: TLB32 hit for " ^ BitStr(vAddr)); */ - let pte = Mk_SV32_PTE(ent.pte); - let ext_pte : extPte = zeros(); // no reserved bits for extensions - let pteBits = Mk_PTE_Bits(pte[BITS]); - match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, - PTE_Check_Success(ext_ptw) => { - match update_PTE_Bits(pteBits, ac, ext_pte) { - None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), - Some(pbits, ext) => { - if not(plat_enable_dirty_update()) - then { - /* pte needs dirty/accessed update but that is not enabled */ - TR_Failure(PTW_PTE_Update(), ext_ptw) - } else { - /* update PTE entry and TLB */ - n_pte = update_BITS(pte, pbits.bits); - /* ext is unused since there are no reserved bits for extensions */ - n_ent : TLB32_Entry = ent; - n_ent.pte = n_pte.bits; - write_TLB32(idx, n_ent); - /* update page table */ - match mem_write_value_priv(to_phys_addr(zero_extend(ent.pteAddr)), 4, n_pte.bits, Supervisor, false, false, false) { - MemValue(_) => (), - MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") - }; - TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw) - } - } - } - } - } - }, - None() => { - match walk32(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { - PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), - PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, zeros()) { - None() => { - add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) - }, - Some(pbits, ext) => - if not(plat_enable_dirty_update()) - then { - /* pte needs dirty/accessed update but that is not enabled */ - TR_Failure(PTW_PTE_Update(), ext_ptw) - } else { - var w_pte : SV32_PTE = update_BITS(pte, pbits.bits); - /* ext is unused since there are no reserved bits for extensions */ - match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits, Supervisor, false, false, false) { - MemValue(_) => { - add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) - }, - MemException(e) => { - /* pte is not in valid memory */ - TR_Failure(PTW_Access(), ext_ptw) - } - } - } - } - } - } - } - } -} - -function init_vmem_sv32() -> unit = { - tlb32 = None() -} diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail deleted file mode 100644 index 68f3d553c..000000000 --- a/model/riscv_vmem_sv39.sail +++ /dev/null @@ -1,194 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -/* Sv39 address translation for RV64. */ - -val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) -function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { - let va = Mk_SV39_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), - PTE39_LOG_SIZE); - let pte_addr = ptb + pt_ofs; - match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { - MemException(_) => { -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) - ^ " pt_base=" ^ BitStr(ptb) - ^ " pt_ofs=" ^ BitStr(pt_ofs) - ^ " pte_addr=" ^ BitStr(pte_addr) - ^ ": invalid pte address"); */ - PTW_Failure(PTW_Access(), ext_ptw) - }, - MemValue(v) => { - let pte = Mk_SV39_PTE(v); - let pbits = pte[BITS]; - let ext_pte = pte[Ext]; - let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr[G] == 0b1); -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) - ^ " pt_base=" ^ BitStr(ptb) - ^ " pt_ofs=" ^ BitStr(pt_ofs) - ^ " pte_addr=" ^ BitStr(pte_addr) - ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits, ext_pte) then { -/* print("walk39: invalid pte"); */ - PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - if isPTEPtr(pbits, ext_pte) then { - if level > 0 then { - /* walk down the pointer to the next level */ - walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) - } else { - /* last-level PTE contains a pointer instead of a leaf */ -/* print("walk39: last-level pte contains a ptr"); */ - PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } - } else { /* leaf PTE */ - match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { -/* print("walk39: pte permission check failure"); */ - PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) - }, - PTE_Check_Success(ext_ptw) => { - if level > 0 then { /* superpage */ - /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; - if (pte[PPNi] & mask) != zero_extend(0b0) then { - /* misaligned superpage mapping */ -/* print("walk39: misaligned superpage mapping"); */ - PTW_Failure(PTW_Misaligned(), ext_ptw) - } else { - /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); -/* let res = append(ppn, va[PgOfs]); - print("walk39: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) - ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) - } - } else { - /* normal leaf PTE */ -/* let res = append(pte[PPNi], va[PgOfs]); - print("walk39: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) - } - } - } - } - } - } - } -} - -/* TLB management: single entry for now */ - -// ideally we would use the below form: -// type TLB39_Entry = TLB_Entry(sizeof(asid64), sizeof(vaddr39), sizeof(paddr64), sizeof(pte64)) -type TLB39_Entry = TLB_Entry(16, 39, 56, 64) -register tlb39 : option(TLB39_Entry) - -val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry)) -function lookup_TLB39(asid, vaddr) = - match tlb39 { - None() => None(), - Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() - } - -val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit -function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV39_LEVEL_BITS); - tlb39 = Some(ent) -} - -function write_TLB39(idx : nat, ent : TLB39_Entry) -> unit = - tlb39 = Some(ent) - -val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit -function flush_TLB39(asid, addr) = - match (tlb39) { - None() => (), - Some(e) => if flush_TLB_Entry(e, asid, addr) - then tlb39 = None() - else () - } - -/* address translation */ - -val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) -function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { - match lookup_TLB39(asid, vAddr) { - Some(idx, ent) => { -/* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */ - let pte = Mk_SV39_PTE(ent.pte); - let ext_pte = pte[Ext]; - let pteBits = Mk_PTE_Bits(pte[BITS]); - match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, - PTE_Check_Success(ext_ptw) => { - match update_PTE_Bits(pteBits, ac, ext_pte) { - None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), - Some(pbits, ext) => { - if not(plat_enable_dirty_update()) - then { - /* pte needs dirty/accessed update but that is not enabled */ - TR_Failure(PTW_PTE_Update(), ext_ptw) - } else { - /* update PTE entry and TLB */ - n_pte = update_BITS(pte, pbits.bits); - n_pte = update_Ext(n_pte, ext); - n_ent : TLB39_Entry = ent; - n_ent.pte = n_pte.bits; - write_TLB39(idx, n_ent); - /* update page table */ - match mem_write_value_priv(zero_extend(ent.pteAddr), 8, n_pte.bits, Supervisor, false, false, false) { - MemValue(_) => (), - MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") - }; - TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw) - } - } - } - } - } - }, - None() => { - match walk39(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { - PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), - PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { - None() => { - add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) - }, - Some(pbits, ext) => - if not(plat_enable_dirty_update()) - then { - /* pte needs dirty/accessed update but that is not enabled */ - TR_Failure(PTW_PTE_Update(), ext_ptw) - } else { - var w_pte : SV39_PTE = update_BITS(pte, pbits.bits); - w_pte = update_Ext(w_pte, ext); - match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { - MemValue(_) => { - add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) - }, - MemException(e) => { - /* pte is not in valid memory */ - TR_Failure(PTW_Access(), ext_ptw) - } - } - } - } - } - } - } - } -} - -function init_vmem_sv39() -> unit = { - tlb39 = None() -} diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail deleted file mode 100644 index 517450aa0..000000000 --- a/model/riscv_vmem_sv48.sail +++ /dev/null @@ -1,156 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -/* Sv48 address translation for RV64. */ - -val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) -function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { - let va = Mk_SV48_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), - PTE48_LOG_SIZE); - let pte_addr = ptb + pt_ofs; - match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { - MemException(_) => { -/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) - ^ " pt_base=" ^ BitStr(ptb) - ^ " pt_ofs=" ^ BitStr(pt_ofs) - ^ " pte_addr=" ^ BitStr(pte_addr) - ^ ": invalid pte address"); */ - PTW_Failure(PTW_Access(), ext_ptw) - }, - MemValue(v) => { - let pte = Mk_SV48_PTE(v); - let pbits = pte[BITS]; - let ext_pte = pte[Ext]; - let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr[G] == 0b1); -/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) - ^ " pt_base=" ^ BitStr(ptb) - ^ " pt_ofs=" ^ BitStr(pt_ofs) - ^ " pte_addr=" ^ BitStr(pte_addr) - ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits, ext_pte) then { -/* print("walk48: invalid pte"); */ - PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - if isPTEPtr(pbits, ext_pte) then { - if level > 0 then { - /* walk down the pointer to the next level */ - walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) - } else { - /* last-level PTE contains a pointer instead of a leaf */ -/* print("walk48: last-level pte contains a ptr"); */ - PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } - } else { /* leaf PTE */ - match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { -/* print("walk48: pte permission check failure"); */ - PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) - }, - PTE_Check_Success(ext_ptw) => { - if level > 0 then { /* superpage */ - /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; - if (pte[PPNi] & mask) != zero_extend(0b0) then { - /* misaligned superpage mapping */ -/* print("walk48: misaligned superpage mapping"); */ - PTW_Failure(PTW_Misaligned(), ext_ptw) - } else { - /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); -/* let res = append(ppn, va[PgOfs]); - print("walk48: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) - ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) - } - } else { - /* normal leaf PTE */ -/* let res = append(pte[PPNi], va[PgOfs]); - print("walk48: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) - } - } - } - } - } - } - } -} - -/* TLB management: single entry for now */ - -// ideally we would use the below form: -// type TLB48_Entry = TLB_Entry(sizeof(asid64), sizeof(vaddr48), sizeof(paddr64), sizeof(pte64)) -type TLB48_Entry = TLB_Entry(16, 48, 56, 64) -register tlb48 : option(TLB48_Entry) - -val lookup_TLB48 : (asid64, vaddr48) -> option((nat, TLB48_Entry)) -function lookup_TLB48(asid, vaddr) = - match tlb48 { - None() => None(), - Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() - } - -val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit -function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV48_LEVEL_BITS); - tlb48 = Some(ent) -} - -function write_TLB48(idx : nat, ent : TLB48_Entry) -> unit = - tlb48 = Some(ent) - -val flush_TLB48 : (option(asid64), option(vaddr48)) -> unit -function flush_TLB48(asid, addr) = - match (tlb48) { - None() => (), - Some(e) => if flush_TLB_Entry(e, asid, addr) - then tlb48 = None() - else () - } - -/* address translation */ - -val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) -function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { - match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { - PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), - PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { - None() => { - add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) - }, - Some(pbits, ext) => - if not(plat_enable_dirty_update()) - then { - /* pte needs dirty/accessed update but that is not enabled */ - TR_Failure(PTW_PTE_Update(), ext_ptw) - } else { - var w_pte : SV48_PTE = update_BITS(pte, pbits.bits); - w_pte = update_Ext(w_pte, ext); - match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { - MemValue(_) => { - add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) - }, - MemException(e) => { - /* pte is not in valid memory */ - TR_Failure(PTW_Access(), ext_ptw) - } - } - } - } - } - } -} - -function init_vmem_sv48() -> unit = { - tlb48 = None() -} diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail index a0e51ca2e..828fa723c 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -6,53 +6,51 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -/* idealized generic TLB entry to model fence.vm and also speed up simulation. */ - -struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int) = { - asid : bits('asidlen), - global : bool, - vAddr : bits('valen), /* VPN */ - pAddr : bits('palen), /* PPN */ - vMatchMask : bits('valen), /* matching mask for superpages */ - vAddrMask : bits('valen), /* selection mask for superpages */ - pte : bits('ptelen), /* PTE */ - pteAddr : bits('palen), /* for dirty writeback */ - age : bits(64) -} +// Although a TLB is not part of the RISC-V Architecture +// specification, we model a simple TLB so that +// (1) we can meaningfully test SFENCE.VMA which would be a no-op wihout a TLB; +// (2) we can greatly speed up simulation speed (for Linux boot, can +// reduce elapsed time from 10s of minutes to few minutes). +type asidbits = bits(16) -val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, 'valen > 0. - (bits('asidlen), bool, bits('valen), bits('palen), bits('ptelen), nat, bits('palen), nat) - -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen) -function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBitSize) = { - let shift : nat = PAGESIZE_BITS + (level * levelBitSize); - /* fixme hack: use a better idiom for masks */ - let vAddrMask : bits('valen) = shiftl(vAddr ^ vAddr ^ zero_extend(0b1), shift) - 1; - let vMatchMask : bits('valen) = ~ (vAddrMask); - struct { - asid = asid, - global = global, - pte = pte, - pteAddr = pteAddr, - vAddrMask = vAddrMask, - vMatchMask = vMatchMask, - vAddr = vAddr & vMatchMask, - pAddr = shiftl(shiftr(pAddr, shift), shift), - age = mcycle - } +// PRIVATE +struct TLB_Entry = { + asid : asidbits, // address-space id + global : bool, // global translation + vAddr : bits(64), // VPN + pAddr : bits(64), // ppn + vMatchMask : bits(64), // matching mask for superpages + vAddrMask : bits(64), // selection mask for superpages + pte : bits(64), // PTE + pteAddr : bits(64), // for dirty writeback + age : bits(64) // for replacement policy? } -val match_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen. - (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), bits('asidlen), bits('valen)) - -> bool -function match_TLB_Entry(ent, asid, vaddr) = - (ent.global | (ent.asid == asid)) & (ent.vAddr == (ent.vMatchMask & vaddr)) - -val flush_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen. - (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), option(bits('asidlen)), option(bits('valen))) - -> bool -function flush_TLB_Entry(e, asid, addr) = { - match(asid, addr) { +// Single-entry TLB (could enlarge this in future for better simulation speed) +// PRIVATE +register tlb : option(TLB_Entry) = None() + +// PUBLIC: invoked in init_vmem() [riscv_vmem.sail] +function init_TLB() -> unit = + tlb = None() + +// PUBLIC: invoked in translate_TLB_hit() [riscv_vmem.sail] +function write_TLB(idx : nat, ent : TLB_Entry) -> unit = + tlb = Some(ent) + +// PRIVATE +function match_TLB_Entry(ent : TLB_Entry, + asid : asidbits, + vaddr : bits(64)) -> bool = + (ent.global | (ent.asid == asid)) + & (ent.vAddr == (ent.vMatchMask & vaddr)) + +// PRIVATE +function flush_TLB_Entry(e : TLB_Entry, + asid : option(asidbits), + addr : option(bits(64))) -> bool = { + match (asid, addr) { ( None(), None()) => true, ( None(), Some(a)) => e.vAddr == (e.vMatchMask & a), (Some(i), None()) => (e.asid == i) & not(e.global), @@ -60,3 +58,58 @@ function flush_TLB_Entry(e, asid, addr) = { & not(e.global)) } } + +// PUBLIC: invoked in translate() [riscv_vmem.sail] +function lookup_TLB (asid : asidbits, vaddr : bits(64)) -> option((nat, TLB_Entry)) = + match tlb { + None() => None(), + Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() + } + +// PRIVATE +function add_to_TLB(asid : asidbits, + vAddr : bits(64), + pAddr : bits(64), + pte : bits(64), + pteAddr : bits(64), + level : nat, + global : bool, + levelBitSize : nat, + PAGESIZE_BITS : nat) -> unit = { + let shift = PAGESIZE_BITS + (level * levelBitSize); + assert(shift <= 64); + let vAddrMask : bits(64) = zero_extend(ones(shift)); + let vMatchMask : bits(64) = ~ (vAddrMask); + let entry : TLB_Entry = struct{asid = asid, + global = global, + pte = pte, + pteAddr = pteAddr, + vAddrMask = vAddrMask, + vMatchMask = vMatchMask, + vAddr = vAddr & vMatchMask, + pAddr = shiftl(shiftr(pAddr, shift), shift), + age = mcycle}; + tlb = Some(entry) +} + +// Top-level TLB flush function +// PUBLIC: invoked from exec SFENCE_VMA +function flush_TLB(asid_xlen : option(xlenbits), + addr_xlen : option(xlenbits)) -> unit = { + let asid : option(asidbits) = + match asid_xlen { + None() => None(), + Some(a) => Some(a[15 .. 0]) + }; + let addr_64b : option(bits(64)) = + match addr_xlen { + None() => None(), + Some(a) => Some(zero_extend(a)) + }; + match tlb { + None() => (), + Some(e) => if flush_TLB_Entry(e, asid, addr_64b) + then tlb = None() + else () + } +}